Peter J. Robinson
Abstract
Ergo is an interactive theorem prover based on a generalised sequent calculus. Users are able to declare theories, carry out proofs, query the theory database and define their own tactics and interfaces.
Users can write tactics and interfaces in Qu-Prolog, which is the implementation language for Ergo, and can also write tactics in the Gumtree tactic language.
