Logical Approaches to Computational Barriers
From MaRDI portal
Publication:5898815
DOI10.1007/11780342zbMath1133.03029OpenAlexW4255986326WikidataQ55968647 ScholiaQ55968647MaRDI QIDQ5898815
Stéphane Lengrand, Roy Dyckhoff
Publication date: 30 April 2007
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11780342
sequent calculusintuitionistic logicpurificationguarded logiccall-by-value semanticsdepth-boundedfocused
Functional programming and lambda calculus (68N18) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Combinatory logic and lambda calculus (03B40)
Related Items
From axioms to synthetic inference rules via focusing, A unified procedure for provability and counter-model generation in minimal implicational logic, An Evaluation-Driven Decision Procedure for G3i, A Survey of the Proof-Theoretic Foundations of Logic Programming, A focused approach to combining logics, Focused linear logic and the \(\lambda\)-calculus, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, Focused proof-search in the logic of bunched implications, Intuitionistic Decision Procedures Since Gentzen, Multi-focused proofs with different polarity assignments, On the unity of duality, Specifying Proof Systems in Linear Logic with Subexponentials, A framework for proof systems, Focalisation and Classical Realisability, Focusing and polarization in linear, intuitionistic, and classical logics
