SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy

SATCHMORE was introduced as a mechanism to integrate relevancy testing with the model-generation theorem prover SATCHMO. This made it possible to avoid invoking some clauses that appear in no refutation, which was a major drawback of the SATCHMO approach. SATCHMORE relevancy, however, is driven by the entire set of negative clauses 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 the efficiency of SATCHMORE. In this paper we introduce a further refinement of SATCHMO called SATCHMOREBID: SATCHMORE with BIDirectional relevancy. SATCHMOREBID 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. SATCHMOREBID is shown to be refutationally sound and complete. Experiments on a prototype SATCHMOREBID implementation point to its potential to enhance the efficiency of the query answering process in disjunctive databases. Donald Loveland, Ph.D.: He is Emeritus Professor of Computer Science at Duke University. He received his Ph.D. in mathematics from New York University and taught at NYU and CMU prior to joining Duke in 1973. His research in automated deduction includes defining the model elimination proof procedure and the notion of linear resolution. He is author of one book and editor/co-editor of two other books on automated theorem proving. He has done research in the areas of algorithms, complexity, expert systems and logic programming. He is an AAAI Fellow, ACM Fellow and winner of the Herbrand Award in Automated Reasoning. Adnan H. Yahya, Ph.D.: He is an associate professor at the Department of Electrical Engineering, Birzeit University, Palestine. He received his Diploma and PhD degrees from St. Petersburg Electrotechnical University and Nothwestern University in 1979 and 1984 respectively. His research interests are in Artificial Intelligence in general and in the areas of Deductive Databases, Logic Programming and Nonmonotonic Reasoning in particular. He had several visiting appointments at universities and research labs in the US, Germany, France and the UK. Adnan Yahya is a member of the ACM, IEEE and IEEE Computer Society.