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 usinglemmaizing andcaching, whereas contraction-based strategies prevent redundant search by usingcontraction rules, such assubsumption. In this work we show that lemmaizing and contraction can coexist in the framework ofsemantic 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 apurity 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. Supported in part by the National Science Foundation with grant CCR-94-08667 and CCR-97-01508. Supported in part by grant NSC 86-2213-E-002-047 and NSC 87-2213-E-002-029 of the National Science Council of the Republic of China. Maria Paola Bonacina, Ph.D.: She is on the faculty of the Department of Computer Science of the University of Iowa. She received a laurea (1986) and a doctorate in informatics from the Universita degli Studi di Milano, and a Ph.D. in computer science from the State University of New York at Stony Brook (1992). She was awarded fellowships by the Universita degli Studi di Milano, the European Union and the General Electric Foundation. The unifying theme of her research is automated theorem proving. Her research areas include distributed automated deduction, the theory of search and strategy analysis, completion-based theorem proving, category theory for computer science, term rewriting systems, logic programming, and manyvalued logic. Jieh Hsiang, Ph.D.: He is a Professor of Computer Science at the National Taiwan University and is also the Director of the Center of Excellence for Research in Computer Systems of the National Taiwan University. Professor Hsiang is known for work in term rewriting systems and automated deduction. His other research interests include logic programming, programming logics, computer viruses, and intelligent agents. Recently he has also become interested in the digitization of Taiwanese and Chinese historical records and heritage. Professor Hsiang received a B.S. degree in mathematics from National Taiwan University in 1976 and a Ph.D. degree in computer science from the University of Illinois at Urbana-Champaign in 1982. Before returning to Taiwan in 1993, he was a Professor of Computer Science at the State University of New York st Stony Brook.