MPI-I-2009-RG1-002

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.