Paper Info
Title
A Survey of the Proof-Theoretic Foundations of Logic Programming.
Abstract
Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, 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 both 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 polarity and focused proofs. These recent results have also provided 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.
Year
DOI
Venue
2022
10.1017/S1471068421000533
Theory and Practice of Logic Programming
DocType
Volume
Issue
Journal
22
6
ISSN
Citations 
PageRank 
1471-0684
0
0.34
References 
Authors
0
1
Name
Order
Citations
PageRank
Dale Miller12485232.26