Reducing redundancy in search has been a major concern for automated deduction. Subgoal-reduction strategies 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 for unit and one for 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. 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.

On semantic resolution with lemmaizing and contraction

BONACINA, Maria Paola;
1996

Abstract

Reducing redundancy in search has been a major concern for automated deduction. Subgoal-reduction strategies 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 for unit and one for 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. 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.
9783540615323
File in questo prodotto:
Non ci sono file associati a questo prodotto.

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: http://hdl.handle.net/11562/16051
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact