Subterm contextual rewriting
Christoph Weidenbach, Patrick Wischnewski · AI Communications · 2010
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 a