Loading...
Please wait, while we are loading the content...
Similar Documents
A Tactic Language for Ergo (1997)
| Content Provider | CiteSeerX |
|---|---|
| Author | Martin, Andrew Nickson, Ray Utting, Mark |
| Description | 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... |
| File Format | |
| Language | English |
| Publisher | Springer-Verlag |
| Publisher Date | 1997-01-01 |
| Publisher Institution | Formal Methods Pacific ’97 |
| Access Restriction | Open |
| Subject Keyword | Tactic Language Introduction Ergo Proof Representation Interactive Proof Tool User Interface Ergo Theorem Prover Tactic Programming Last Ten Year Inbuilt Object Logic Single Term Arbitrary Term Classical Propositional Calculus New Version Named Tuples Single Tactic Language New Theory Generic Prover Definitional Theory |
| Content Type | Text |
| Resource Type | Article |
