Completion Procedures as Semidecision Procedures

Completion procedures, originated from the seminal work of Knuth and Bendix, are wellknown as procedures for generating confluent rewrite systems, i.e. decision procedures for al theories. In this paper we present a new abstract framework for the utilization of completion procedures as semidecision procedures for theorem proving. The key idea in our approach is that a semidecision process should be target-oriented, i.e. keep into account the target theorem to be proved. For the inference rules of a completion procedure, we present target-oriented schemes of contraction inference rules, i.e. inference rules that delete sentences which are redundant for proving the target. For the search plan, we give a target-oriented, definition of fairness, according to which not all critical pairs need to be considered. We prove that our notion of fairness, together with the refutational completeness of the inference rules, is sufficient for a completion procedure to be a semidecision procedure. By ...

• Type: Conference
• Year: 1990
• Where: CTRS
• Authors: Maria Paola Bonacina, Jieh Hsiang
• Keywords: Completion Procedures, CTRS 1990, CTRS 1992, Decision Procedures, Inference Rules