Ergo Home Page

Ergo is a generic sequent calculus based prover designed and implemented at Information Technology and Electrical Engineering, The University of Queensland.

Ergo has the following main features.


Documentation



Downloads

Ergo runs on Linux and Unix machines.

Before downloading Ergo you need to first download and build Qu-Prolog.

To Do List

Our short-term list of things to do include the following.


Implementation Overview

Ergo is implemented in Qu-Prolog and takes a two-layer approach to prevent users and tactics from carrying out unsound steps. The inner layer (ther Ergo kernel) is responsible for managing proofs and the theory database. The theory database stores information about the theories: axioms, definitions, symbol declarations, theory inheritence, etc..  Each theorem is stored in the database as a postulate until proved, at which point the database changes to reflect this - storing information about what theorems were used in its proof. This information is used in other proofs to avoid circular reasoning. Users can only modify this database by theory declaration and as a result of completing proofs.

The proof engine is the other part of the Ergo kernel. The proof engine constructs a proof tree and users can interact with the proof tree only via predefined methods of the proof engine. Users extend the proof tree by using the method that applies a rule. The engine looks up the rule in the database, determines if the rule is applicable, and if so applies the rule, modifying the proof tree. Other methods extract information from the proof tree: what the open nodes are, what the proofs constraints are, etc.

The outer layer is where user interfaces and tactics live. Users are free to write and use their own interfaces and tactics without fear of producing unsound inferences. As an example at this level, Ergo comes with the predefined Gumtree proof interface and tactic language.

The implementation contains several "hooks" which allow users to modify the behaviour of some (non-critical) parts of the system. For example, the implementation allows "documentation nodes" to be attached to code. This documentation is added to the database. Users are able to use a hook to determine how this documentation is to be displayed. In the emacs interface, a predefined hook causes the documentation to be displayed as hypertext within emacs. Another hook causes the documentation to be translated into latex form, and yet another causes the documentation to be translated to HTML form. The system makefile uses the last two hooks to produce both a latex and HTML reference manual.


Ergo History

The original Ergo (Ergo4) was a prover based directly on window inference. The main drawback of Ergo4 was that the window opening rules were all primitive (and quite complex) - they could not be proved within Ergo4. It was therefore very difficult to see what the "real" axioms of a given theory were.

The current Ergo, on the other hand, is a Sequent Calculus prover and so these problems do not arise. It is still possible to carry out window inference within Ergo by using the supplied window inference tactics and supporting rules. In Ergo, the opening rules are much simpler than in Ergo4 and all the "work" of opening a window is done by tactics (that use combinations of rules) rather than using one complicated opening rule as was done in Ergo4. This means that rules related to window inference are just like any other rules and so it is clear exactly what the axioms of any given theory are.

The initial population of the Ergo theories was done by translating the Ergo4 theories and proofs into the required form, rebuilding the theories, and rerunning the translated proofs.

Recently,  ZFC set theory, a natural numbers theory and an integers theory were completely redone from scratch.



For more information about Ergo, contact the Peter Robinson at: pjr@itee.uq.edu.au.

Feedback on any aspect is also welcome.