Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25751
Titel: Cancellative abelian monoids in refutational theorem proving
Verfasser: Waldmann, Uwe
Sprache: Englisch
Erscheinungsjahr: 1997
SWD-Schlagwörter: Automatisches Beweisverfahren ; Superpositionskalkül ; Kürzbares Monoid ; Abelsche Gruppe ; Widerlegungsvollständigkeit
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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 zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-2431
hdl:20.500.11880/25807
http://dx.doi.org/10.22028/D291-25751
Erstgutachter: Harald Ganzinger
Tag der mündlichen Prüfung: 28-Jul-1997
SciDok-Publikation: 17-Mai-2004
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
UweWaldmann_ProfDrHaraldGanzinger.pdf1,4 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.