Skip to Main content Skip to Navigation
Journal articles

Reciprocal Influences Between Proof Theory and Logic Programming

Dale Miller 1 
1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
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 metadata

Cited literature [106 references]  Display  Hide  Download
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Tuesday, November 19, 2019 - 1:21:22 PM
Last modification on : Friday, July 8, 2022 - 10:09:59 AM
Long-term archiving on: : Thursday, February 20, 2020 - 3:17:46 PM


Files produced by the author(s)



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



Record views


Files downloads