SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy |
| |
Authors: | Donald W Loveland Adnan H Yahya |
| |
Affiliation: | (1) Department of Computer Science, Duke University, 27708 Durham, NC, USA;(2) Electrical Engineering Department, Birzeit University, Birzeit, Palestine |
| |
Abstract: | 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. |
| |
Keywords: | Disjunctive Deductive Databases Query Answering Bidirectional Search Model Generation Theorem Proving Relevancy |
本文献已被 SpringerLink 等数据库收录! |
|