Overview

The Saturate system is an experimental automated theorem prover for first-order logic primarily based on saturation up to redundancy. The theoretical basis of Saturate are rewrite techniques for transitive relations as described in (Bachmair & Ganzinger, 1994 c) and (Bachmair & Ganzinger, 1995 b). Clausal normal form transformation is integrated into Saturate in an attempt to keep the logical structure, in particular quantifiers and equivalences, visible. The system is written in Prolog and runs under Quintus and SICStus.

Saturate is a cooperation project between UPC Barcelona and MPI Informatik within the ESPRIT Basic Research Working Groups CCL and CCL II.

The main focus of the system is on

• the efficient treatment of transitive relations by term rewrite techniques, and on
• the global restriction of the search space in saturation-based theorem proving by applying techniques for detecting redundancy of clauses and inferences.

Moreover, Saturate

• integrates a set of inference rules that are derived from the sequent calculus into saturation so as to not prematurely eliminate quaintifiers and other logical structure;
• provides methods for translating modal logics into first-order logic based on various semantic embeddings into Kripke structures, and
• supports AC-operators by providing AC-unification, AC-matching, AC-extensions of equalities, and AC-compatible orderings as a basis for a future integration of specific algebraic methods for theories such as abelian groups, rings and fields.

There are three basic kinds of problems for which Saturate can be used:

• for refutational theorem proving
• for the finite saturation of a consistent theory, and
• for finding complexity bounds for decidable theories.

This manual is also available as a Postscript file.

Imprint | Data Protection