Reducing redundancy in search has been a major concern for automated deduction. Subgoal-reduction strategies, such as those based on model elimination and implemented in Prolog technology theorem provers, prevent redundant search by using lemmaizing and caching, whereas contraction-based strategies prevent redundant search by using contraction rules, such as subsumption. In this work we show that lemmaizing and contraction can coexist in the framework of semantic resolution. On the lemmaizing side, we define two meta-level inference rules for lemmaizing in semantic resolution, one producing unit lemmas and one producing non-unit lemmas, and we prove their soundness. Rules for lemmaizing are meta-rules because they use global knowledge about the derivation, e.g. ancestry relations, in order to derive lemmas. Our meta-rules for lemmaizing generalize to semantic resolution the rules for lemmaizing in model elimination. On the contraction side, we give contraction rules for semantic strategies, and we define a purity deletion rule for first-order clauses that preserves completeness. While lemmaizing generalizes success caching of model elimination, purity deletion echoes failure caching. Thus, our approach integrates features of backward and forward reasoning. We also discuss the relevance of our work to logic programming.

On semantic resolution with lemmaizing and contraction and a formal treatment of caching

BONACINA, Maria Paola
;
1998-01-01

Abstract

Reducing redundancy in search has been a major concern for automated deduction. Subgoal-reduction strategies, such as those based on model elimination and implemented in Prolog technology theorem provers, prevent redundant search by using lemmaizing and caching, whereas contraction-based strategies prevent redundant search by using contraction rules, such as subsumption. In this work we show that lemmaizing and contraction can coexist in the framework of semantic resolution. On the lemmaizing side, we define two meta-level inference rules for lemmaizing in semantic resolution, one producing unit lemmas and one producing non-unit lemmas, and we prove their soundness. Rules for lemmaizing are meta-rules because they use global knowledge about the derivation, e.g. ancestry relations, in order to derive lemmas. Our meta-rules for lemmaizing generalize to semantic resolution the rules for lemmaizing in model elimination. On the contraction side, we give contraction rules for semantic strategies, and we define a purity deletion rule for first-order clauses that preserves completeness. While lemmaizing generalizes success caching of model elimination, purity deletion echoes failure caching. Thus, our approach integrates features of backward and forward reasoning. We also discuss the relevance of our work to logic programming.
1998
Mechanical theorem proving; semantic resolution; resolution with set of support; model elimination; forward and backward reasoning
File in questo prodotto:
File Dimensione Formato  
NGC1998semrlc.pdf

accesso aperto

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