Negative Hyper-resolution as Procedural Semantics of Disjunctive Logic Programs
We prove that negative hyper-resolution is a sound and complete procedure for answering queries in disjunctive logic programs. In our formulation, answers of queries are defined using disjunctive substitutions, which are more flexible than answer literals used in theorem proving systems.