Evaluation-Based Reasoning with Disjunctive Informationin First-Order Knowledge Bases

Abstract In previous work, Levesque proposed anevaluation-based reasoning procedure for socalled proper KBs, equivalent to a possibly in-complete possibly infinite set of function-free ground literals. The procedure, called V; pre-served the efficiency and logical soundness of database query evaluation. Moreover, if thequery was constrained to be in a special normal form, V was also logically complete. In this pa-per, we propose an extension to this work to handle disjunctive information in a KB. We definea query evaluation procedure X that generalizes V to deal with KBs that are equivalent to a pos-sibly infinite set of function-free ground clauses. Deductive reasoning that is logically sound andcomplete in this case is undecidable in general, and so, we describe what we are willing to giveup in X to preserve tractability