Completion procedures, originated from the seminal work of Knuth and Bendix, are well-known as procedures for generating confluent rewrite systems, i.e. decision procedures for equational 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 relaxing the requirement of considering all critical pairs, our target-oriented framework should be more suitable for designing efficient procedures for theorem proving. The generation of decision procedures is included as a special side-effect and all the results of the classical approach to completion are re-obtained in our framework. The application of completion to disprove inductive conjectures, i.e. the so called inductionless induction method, is also covered as a semidecision process. Finally, we present according to our framework, some equational completion procedures based on Unfailing Knuth-Bendix completion.

Towards a foundation of completion procedures as semidecision procedures

BONACINA, Maria Paola
;
1995-01-01

Abstract

Completion procedures, originated from the seminal work of Knuth and Bendix, are well-known as procedures for generating confluent rewrite systems, i.e. decision procedures for equational 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 relaxing the requirement of considering all critical pairs, our target-oriented framework should be more suitable for designing efficient procedures for theorem proving. The generation of decision procedures is included as a special side-effect and all the results of the classical approach to completion are re-obtained in our framework. The application of completion to disprove inductive conjectures, i.e. the so called inductionless induction method, is also covered as a semidecision process. Finally, we present according to our framework, some equational completion procedures based on Unfailing Knuth-Bendix completion.
1995
Automated theorem proving; term rewriting; completion-based theorem proving; Knuth-Bendix completion; equational reasoning
File in questo prodotto:
File Dimensione Formato  
TCS1995completion.pdf

accesso aperto

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 386.77 kB
Formato Adobe PDF
386.77 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/300536
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 27
  • ???jsp.display-item.citation.isi??? 21
social impact