English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
 Local TagsRelease HistoryDetailsSummary
  Elimination of Equality via Transformation with Ordering Constraints

Bachmair, L., Ganzinger, H., & Voronkov, A. (1998). Elimination of Equality via Transformation with Ordering Constraints. In C. Kirchner, & H. Kirchner (Eds.), Proceedings of the 15th International Conference on Automated Deduction (CADE-98) (pp. 175-190). Berlin, Germany: Springer.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-382F-0 Version Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-3831-8
Genre: Conference Paper

Files

show Files

Locators

show

Creators

show
hide
 Creators:
Bachmair, Leo1, Author           
Ganzinger, Harald1, Author           
Voronkov, Andrei1, Author           
Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045              

Content

show
hide
Free keywords: -
 Abstract: We refine Brand's method for eliminating equality axioms by (i) imposing ordering constraints on auxiliary variables introduced during the transformation process and (ii) avoiding certain transformations of positive equations with a variable on the right-hand side. The refinements are both of theoretical and practical interest. For instance, the second refinement is implemented in Setheo and appears to be critical for that prover's performance on equational problems. The correctness of this variant of Brand's method was an open problem that is solved by the more general results in the present paper. The experimental results we obtained from a prototype implementation of our proposed method for the model elimination prover Protein also show some dramatic improvements of the proof search. Ordering constraints have already been widely used in equational theorem provers based on paramodulation. We prove the correctness of our refinements of Brand's method by establishing a suitable connection to basic paramodulation calculi and thereby shed new light on the connection between different approaches to equational theorem proving.

Details

show
hide
Language(s): eng - English
 Dates: 2010-03-121998
 Publication Status: Issued
 Pages: -
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: eDoc: 519695
Other: Local-ID: C1256104005ECAFC-017F31F75109D91DC1256744004C11FA-BachmairGanzingerVoronkov-98-cade
 Degree: -

Event

show
hide
Title: Untitled Event
Place of Event: Lindau, Germany
Start-/End Date: 1998

Legal Case

show

Project information

show

Source 1

show
hide
Title: Proceedings of the 15th International Conference on Automated Deduction (CADE-98)
Source Genre: Proceedings
 Creator(s):
Kirchner, Claude, Editor
Kirchner, Hélène, Editor
Affiliations:
-
Publ. Info: Berlin, Germany : Springer
Pages: - Volume / Issue: - Sequence Number: - Start / End Page: 175 - 190 Identifier: ISBN: 3-540-64675-2

Source 2

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