A Survey of the Proof-Theoretic Foundations of Logic Programming

Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this article, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. Logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking.

An Improved Proof-Theoretic Compilation of Logic Programs

In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their linear variant. Compiled clauses were themselves logic formulas except for the presence of a second-order abstraction over the atomic goals matching their head. In this paper, we revisit our previous results into a more detailed and fully logical justification that does away with this spurious abstraction. We then refine the resulting technique to support well-moded programs efficiently.

Logic Programming Languages for Expert Systems

“Expert systems” are a significant subset of what is known as “decision support systems” (DSS). This article suggests a different paradigm for expert systems than what is commonly used. Most often, expert systems are developed with a tool called an “expert system shell.” For the more adventurous, an expert system might be developed with Prolog, a language for artificial intelligence. Both Prolog and expert system shells stem from technology that is approximately 30 years old.1 There have been updates to these platforms, such as GUI interfaces, XML interfaces, and other “bells and whistles.” However, the technology is still fundamentally old. As an analogy, the current technology is akin to updating a 30-year-old car with new paint (a gooey interface), new upholstery, GPS, and so forth. However, the car is fundamentally still a 30-year-old car. It may be in far better shape than another 30-year-old car without the updates, but it cannot compete from an engineering perspective with current models.2 Similarly, the reasoning power of current expert system technology cannot compete with the reasoning power of the state of the art in logic programming. These advances that have taken place in the logic programming community since the advent of Prolog and expert system shells include: a well developed theory of multiple forms of negation, an understanding of open domains, and the closed world assumption, default reasoning with exceptions, reasoning with respect to time (i.e., a solution to the frame problem and introspection with regard to previous beliefs), reasoning about actions, introspection, and maintaining multiple views of the world simultaneously (i.e., reasoning with uncertainty). This article examines a family of logic programming languages. This article in conjunction with a companion article this volume, Knowledge Representation That Can Empower Expert Systems, suggest that logic programs employing recent advances in semantics and in knowledge representation provide a more robust framework in which to develop expert systems. The author has successfully applied this paradigm and these ideas to financial applications, security applications, and enterprise information systems.