Getting started

The system is implemented in Prolog and expects commands in the syntactic form of Prolog goals. The list of all the Saturate commands is given here. For proving $\Phi$ in automatic mode enter $\mbox{{\tt prove}}(\Phi)$. The syntax of formulas is explained here.

In semi-automatic mode, or for saturating a consistent theory, the typical interaction cycle with Saturate consists of reading a set of (general) clauses, issuing commands to define the reduction ordering, inference system, redundancy checks, system messages and profiling flags, and, finally, starting the saturation process. If saturation terminates or is interrupted (by typing control-C), proofs of generated clauses can be inspected. Saturated systems of clauses can be filed out for later uses as modules of more complex theories.

Imprint | Data Protection