English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
  Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups

Waldmann, U. (1999). Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups. In H. Ganzinger, D. McAllester, & A. Voronkov (Eds.), Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99) (pp. 131-147). Berlin, Germany: Springer.

Item is

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Waldmann, Uwe1, 2, Author           
Affiliations:
1Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              
2Programming 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: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519859
Other: Local-ID: C1256104005ECAFC-23C6035327C8D0DAC12567EC005AE4FE-Waldmann1999LPAR
 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: Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning (LPAR-99)
Source Genre: Proceedings
 Creator(s):
Ganzinger, Harald1, Editor           
McAllester, David, Editor
Voronkov, Andrei1, Editor           
Affiliations:
1 Programming Logics, MPI for Informatics, Max Planck Society, ou_40045            
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 131 - 147 Identifier: ISBN: 3-540-66492-0

Source 2

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