CH-Prolog: A Proof Procedure for Positive Disjunctive Logic Programming
Wenjin Lu · 1999
The success of Prolog motivates people to use full firstorder logic instead of only Horn clauses as the basis of logic programming. One of the main work in this extending is to seek proof procedure 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 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. Key Words: Disjunctive Logic Programming, SLDresolution, Proof Procedure. 1. Introduction The success of Prolog motivates people to use full firstorder logic instead of only Horn clauses as the basis of logic programming (Loveland 1987). Positive disjunctive logic programming is one of th...