Please use this identifier to cite or link to this item: doi:10.22028/D291-25751
Title: Cancellative abelian monoids in refutational theorem proving
Author(s): Waldmann, Uwe
Language: English
Year of Publication: 1997
SWD key words: Automatisches Beweisverfahren ; Superpositionskalkül ; Kürzbares Monoid ; Abelsche Gruppe ; Widerlegungsvollständigkeit
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
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.
Link to this record: urn:nbn:de:bsz:291-scidok-2431
hdl:20.500.11880/25807
http://dx.doi.org/10.22028/D291-25751
Advisor: Harald Ganzinger
Date of oral examination: 28-Jul-1997
Date of registration: 17-May-2004
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
UweWaldmann_ProfDrHaraldGanzinger.pdf1,4 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.