Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-97-2-012

Elimination of equality via transformation with ordering constraints

Bachmair, Leo and Ganzinger, Harald and Voronkov, Andrei

MPI-I-97-2-012. December 1997, 18 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:
http://www.mpi-sb.mpg.de/\~{}hg/pra.html\#MPI-I-97-2-012

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-97-2-012.ps313 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1997-2-012
Hide details for BibTeXBibTeX
@TECHREPORT{BachmairGanzingerVoronkov97,
  AUTHOR = {Bachmair, Leo and Ganzinger, Harald and Voronkov, Andrei},
  TITLE = {Elimination of equality via transformation with ordering constraints},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-97-2-012},
  MONTH = {December},
  YEAR = {1997},
  ISSN = {0946-011X},
}