Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

Publications Master Template :: Thesis :: Waldmann, Uwe

Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit

Author(s)*:Waldmann, Uwe
BibTeX citekey*:Waldmann1997

Title, School
Title*:Cancellative Abelian Monoids in Refutational Theorem Proving
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation

Note, Abstract, Copyright
LaTeX 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.
Keywords:first-order theorem proving, paramodulation, superposition, algebra
HyperLinks / References / URLs:

Referees, Status, Dates
1. Referee:Harald Ganzinger
2. Referee:Michaël Rusinowitch
Supervisor:Harald Ganzinger
Date Kolloquium:28 July 1997
Chair Kolloquium:Jörg Siekmann

MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:experts only
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography

BibTeX Entry:

AUTHOR = {Waldmann, Uwe},
TITLE = {Cancellative Abelian Monoids in Refutational Theorem Proving},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {1997},
TYPE = {Doctoral dissertation}
MONTH = {July},

Entry last modified by Uwe Waldmann, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Uwe Waldmann
01/07/1998 03:43:39 PM

Uwe Waldmann
Uwe Waldmann

Edit Date
27/07/98 23:12:53
07/01/98 15:43:39