Back to Search
Start Over
A Survey of the Proof-Theoretic Foundations of Logic Programming
- Source :
- Theory and Practice of Logic Programming, Theory and Practice of Logic Programming, Cambridge University Press (CUP), 2021, pp.1-46. ⟨10.1017/S1471068421000533⟩, Theory and Practice of Logic Programming, 2021, pp.1-46. ⟨10.1017/S1471068421000533⟩
- Publication Year :
- 2021
- Publisher :
- Cambridge University Press (CUP), 2021.
-
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 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.<br />To appear in Theory and Practice of Logic Programming (TPLP)
- Subjects :
- FOS: Computer and information sciences
Computer Science - Logic in Computer Science
F.3.2
F.4.1
Computer science
Semantics (computer science)
0102 computer and information sciences
Mathematical proof
computer.software_genre
01 natural sciences
Theoretical Computer Science
Artificial Intelligence
Computer Science::Logic in Computer Science
Structural proof theory
0101 mathematics
Logic programming
Functional programming
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Computer Science - Programming Languages
Programming language
010102 general mathematics
Classical logic
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Linear logic
Logic in Computer Science (cs.LO)
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Computational Theory and Mathematics
010201 computation theory & mathematics
Hardware and Architecture
Proof theory
Computer Science::Programming Languages
computer
Software
Programming Languages (cs.PL)
Subjects
Details
- ISSN :
- 14753081 and 14710684
- Volume :
- 22
- Database :
- OpenAIRE
- Journal :
- Theory and Practice of Logic Programming
- Accession number :
- edsair.doi.dedup.....4ad6e21bb75c8a9e6cb972766025af8b