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

Wenjin Lu, University of Koblenz-Landau

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.


This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.