Introduction

This document describes the commands available in the theorem prover Ergo. It assumes that the reader is familiar, to some extent, with Ergo (refer to the online tutorials). As such, it is intended to serve as a reference only.

Ergo is a generalised Sequent Calculus theorem prover designed and implemented at the Software Verification Research Centre at the University of Queensland.

The architecture of Ergo is based on the following layered design.

The proof engine forms the core of Ergo. The theory database is Ergo's repository of information containing object logics. The next layer contains tactics (user-writable code written in Qu-Prolog) that implement the command-line interface. This layer constructs the theory database and controls the proof engine. Finally, the user front-end (Emacs) communicates with Ergo via tactic interfaces.

The commands available in Ergo depend upon the user interface and theory being used: the default gumtree proof interface, constructing theories, or the higher level Ergo-Emacs interface.

Every Ergo command has a declaration that gives the command's name, the types and modes of its arguments, the interface from which it is available and a description of the command. The textual descriptors for each command can be extended with concept nodes.

Concept nodes describe groups of commands or other general concepts and are linked into a network by cross-references. They allow the automatic generation of on-line help.

In addition to the commands supplied by each user interface, there are also a number of general commands (available from all user interfaces). These allow users to inspect the ergo database, obtain help and so on.