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

Reducing redundancy in search has been a major concern for automated deduction. Sub- goal-reduction strategies, such as those based on model elimination and implemented in Pro- log 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 dene 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 lem- mas. 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 strate- gies, and we dene a purity deletion rule for rst-order clauses that preserves completeness. While lemmaizing generalizes success caching of model elimination, purity deletion echoes fai- lure caching. Thus, our approach integrates features of backward and forward reasoning. We also discuss the relevance of our work to logic programming.