International Summer School on Constraints in Computational Logic

Constraints and Theorem Proving

Harald Ganzinger, MPI Saarbrücken, Germany
Robert Nieuwenhuis, Tech. University of Catalonia, Barcelona, Spain

Symbolic constraints provide a convenient way of describing the connection between deduction at the level of ground formulae and the general inferences that are actually applied by a prover on formulae with variables.

For instance, each resolution inference represents infinitely many ground inferences, obtained by substituting ground terms for the variables in the clauses. For refutational completeness only certain restricted cases of ground inferences are required. In the case of ordered resolution, essential ground inferences only resolve maximal literals. On the non-ground level, these ordering restrictions can be represented as a kind of restricted quantification: only ground terms that satisfy the ordering restrictions should be substituted for the variables. This leads us to resolution calculi with order-constrained clauses, where in each inference the conclusion is restricted by the ordering constraints of the current deduction step, combined with the constraints that are already present in the premises. Clauses with unsatisfiable constraints represent no ground clauses and can hence be removed during the deduction process, thus pruning the search space.

In our lectures we will mainly focus on saturation-based theorem proving methods including resolution, superposition and chaining. In this context, apart from ordering restrictions, constraints are also used to describe unification problems and certain irreducibility properties of terms. The course will consist of three main parts.

First we will introduce the main concepts for the case of pure equational logic, where rewriting and Knuth/Bendix completion are fundamental deduction methods. The topics covered will include Birkhoff's theorem, first-order vs. inductive consequences, term rewrite systems, confluence, termination, orderings, critical pair computation (i.e., ordered paramodulation and superposition), and completion with simplification (i.e., theorem proving procedures with redundancy criteria). Here, as well as in the remaining part of our lectures, all concepts will be illustrated by examples run on-line with the Saturate prover.

In the second part, we will extend these ideas to saturation-based methods for general first-order clauses, including superposition and chaining-based inference systems, completeness proofs by means of the model generation method, an abstract notion of redundancy for inferences, and concrete medoths for redundancy elimination.

The third part we will cover several extensions, with special attention to those aspects for which constraints play an important role, like basic strategies, deduction modulo equational theories, constraint-based redundancy methods, and deduction-based complexity analysis and decision procedures.


ccl99@lri.fr
CCL'99 main page
Last change: April 8, 1999.