We discuss the conditional rewriting aspects of the Focus program transformation/synthesis system. The term-rewriting induction principle, presented earlier for unconditional rewrite systems, is generalized for conditional systems. We also present a novel deduction method for first-order clauses called contextual deduction which may be considered to be the first-order analogue of the rewriting operation. Like rewriting, contextual deduction uses pattern matching instead of unification and has the property of finite termination. We identify a sufficient condition for clausal theories, called saturation, under which contextual deduction is complete for refuting ground goal clauses.
CITATION STYLE
Bronsard, F., & Reddy, U. S. (1991). Conditional rewriting in focus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 516 LNCS, pp. 2–13). Springer Verlag. https://doi.org/10.1007/3-540-54317-1_77
Mendeley helps you to discover research relevant for your work.