A Comparison of two Proof Critics: Power vs. Robustness
Proof critics are a technology from the proof planning paradigm. They examine failed proof attempts in order to extract information which can be used to generate a patch which will allow the proof to go through. We consider the proof of the $quot;whisky problem$quot;, a challenge problem from the d...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Conference or Workshop Item |
| Published: |
Springer
2002
|
| Online Access: | https://eprints.nottingham.ac.uk/321/ |
| _version_ | 1848790392382685184 |
|---|---|
| author | Dennis, Louise Abigail Bundy, Alan |
| author2 | Carreno, V. A. |
| author_facet | Carreno, V. A. Dennis, Louise Abigail Bundy, Alan |
| author_sort | Dennis, Louise Abigail |
| building | Nottingham Research Data Repository |
| collection | Online Access |
| description | Proof critics are a technology from the proof planning paradigm. They examine failed proof attempts in order to extract information which can be used to generate a patch which will allow the proof to go through.
We consider the proof of the $quot;whisky problem$quot;, a challenge problem from the domain of temporal logic. The proof requires a generalisation of the original conjecture and we examine two proof critics which can be used to create this generalisation. Using these critics we believe we have produced the first automatic proofs of this challenge problem.
We use this example to motivate a comparison of the two critics and propose that there is a place for specialist critics as well as powerful
general critics. In particular we advocate the development of critics
that do not use meta-variables. |
| first_indexed | 2025-11-14T18:11:53Z |
| format | Conference or Workshop Item |
| id | nottingham-321 |
| institution | University of Nottingham Malaysia Campus |
| institution_category | Local University |
| last_indexed | 2025-11-14T18:11:53Z |
| publishDate | 2002 |
| publisher | Springer |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | nottingham-3212020-05-04T20:32:21Z https://eprints.nottingham.ac.uk/321/ A Comparison of two Proof Critics: Power vs. Robustness Dennis, Louise Abigail Bundy, Alan Proof critics are a technology from the proof planning paradigm. They examine failed proof attempts in order to extract information which can be used to generate a patch which will allow the proof to go through. We consider the proof of the $quot;whisky problem$quot;, a challenge problem from the domain of temporal logic. The proof requires a generalisation of the original conjecture and we examine two proof critics which can be used to create this generalisation. Using these critics we believe we have produced the first automatic proofs of this challenge problem. We use this example to motivate a comparison of the two critics and propose that there is a place for specialist critics as well as powerful general critics. In particular we advocate the development of critics that do not use meta-variables. Springer Carreno, V. A. Munoz, C. A. Tahar, S. 2002 Conference or Workshop Item PeerReviewed Dennis, Louise Abigail and Bundy, Alan (2002) A Comparison of two Proof Critics: Power vs. Robustness. In: Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, August 20-23, 2002, Hampton, VA, USA. |
| spellingShingle | Dennis, Louise Abigail Bundy, Alan A Comparison of two Proof Critics: Power vs. Robustness |
| title | A Comparison of two Proof Critics: Power vs. Robustness |
| title_full | A Comparison of two Proof Critics: Power vs. Robustness |
| title_fullStr | A Comparison of two Proof Critics: Power vs. Robustness |
| title_full_unstemmed | A Comparison of two Proof Critics: Power vs. Robustness |
| title_short | A Comparison of two Proof Critics: Power vs. Robustness |
| title_sort | comparison of two proof critics: power vs. robustness |
| url | https://eprints.nottingham.ac.uk/321/ |