非表示:
キーワード:
-
要旨:
We refine Brand's method for eliminating equality axioms by
(i)
imposingeordering 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.
