MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Stuber, Jürgendblp
Editor(s):
Ganzinger, Haralddblp
BibTeX cite key*:
StuberRTA96
Title, Booktitle
Title*:
Superposition Theorem Proving for Abelian Groups Represented as Integer Modules
Booktitle*:
Rewriting Techniques and Applications, 7th International Conference, RTA-96
Event, URLs
Conference URL::
Downloading URL:
Event Address*:
New Brunswick, USA
Language:
English
Event Date*
(no longer used):
July 1996
Organization:
Event Start Date:
19 May 2024
Event End Date:
19 May 2024
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
1103
Number:
Month:
Pages:
33-47
Year*:
1996
VG Wort Pages:
ISBN/ISSN:
3-540-61464-8
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We define a superposition calculus specialized for abelian
groups represented as integer modules, and show its
refutational completeness. This allows to substantially
reduce the number of inferences compared to a standard
superposition prover which applies the axioms directly.
Specifically, equational literals are simplified, so that
only the maximal term of the sums is on the left-hand
side. Only certain minimal superpositions need to be
considered; other superpositions which a standard prover
would consider become redundant. This not only reduces
the number of inferences, but also reduces the size of the
AC-unification problems which are generated. That is,
AC-unification is not necessary at the top of a term, only
below some non-AC-symbol. Further, we consider situations
where the axioms give rise to variable overlaps and
develop techniques to avoid these explosive cases where
possible.
HyperLinks / References / URLs:
http://www.mpi-sb.mpg.de/~juergen/publications/RTA96/
Download
Access Level:

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:
@INPROCEEDINGS{StuberRTA96,
AUTHOR = {Stuber, J{\"u}rgen},
 EDITOR = {Ganzinger, Harald},
 TITLE = {Superposition Theorem Proving for Abelian Groups Represented as Integer Modules},
 BOOKTITLE = {Rewriting Techniques and Applications, 7th International Conference, RTA-96},
 PUBLISHER = {Springer},
 YEAR = {1996},
 VOLUME = {1103},
 PAGES = {33--47},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {New Brunswick, USA},
 ISBN = {3-540-61464-8},
}

Entry last modified by Uwe Brahm, 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)
Jürgen Stuber		Created
03/12/1997 03:29:27 PM
Revisions
4.
3.
2.
1.
0.		Editor(s)
Uwe Brahm
Uwe Brahm
Uwe Brahm
Uwe Brahm
Uwe Brahm		Edit Dates
06.06.97 20:04:37
06.06.97 20:00:58
27.03.97 15:08:31
17.03.97 18:57:56
12/03/97 15:43:22