Proofs as computations in linear logic

DOI10.1016/S0304-3975(00)00024-4MaRDI QIDQ5941199zbMATH OpenFDO

Authors Giorgio Delzanno, M. Martelli

Publication date 20 August 2001

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0304-3975(00)00024-4

zbMATH Keywords

extensions of logic programminghigher-order logiclinear logic

Mathematics Subject Classification ID

Recommendations

• Uniform proofs as a foundation for logic programming
• Logic Programming with Focusing Proofs in Linear Logic
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• A proof procedure for the logic of hereditary Harrop formulas
• scientific article; zbMATH DE number 1761892

Cites work

• A specification logic for concurrent object-oriented programming
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• Asynchronous communication model based on linear logic
• Forum: A multiple-conclusion specification logic
• scientific article; zbMATH DE number 4209572 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 1231530 (Why is no real title available?)
• scientific article; zbMATH DE number 1231695 (Why is no real title available?)
• Linear logic
• Logic programming in a fragment of intuitionistic linear logic
• Logic Programming with Focusing Proofs in Linear Logic
• Object calculi in linear logic
• On proof normalization in linear logic
• The Semantics of Predicate Logic as a Programming Language
• Uniform proofs as a foundation for logic programming

Cited in

(23)

• The number of proof lines and the size of proofs in first order logic
• A proof procedure for the logic of hereditary Harrop formulas
• Linear logic as a logic of computations
• Logic programming in a fragment of intuitionistic linear logic
• On proof normalization in linear logic
• New uses of linear arithmetic in automated theorem proving by induction
• Uniform proofs as a foundation for logic programming
• Forward and backward chaining in linear logic. (Extended abstract)
• An even closer integration of linear arithmetic into inductive theorem proving
• Proof-theoretic and higher-order extensions of logic programming
• From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing
• Logic Programming with Focusing Proofs in Linear Logic
• scientific article; zbMATH DE number 1324432 (Why is no real title available?)
• scientific article; zbMATH DE number 517072 (Why is no real title available?)
• A Uniform Proof-theoretic Investigation of Linear Logic Programming
• Some Properties of Linear Logic Proved by Semantic Methods
• scientific article; zbMATH DE number 1104361 (Why is no real title available?)
• scientific article; zbMATH DE number 1368923 (Why is no real title available?)
• An improved proof-theoretic compilation of logic programs
• scientific article; zbMATH DE number 7441265 (Why is no real title available?)
• scientific article; zbMATH DE number 7455712 (Why is no real title available?)
• Logic Programming
• Correctness of linear logic proof structures is NL-complete

Describes a project that uses

Uses Software

• Lolli

This page was built for publication: Proofs as computations in linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5941199)