scientific article; zbMATH DE number 7455712

MaRDI QIDQ5020970zbMATH OpenFDO

Authors Paul Tarau, Valeria de Paiva

Publication date 11 January 2022

Full work available at URL https://arxiv.org/abs/2009.10241, http://eptcs.web.cse.unsw.edu.au/paper.cgi?ICLP2020.18

zbMATH Keywords

combinatorial generation of provable formulas of a given sizeCurry-Howard isomorphismefficient generation of linear lambda terms in normal formintuitionistic and linear logic theorem proversprolog programs for lambda term generation and theorem provingtheorems of the implicational fragment of propositional linear intuitionistic logic

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• The semantics and proof theory of linear logic
• scientific article; zbMATH DE number 4145871
• Deduction theorems for weak implicational logics
• scientific article; zbMATH DE number 1292302
• scientific article; zbMATH DE number 786489
• Proof finding algorithms for implicational logics
• Proofs as computations in linear logic
• scientific article; zbMATH DE number 2152687
• Natural deduction for intuitionistic linear logic
• A Uniform Proof-theoretic Investigation of Linear Logic Programming

Cites work

• A hiking trip through the orders of magnitude: deriving efficient generators for closed simply-typed lambda terms and normal forms
• Asymptotics and random sampling for BCI and BCK lambda terms
• Closed categories and the theory of proofs
• Contraction-free sequent calculi for intuitionistic logic
• Counting and generating lambda terms
• Decidability of linear affine logic
• scientific article; zbMATH DE number 3983158 (Why is no real title available?)
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 2024859 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Intuitionistic propositional logic is polynomial-space complete
• Intuitionistic vs. Classical Tautologies, Quantitative Comparison
• Linear logic
• Neural probabilistic logic programming in DeepProbLog
• On uniquely closable and uniquely typable skeletons of lambda terms
• Quantitative Aspects of Linear and Affine Closed Lambda Terms
• Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers
• The ILLTP library for intuitionistic linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(2)

• Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis
• Almost all Classical Theorems are Intuitionistic

Describes a project that uses

Uses Software

• ILLTP
• Haskell
• OEIS
• DeepProbLog

This page was built for publication:

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