scientific article; zbMATH DE number 7455712
From MaRDI portal
Publication:5020970
Publication date: 11 January 2022
Full work available at URL: https://arxiv.org/abs/2009.10241
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Curry-Howard isomorphismcombinatorial generation of provable formulas of a given sizeefficient 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
Related Items
Abductive Reasoning in Intuitionistic Propositional Logic via Theorem Synthesis ⋮ Almost all Classical Theorems are Intuitionistic
Uses Software
Cites Work
- Asymptotics and random sampling for BCI and BCK lambda terms
- Linear logic
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Closed categories and the theory of proofs
- Intuitionistic propositional logic is polynomial-space complete
- On uniquely closable and uniquely typable skeletons of lambda terms
- Decidability of linear affine logic
- Neural probabilistic logic programming in DeepProbLog
- A hiking trip through the orders of magnitude: deriving efficient generators for closed simply-typed lambda terms and normal forms
- Intuitionistic vs. Classical Tautologies, Quantitative Comparison
- Contraction-free sequent calculi for intuitionistic logic
- Quantitative Aspects of Linear and Affine Closed Lambda Terms
- Random generation of closed simply typed λ-terms: A synergy between logic programming and Boltzmann samplers
- Counting and generating lambda terms
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
