Cancellative abelian monoids in refutational theorem proving

Abstract

We present a constraint superposition calculus in which the axioms of cancellative abelian monoids and, optionally, further axioms (e.g., torsion-freeness) are integrated. Cancellative abelian monoids comprise abelian groups, but also such ubiquitous structures as the natural numbers or multisets. Our calculus requires neither extended clauses nor explicit inferences with the theory axioms. The number of variable overlaps is significantly reduced by strong ordering restrictions and powerful variable elimination techniques; in divisible torsion-free abelian groups, variable overlaps can even be avoided completely. Thanks to the equivalence of torsion-free cancellative and totally ordered abelian monoids, our calculus allows us to solve equational problems in totally ordered abelian monoids without requiring a detour via ordering literals.

Wir stellen einen Constraint-Superpositionskalkül vor, in den die Axiome kürzbarer abelscher Monoide und weitere optionale Axiome (z.B. Torsionsfreiheit) eingebaut sind. Kürzbare abelsche Monoide umfassen abelsche Gruppen, aber auch so allgegenwärtige Strukturen wie die natürlichen Zahlen oder Multisets. Unser Kalkül erfordert weder erweiterte Klauseln noch explizite Interferenzen mit den Theorieaxiomen. Durch verschärfte Ordnungseinschränkungen und leistungsfähige Variableneliminationstechniken erzielen wir eine deutliche Einschränkung von Überlappungen mit Variablen; in dividierbaren torsionsfreien abelschen Gruppen werden Variablenüberlappungen sogar gänzlich überflüssig. Dank der Äquivalenz torsionsfreier kürzbarer und total geordneter abelscher Monoide bietet unser Kalkül die Möglichkeit, Gleichungsprobleme in total geordneten abelschen Monoiden ohne Umweg über Ordnungsliterale zu lösen.