Intuitionistic games: determinacy, completeness, and normalization

DOI10.1007/s11225-016-9661-4zbMath1417.03127OpenAlexW2284305443MaRDI QIDQ332080

Paweł Urzyczyn

Publication date: 27 October 2016

Published in: Studia Logica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11225-016-9661-4

zbMATH Keywords

intuitionistic logicgamesinhabitationproofs

Mathematics Subject Classification ID

Applications of game theory (91A80) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (4)

Small model property reflects in games and automata ⋮ Hammer for Coq: automation for dependent type theory ⋮ Answer set programming in intuitionistic logic ⋮ A dialogical route to logical pluralism

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mechanical procedure for proof construction via closed terms in typed \(\lambda\) calculus
• Lectures on the Curry-Howard isomorphism
• Focusing and polarization in linear, intuitionistic, and classical logics
• On the strong normalisation of intuitionistic natural deduction with permutation-conversions
• Proofs and countermodels in non-classical logics
• A short note on type-inhabitation: formula-trees vs. game semantics
• Locus Solum: From the rules of logic to the logic of rules
• On Long Normal Inhabitants of a Type
• Proof Search and Counter Model of Positive Minimal Predicate Logic

This page was built for publication: Intuitionistic games: determinacy, completeness, and normalization