Several formal systems, such as resolution and minimal model semantics, provide a frameworkfor logic programming. In this article, we will survey the use of structural proof theory as analternative foundation. Researchers have been using this foundation for the past 35 years toelevate logic programming from its roots in first-order classical logic into higher-order versionsof intuitionistic and linear logic. These more expressive logic programming languages allow forcapturing 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 extendedlogic 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-levelmeans for presenting the differences between forward-chaining and backward-chaining style inferences.Anchoring logic programming in proof theory has also helped identify its connectionsand differences with functional programming, deductive databases, and model checking.
展开▼
