Superposition theorem proving for commutative algebraic theories

Abstract

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.

Wir entwickeln in dieser Arbeit spezielle Superpositionskalküle für die Theorien der Abelschen Gruppen, der kommutativen Ringe, und der Moduln und kommutativen Algebren über Körpern und den ganzen Zahlen, mit dem Ziel das automatische Theorembeweisen in Logik erster Stufe für diese Theorien effektiver zu machen. Die Kalküle sind widerlegungsvollständig für beliebige Mengen von Grundklauseln, in denen insbesondere auch beliebige, nicht in der Theorie auftretende, Funktionssymbole vorkommen dürfen. Die Kalküle entwickeln wir systematisch aus einer Darstellung der Theorien als konvergente Termersetzungssysteme. Im Vergleich zu Standardsuperposition haben sie stärkere Ordnungseinschränkungen, so daß Interferenzen nur noch auf maximale Summanden angewendet werden müssen, und sie enthalten Makroinferenzregeln, die Theorieaxiome in zielgerichteter Weise anwenden. Im allgemeinen benötigen wir weiterhin Interferenzen, um kritische Paare zwischen erweiterten Klauseln zu behandeln. Wir zeigen, dass diese für Abelsche Gruppen und Moduln nicht nötig sind, und daß für kommutative Ringe und Algebren eine Interferenz für jedes Paar von Grundklauseln genügt. Um die Konstruktion von Termordnungen für unsere Kalküle zu vereinfachen, führen wir den Begriff der Theoriepfadordnung ein.