Sciweavers

Share
NGC
1998
Springer

On Semantic Resolution with Lemmaizing and Contraction and a Formal Treatment of Caching

10 years 2 months ago
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. 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 stra...
Maria Paola Bonacina, Jieh Hsiang
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 1998
Where NGC
Authors Maria Paola Bonacina, Jieh Hsiang
Comments (0)
books