A Tactic Language for Ergo
A. Martin‚ R. Nickson and M. Utting
Abstract
A new version of the Ergo theorem prover is under development. It uses a single tactic language, based on Angel, for tactic programming, user interface, and proof representation. This paper describes the language as it is used in each of these cases, and explains the details of its implementation in Qu-Prolog. An example from classical propositional calculus is included.
Details
| Address |
Singapore |
| Book Title |
Formal Methods Pacific '97 |
| Editor |
Lindsay Groves and Steve Reeves |
| ISBN |
981−3083−31−X |
| Keywords |
tactics‚user interface |
| Month |
jul |
| Note |
Also appears as TR97−16‚ Software Verification Research Centre‚ The University of Queensland‚ QLD 4072‚ Australia |
| Publisher |
Springer−Verlag |
| Series |
Springer Series in Discrete Mathematics and Theoretical Computer Science |
| Year |
1997 |
Links
Related pages
|
People |