Superposition Theorem Proving for Commutative Algebraic Theories

We develop special superposition calculi for first-order

theorem proving in the theories of abelian groups,
commutative rings, and modules and commutative algebras
over fields or over the ring of integers,
in order to make automated theorem proving in these theories more effective.
The calculi are refutationally complete
on arbitrary sets of ground clauses,
which in particular may contain additional function symbols.

The calculi are derived systematically from a representation
of the theory as a convergent term rewriting system.
Compared to standard superposition they have stronger ordering restrictions
so that inferences are applied only to maximal summands,
and they contain macro inference rules
that use theory axioms in a goal directed fashion.
In general we need additional inferences to handle critical peaks
between extended clauses.
We show that these are not needed for abelian groups and modules,
and that for commutative rings and commutative algebras
one such inference suffices for any pair of ground clauses.
To facilitate the construction of term orderings for such calculi
we introduce theory path orderings.

Theorem Proving, Superposition

MPI Saarbrücken

May

2000

Gert Smolka