Proceedings Volume
@Proceedings
Tagungsband, Workshopband


Show entries of:

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

Action:

login to update

Options:








Author, Editor

Editor(s):

Ganzinger, Harald
McAllester, David
Voronkov, Andrei

dblp
dblp
dblp



BibTeX citekey*:

Ganzinger1999LPAR

Language:

English

Title, Conference

Title*:

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



Event Address*:

Tbilisi, Georgia

Conference URL:

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

Event Start Date:

17 September 2019

Event End Date:

17 September 2019

Event Date*
(no longer used):

September, 6-10

Organization:


Publisher

Name*:

Springer

Publisher's URL:






Address*:

Berlin, Germany

Publishing Year*:

1999

Vol, No, pp., Year

Series:

Lecture Notes in Artificial Intelligence

Volume:

1705

Number:


Month:


Pages*:

397

ISBN:

3-540-66492-0

VG Wort Pages:


ISSN:




Abstract, Links, ©

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.

Categories / Keywords:

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

HyperLinks / References / URLs:


Copyright Message:


Personal Comments:


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:

@PROCEEDINGS{Ganzinger1999LPAR,
EDITOR = {Ganzinger, Harald and McAllester, David and Voronkov, Andrei},
TITLE = {Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99)},
PUBLISHER = {Springer},
YEAR = {1999},
VOLUME = {1705},
PAGES = {397},
SERIES = {Lecture Notes in Artificial Intelligence},
ADDRESS = {Tbilisi, Georgia},
ISBN = {3-540-66492-0},
}


Entry last modified by Christine Kiesel, 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
02/22/2000 01:20:37 PM
Revisions
11.
10.
9.
8.
7.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Uwe Brahm
Uwe Brahm
Edit Dates
26.01.2001 03:08:34 PM
25.01.2001 04:04:20 PM
30/03/2000 17:06:31
28.03.2000 10:40:56
23/02/2000 10:05:53