Incorporating bidirectional relevancy into model generation theorem provers

Abstract

Model-generation theorem provers, SATCHMO-style, can explore a larger than needed search space when answering a query. Partial and total relevancy were suggested as a mechanisms to limit the search space to clauses that are needed for the refutation. SATCHMORE was an implementation of the latter. SATCHMORE relevancy, however, is driven by the entire set of negative clauses of the theory and no distinction is accorded to the query negation. Under unfavorable circumstances, such as in the presence of large amounts of negative data, this can reduce e ciency. In this lecture we de ne a further re nement of that uses only the negation of the query for relevancy determination at the start. Other negative clauses are introduced on demand and only if a refutation is not possible using the current set of negative clauses. The search for the relevant negative clauses is performed in a forward chaining mode as opposed to relevancy propagation in SATCHMORE which is based on backward chaining. The approach is shown to be refutationally sound and complete. Experiments on a prototype implementation point to its potential to enhance the effciency of the query answering process in disjunctive databases.