Typed Lambda Calculi and Applications

DOI10.1007/b135690zbMath1114.03044OpenAlexW2501230561MaRDI QIDQ5704011

Olivier Hermant

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

zbMATH Keywords

Kripke structurededuction modulointuitionistic sequent calculuscut admissibilitycut elimination property

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Grammars and rewriting systems (68Q42) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (9)

On Artemov and Protopopescu's intuitionistic epistemic logic expanded with distributed knowledge ⋮ Some general results about proof normalization ⋮ A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Resolution is cut-free ⋮ Regaining cut admissibility in deduction modulo using abstract completion ⋮ Axiom Directed Focusing ⋮ Automating Theories in Intuitionistic Logic ⋮ On the Convergence of Reduction-based and Model-based Methods in Proof Theory

This page was built for publication: Typed Lambda Calculi and Applications