Subterm contextual rewriting

Abstract

Sophisticated reductions are an important means to achieve 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 called subterm contextual rewriting 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.