Reciprocal Influences Between Proof Theory and Logic Programming

Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : The topics of structural proof theory and logic programming have influenced each other for more than three decades. Proof theory has contributed the notion of sequent calculus, linear logic, and higher-order quantification. Logic programming has introduced new normal forms of proofs and forced the examination of logic-based approaches to the treatment of bindings. As a result, proof theory has responded by developing an approach to proof search based on focused proof systems in which introduction rules are organized into two alternating phases of rule application. Since the logic programming community can generate many examples and many design goals (e.g., modularity of specifications and higher-order programming), the close connections with proof theory have helped to keep proof theory relevant to the general topic of computational logic.
Complete list of metadatas

Cited literature [106 references]  Display  Hide  Download

https://hal.inria.fr/hal-02368867
Contributor : Dale Miller <>
Submitted on : Tuesday, November 19, 2019 - 1:21:22 PM
Last modification on : Thursday, November 21, 2019 - 3:52:07 PM

File

lppt-extended.pdf
Files produced by the author(s)

Identifiers

Citation

Dale Miller. Reciprocal Influences Between Proof Theory and Logic Programming. Philosophy & Technology, Springer, 2019, ⟨10.1007/s13347-019-00370-x⟩. ⟨hal-02368867⟩

Share

Metrics

Record views

32

Files downloads

43