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:

18 September 2019

Event End Date:

18 September 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:




MPG Subunit:


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, 11/07/2006
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
11/07/2006 11:46:09 AM
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