MPI-INF/SWS Research Reports 1991-2021

2. Number - only RG1


Contextual rewriting

Wischnewski, Patrick and Weidenbach, Christoph

April 2009, 28 pages.

Status: available - back from printing

Sophisticated reductions are of particular importance for progress in automated theorem proving. We consider the powerful reduction rule Contextual Rewriting in connection with the superposition calculus. If considered in its most general form the applicability of contextual rewriting is not decidable. We develop an instance of contextual rewriting where applicability becomes decidable while preserving a great deal of its simplification power. A sophisticated implementation of the rule in SPASS reveals its application potential. Our contextual rewriting instance is feasible in the sense that it can be executed on the overall TPTP resulting in a gain of solved problems and new solutions to a number of problems that could not be solved by theorem provers so far.

  • MPI-I-2009-RG1-002.pdf
  • Attachement: MPI-I-2009-RG1-002.pdf (283 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Wischnewski, Patrick and Weidenbach, Christoph},
  TITLE = {Contextual rewriting},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-2009-RG1-002},
  MONTH = {April},
  YEAR = {2009},
  ISSN = {0946-011X},