CONTEXTUAL REWRITING IN AUTOMATED REASONING

Article type: Research Article

Authors: Zhang, Hantao

Affiliations: Department of Computer Science, The University of Iowa, Iowa City, IA 52242, [email protected]

Note: [] Partially supported by the National Science Foundation under Giants CCR-9202838 and CCR-9357851.

Abstract: Contextual rewriting as a generalization of conditional rewriting has been found in different forms in the papers whose major subject is not contextual rewriting. Here, we put the scattered information together and give it a systematic study. Among various properties of contextual rewriting, we show that contextual rewriting is a powerful simplification rule for the first-order theorem proving with equality and preserves the refutational completeness of many reasoning systems. We compare definitions of contextual rewriting by Boyer-Moore, Rémy, Zhang-Rémy, Ganzinger, Zhang-Kapur, and Bouhoula-Rusinowitch in regard to its efficiency and power. We provide a detailed procedure for simplifying clauses using contextual rewriting and a solution on how to handle variables which appear only in the condition of a conditional rewrite rule.

DOI: 10.3233/FI-1995-24125

Journal: Fundamenta Informaticae, vol. 24, no. 1-2, pp. 107-123, 1995