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 one 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 also show some dramatic improvements of the proof search in model elimination
theorem proving. 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.
|
Year | DOI | Venue |
---|---|---|
1998 | 10.1007/BFb0054259 | CADE |
Keywords | Field | DocType |
ordering constraints | Model elimination,Discrete mathematics,Constraint satisfaction,Open problem,Axiom,Computer science,Automated theorem proving,Satisfiability,Correctness,Algorithm,Gas meter prover | Conference |
ISBN | Citations | PageRank |
3-540-64675-2 | 12 | 0.66 |
References | Authors | |
7 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Leo Bachmair | 1 | 1006 | 90.72 |
Harald Ganzinger | 2 | 1513 | 155.21 |
Andrei Voronkov | 3 | 2670 | 225.46 |