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

Ganzinger, Harald; McAllester, David; Voronkov, Andrei

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Proceedings

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

MPS-Authors

/persons/resource/persons44474

Ganzinger, Harald
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45678

Voronkov, Andrei
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

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.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-3687-3

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.