A top-down query processing method for first order deductive databases under the disjunctive well-founded semantics (DWFS) is presented. The method is based upon a characterisation of the DWFS in terms of the Gelfond-Lifschitz transformation, and employs a hyperresolution like operator and quasi cyclic trees to handle minimal model processing. The method is correct and complete, and can be guaranteed to terminate given certain mild constraints on the format of database rules. The efficiency of the method is enhanced by the fact that large parts of the search tree are naturally grounded, even for first order queries and databases. In the case of a grounded yes/no answer, the search tree only becomes non-grounded if processing enters the definite part of the database. For finite propositional databases the method runs in polynomial space. Efficiency may be enhanced by the application of partial compilation.
C. A. Johnson