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
To Do List
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.
Feedback on any aspect is also welcome.