A Case-Analysis Approach to Disjunctive Logic Programming

Disjunctive Logic programming is an extension of standard Horn logic programming which allows for the expression of indefinite or incomplete information. In this thesis, we provide a unified approach to disjunctive logic programming based on case-analysis. We describe a family of procedures, called the near-Horn Prologs, which naturally extend the standard Horn program procedure (SLD-resolution) through case-analysis. Since the near-Horn Prolog procedures retain much of the form and flavor of SLD-resolution (the basis of the programming language Prolog), they may be seen as the ideal basis for a programming language which extends Prolog. The near-Horn Prolog procedures also appear to be more efficient than alternative procedures (such as SLI-resolution), especially when the amount of non-Horn information in a program is small. We provide the theoretical foundations of the near-Horn Prologs with a declarative characterization of disjunctive logic programs which utilizes fixpoint operators. In addition to capturing the consequences of a program (while naturally extending the standard Horn program characterization), this characterization matches the case-analysis behavior of one of the near-Horn Prolog variants and so provides insight into its behavior. We consider the addition of negation to disjunctive logic programs, demonstrating that both explicit classical negation and implicit default negation can easily be incorporated into our case-analysis approach. We also compare the near-Horn Prologs with proof systems taken from varied application domains, and show that each utilizes case-analysis in a similar manner. By comparing these different systems, we gain insight into the approach and the relative tradeoffs involved.