Max-Planck-Institut für Informatik
max planck institut
informatik
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
Author(s)*:Waldmann, Uwe
BibTeX citekey*:Waldmann1997
Language:English

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


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:http://www.mpi-sb.mpg.de/~uwe/paper/PhD.ps.gz

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

Correlation
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:

@PHDTHESIS{Waldmann1997,
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)

Editor(s)
Uwe Waldmann
Created
01/07/1998 03:43:39 PM
Revision
1.
0.


Editor
Uwe Waldmann
Uwe Waldmann


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