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

- Ergo6.3 reference manual - refman.ps (300K) and refman.html
- An Ergo tutorial slide show (use acroread) notes.pdf

Downloads

Before downloading

- The current release of Ergo: ergo6.4.tar.gz (2.1M)
- An Ergo interface GUI based on the Qt library: xergo1.0.tgz (41K)

**To Do List
**

- 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
**

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.