Typed Lambda Calculi and Applications
From MaRDI portal
Publication:5704011
DOI10.1007/b135690zbMath1114.03044MaRDI QIDQ5704011
Publication date: 11 November 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/b135690
Kripke structure; deduction modulo; intuitionistic sequent calculus; cut admissibility; cut elimination property
03F05: Cut-elimination and normal-form theorems
68Q42: Grammars and rewriting systems
03B47: Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics)
03B20: Subsystems of classical logic (including intuitionistic logic)
Related Items
A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic, Resolution is cut-free, Some general results about proof normalization, On Artemov and Protopopescu's intuitionistic epistemic logic expanded with distributed knowledge, First-order automated reasoning with theories: when deduction modulo theory meets practice, Regaining cut admissibility in deduction modulo using abstract completion, On the Convergence of Reduction-based and Model-based Methods in Proof Theory, Axiom Directed Focusing, Automating Theories in Intuitionistic Logic