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: | Dissertation |
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 | Size | Format | |
---|---|---|---|---|
UweWaldmann_ProfDrHaraldGanzinger.pdf | 1,4 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.