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.

  • Genericity (supports modal and classical logics).
  • Support for schematic rules and answer extraction.
  • A query language for searching for rules.
  • The use of a high level logic programming language, Qu-Prolog for writing user tactics and prover extensions.
  • A pre-defined Gumtree proof interface and tactic language.
  • A Gumtree compiler that translates Gumtree tactics into Qu-Prolog code, optimizes this code using partial evaluation, and compiles this into Qu-Prolog object code.
  • Many tactics that encode common proof patterns.
  • Window inference support as Gumtree tactics and supporting rules.
  • A simple Emacs graphical user interface.
  • Support for storing, browsing and replaying proofs.
  • Sophisticated theory construction facilities, including theory interpretation.
  • Separate name space and syntax for each theory.
  • A large library of standard theories. Currently, this library contains about 50 theories and nearly 1500 theorems (derived inference rules).
  • An online hypertext help system (emacs).
  • An interactive introduction to Ergo using the Emacs interface

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.

  • We have discovered a semantic problem with using multiple contexts that we intend to address shortly. The supplied theories use only the single (hyp) context and so the problem does not arise in those theories. The problem would arise, however if a user declared and used their own context.
  • Flesh out a theory of sets to support B and add theories about finite sets, sequences and bags (mostly done).
  • Use the fixed point theory and the ZFC set theory to interpret the naturals theory.

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.

On This Site