In this paper we give a new abstract framework for the study of Knuth-Bendix type completion procedures, which are regarded as semidecision procedures for theorem proving. First, we extend the classical proof ordering approach started by Bachmair-Dershowitz-Hsiang in such a way that proofs of different theorems can also be compared. This is necessary for the application of proof orderings to theorem proving derivations. We use proof orderings to uniformly define all the fundamental concepts in terms of proof reduction. A completion procedure is given by a set of inference rules and a search plan. The inference rules determine what can be derived from given data. The search plan chooses at each step of the derivation which inference rule to apply to which data. Each inference step either reduces the proof of a theorem or deletes a redundant sentence. Our definition of redundancy is based on the assumed proof ordering. We have shown in a related paper that our definition subsumes those given by Kounalis-Rusinowitch and Bachmair-Ganzinger. We prove that if the inference rules are refutationally complete and the search plan is fair, a completion procedure is a semidecision procedure for theorem proving. The key part of this result is the notion of fairness. Our definition of fairness is the first definition of fairness for completion procedures which addresses the theorem proving problem. It is new in three ways: it is target-oriented, that is it keeps the theorem to be proved into consideration, it is explicitly stated as a property of the search plan and it is defined in terms of proof reduction, so that expansion inferences and contraction inferences are treated uniformly. According to this definition of fairness, it is not necessary to consider all critical pairs in a derivation for the derivation to be fair. This is because not all critical pairs are necessary to prove a given theorem. Considering all critical pairs is an unnecessary source of inefficiency in a theorem proving derivation. We also show that the process of disproving inductive theorems by the so called inductionless induction method is a semidecision process. Finally, we present according to our framework, some equational completion procedures based on Unfailing Knuth-Bendix completion.

Completion procedures as semidecision procedures

BONACINA, Maria Paola
;
1991-01-01

Abstract

In this paper we give a new abstract framework for the study of Knuth-Bendix type completion procedures, which are regarded as semidecision procedures for theorem proving. First, we extend the classical proof ordering approach started by Bachmair-Dershowitz-Hsiang in such a way that proofs of different theorems can also be compared. This is necessary for the application of proof orderings to theorem proving derivations. We use proof orderings to uniformly define all the fundamental concepts in terms of proof reduction. A completion procedure is given by a set of inference rules and a search plan. The inference rules determine what can be derived from given data. The search plan chooses at each step of the derivation which inference rule to apply to which data. Each inference step either reduces the proof of a theorem or deletes a redundant sentence. Our definition of redundancy is based on the assumed proof ordering. We have shown in a related paper that our definition subsumes those given by Kounalis-Rusinowitch and Bachmair-Ganzinger. We prove that if the inference rules are refutationally complete and the search plan is fair, a completion procedure is a semidecision procedure for theorem proving. The key part of this result is the notion of fairness. Our definition of fairness is the first definition of fairness for completion procedures which addresses the theorem proving problem. It is new in three ways: it is target-oriented, that is it keeps the theorem to be proved into consideration, it is explicitly stated as a property of the search plan and it is defined in terms of proof reduction, so that expansion inferences and contraction inferences are treated uniformly. According to this definition of fairness, it is not necessary to consider all critical pairs in a derivation for the derivation to be fair. This is because not all critical pairs are necessary to prove a given theorem. Considering all critical pairs is an unnecessary source of inefficiency in a theorem proving derivation. We also show that the process of disproving inductive theorems by the so called inductionless induction method is a semidecision process. Finally, we present according to our framework, some equational completion procedures based on Unfailing Knuth-Bendix completion.
1991
9783540543176
Completion procedures, Knuth-Bendix completion, proof orderings, superposition, redundancy, target-oriented completion, goal-sensitive theorem proving
File in questo prodotto:
File Dimensione Formato  
CTRS1990completion.pdf

accesso aperto

Descrizione: Articolo
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 355.33 kB
Formato Adobe PDF
355.33 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/16059
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 5
  • ???jsp.display-item.citation.isi??? 0
social impact