Intuitionistic games: determinacy, completeness, and normalization

DOI10.1007/S11225-016-9661-4MaRDI QIDQ332080zbMATH OpenOpenAlexFDO

Authors 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

gamesinhabitationintuitionistic logicproofs

Mathematics Subject Classification ID

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

Recommendations

• The problem of determinacy of infinite games from an intuitionistic point of view
• Dialogues, strategies, and intuitionistic provability
• Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves
• Some remarks on relations between proofs and games
• The intuitionistic fragment of computability logic at the propositional level

Cites work

• A short note on type-inhabitation: formula-trees vs. game semantics
• Focusing and polarization in linear, intuitionistic, and classical logics
• scientific article; zbMATH DE number 5853298 (Why is no real title available?)
• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 1499102 (Why is no real title available?)
• scientific article; zbMATH DE number 2085249 (Why is no real title available?)
• scientific article; zbMATH DE number 3300581 (Why is no real title available?)
• Lectures on the Curry-Howard isomorphism
• Locus solum: From the rules of logic to the logic of rules.
• Logic in games
• Long normal form proof search and counter-model generation
• Mechanical procedure for proof construction via closed terms in typed calculus
• On Long Normal Inhabitants of a Type
• On the strong normalisation of intuitionistic natural deduction with permutation-conversions
• Proof Search and Counter Model of Positive Minimal Predicate Logic
• Proofs and countermodels in non-classical logics
• Some remarks on relations between proofs and games

Cited in

(11)

• Dialogues, strategies, and intuitionistic provability
• Hammer for Coq: automation for dependent type theory
• Answer set programming in intuitionistic logic
• Small model property reflects in games and automata
• Weak axioms of determinacy and subsystems of analysis I: δ20 games
• Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves
• The problem of determinacy of infinite games from an intuitionistic point of view
• The Parallel Intensionally Fully Abstract Games Model of PCF
• Finite high-order games and an inductive approach towards Gowers's dichotomy
• A dialogical route to logical pluralism
• Duality in intuitionistic propositional logic

Describes a project that uses

Uses Software

• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q332080)