Skip to main content

Research Repository

See what's under the surface

Advanced Search

A Comparison of two Proof Critics: Power vs. Robustness

Dennis, Louise Abigail; Bundy, Alan

Authors

Louise Abigail Dennis

Alan Bundy



Contributors

V. A. Carreno
Editor

C. A. Munoz
Editor

S. Tahar
Editor

Abstract

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.

Publication Date Jan 1, 2002
Peer Reviewed Peer Reviewed
APA6 Citation Dennis, L. A., & Bundy, A. (2002). A Comparison of two Proof Critics: Power vs. Robustness. In C. A. Munoz, V. A. Carreno, & S. Tahar (Eds.),
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
Additional Information Lecture Notes in Computer Science 2410

Files

whisky.ps (222 Kb)
Other

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





Downloadable Citations

;