Building abelian groups and commutative rings into first-order theorem proving

Jürgen Stuber

Date: July 17th (Wednesday)
Time: ??.??
Abstract
For many theories from algebra there exist convergent term rewriting systems, possibly modulo some equational theory. We present a technique to build such a theory into ordering-restricted first-order clausal theorem proving. In this way one obtains a refutationally complete inference system which creates a smaller search space than by directly applying a more general prover to the axioms of the theory.

Specifically, on the ground level equational literals are simplified, until they are in a sufficiently simplified form. For each of these forms one derives a symmetrization, that is a set of rules such that critical pairs with the theory converge. One then considers overlaps between symmetrizations. Since their structure is know, one can exploit this by showing that only a few critical pairs need to be tested to obtain convergence.

To lift this to the non-ground level, each step of the simplification becomes an inference. These are either carefully controlled superpositions with theory axioms or derived inferences like cancellation. Then, for inferences between sufficiently simplified non-theory clauses, one distinguished between overlaps of two extended rules and overlaps where at least one rule is not extended. The former correspond to the critical pairs obtained above; the latter are similar to superposition inferences, except that they take the extended rules in the symmetrization into account.

The technique is quite general, but it seems most useful for theories which have abelian groups as a subtheory. In that case a single term of a sum can be isolated on the left-hand side. The inference systems obtained are extensions of the corresponding Gröbner base algorithms.

______________
__________________________________________

Previous page RISC SWP Linz Austria