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

Publications Master Template :: Thesis :: Stuber, Jürgen


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)*:Stuber, Jürgen
BibTeX citekey*:Stuber1999
Language:English

Title, School
Title*:Superposition Theorem Proving for Commutative Algebraic Theories
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation
Month:December
Year:1999


Note, Abstract, Copyright
LaTeX Abstract:We develop special superposition calculi for first-order

theorem proving in the theories of abelian groups,
commutative rings, and modules and commutative algebras
over fields or over the ring of integers,
in order to make automated theorem proving in these theories more effective.
The calculi are refutationally complete
on arbitrary sets of ground clauses,
which in particular may contain additional function symbols.

The calculi are derived systematically from a representation
of the theory as a convergent term rewriting system.
Compared to standard superposition they have stronger ordering restrictions
so that inferences are applied only to maximal summands,
and they contain macro inference rules
that use theory axioms in a goal directed fashion.
In general we need additional inferences to handle critical peaks
between extended clauses.
We show that these are not needed for abelian groups and modules,
and that for commutative rings and commutative algebras
one such inference suffices for any pair of ground clauses.
To facilitate the construction of term orderings for such calculi
we introduce theory path orderings.

Keywords:Theorem Proving, Superposition
HyperLinks / References / URLs:http://www.mpi-sb.mpg.de/~juergen/publications/Stuber1999Diss.html
Download Access Level:Public
Download File(s):View attachments here:

Referees, Status, Dates
1. Referee:Harald Ganzinger
2. Referee:Christopher Lynch
Supervisor:Harald Ganzinger
Status:Completed
Location of Lecture:MPI Saarbrücken
Date Kolloquium:25 May 2000
Chair Kolloquium:Gert Smolka

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


BibTeX Entry:
@PHDTHESIS{Stuber1999,
AUTHOR = {Stuber, J{\"u}rgen},
TITLE = {Superposition Theorem Proving for Commutative Algebraic Theories},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {1999},
TYPE = {Doctoral dissertation}
MONTH = {December},
}





Entry last modified by Anja Becker, 07/08/2011
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)
Jürgen Stuber
Created
09/05/2000 12:01:50 PM
Revisions
6.
5.
4.
3.
2.
Editor(s)
Anja Becker
Uwe Brahm
Uwe Brahm
Uwe Brahm
Uwe Brahm
Edit Dates
08.07.2011 13:47:11
2007-07-02 11:09:53
2007-07-02 11:09:13
2007-07-02 10:57:54
2007-07-02 10:57:34