A Tactic Language for Ergo
Andrew Martin, R. Nickson, Mark Utting · ePrints Soton (University of Southampton) · 1997
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. 1 Introduction Ergo is an interactive proof tool that has been designed and implemented at the SVRC over the last ten years. It is implemented in Qu-Prolog (Robinson and Hagen, 1997), and is designed to be extensible, so that users can add new theories, tactics and user interfaces. Ergo 5 is currently under development. Having no inbuilt object logic, it is a generic prover that can be instantiated by providing a collection of axiomatic and/or definitional theories. The core of Ergo 5 provides support for (uninterpreted) sequents with named tuples of arbitrary terms as antecedents and single terms as consequents...