Conditional rewriting in focus

Abstract

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.