English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

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

Ganzinger, H., McAllester, D., & Voronkov, A. (Eds.). (1999). Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Ganzinger, Harald1, Editor           
McAllester, David, Editor
Voronkov, Andrei1, Editor           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 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.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121999
 Publication Status: Issued
 Pages: 397
 Publishing info: Berlin, Germany : Springer
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519755
ISBN: 3-540-66492-0
Other: Local-ID: C1256104005ECAFC-47D6A4FD814DA9E3C125688D0043CE50-Ganzinger1999LPAR
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Tbilisi, Georgia
Start-/End Date: 1999

Legal Case

show

Project information

show

Source 1

show
hide
Title: Lecture Notes in Computer Science
Source Genre: Series
 Creator(s):
Affiliations:
Publ. Info: -
Pages: - Volume / Issue: 1705 Sequence Number: - Start / End Page: - Identifier: -