Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Waldmann, Uwe

dblp



Editor(s):

Ganzinger, Harald
McAllester, David
Voronkov, Andrei

dblp
dblp
dblp



BibTeX cite key*:

Waldmann1999LPAR

Title, Booktitle

Title*:

Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups

Booktitle*:

Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99)

Event, URLs

URL of the conference:

http://www.csd.uu.se/~voronkov/lpar99.html

URL for downloading the paper:


Event Address*:

Tbilisi, Georgia

Language:

English

Event Date*
(no longer used):

September 6-10

Organization:


Event Start Date:

15 October 2019

Event End Date:

15 October 2019

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Artificial Intelligence

Volume:

1705

Number:


Month:


Pages:

131-147

Year*:

1999

VG Wort Pages:


ISBN/ISSN:

3-540-66492-0

Sequence Number:


DOI:




Note, Abstract, ©

Note:

%Earlier version: Technical Report MPI-I-1999-2-003, Max-Planck-Institut für Informatik, Saarbrücken

(LaTeX) Abstract:

In divisible torsion-free abelian groups, the efficiency of the cancellative superposition calculus can be greatly increased by combining it with a variable elimination algorithm that transforms every clause into an equivalent clause without unshielded variables. We show that the resulting calculus is not only refutationally complete (even in the presence of arbitrary free function symbols), but that it is also a decision procedure for the theory of divisible torsion-free abelian groups.

Keywords:

refutational theorem proving, first-order logic, superposition, cancellative abelian monoids, variable elimination, divisible torsion-free abelian groups, algebra, decision problem



Download
Access Level:


Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

experts only

Appearance:

MPII WWW Server, university publications list, CCL bibliography, MPII FTP Server, working group publication list, MPG publications list, Fachbeirat



BibTeX Entry:

@INPROCEEDINGS{Waldmann1999LPAR,
AUTHOR = {Waldmann, Uwe},
EDITOR = {Ganzinger, Harald and McAllester, David and Voronkov, Andrei},
TITLE = {Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups},
BOOKTITLE = {Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99)},
PUBLISHER = {Springer},
YEAR = {1999},
VOLUME = {1705},
PAGES = {131--147},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Tbilisi, Georgia},
ISBN = {3-540-66492-0},
}


Entry last modified by Manfred Jaeger, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
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
09/14/1999 06:32:48 PM
Revisions
2.
1.
0.

Editor(s)
Manfred Jaeger
Uwe Brahm
Uwe Waldmann

Edit Dates
31/08/2001 18:32:29
28.03.2000 10:41:30
09/14/99 06:32:48 PM