CH-Prolog: A Proof Procedure for Positive Disjunctive Logic Programming

The success of Prolog motivates people to use full first-order logic instead of only Horn clauses as the basis of logic programming. One of the main work in this extending is to seek proof procedures for new logic programming. Positive disjunctive logic programming extends Horn clause programming by allowing more than one atoms to occur in the head of a program clause. In this paper we propose a new proof procedure for disjunctive logic programming which is based on a novel program transformation. With this transformation, the new proof procedure shares many important properties enjoyed by SLD-resolution. The soundness and completeness of the proof procedure with respect to computing answers are given.