Kripke models for classical logic
From MaRDI portal
Publication:636371
DOI10.1016/j.apal.2010.04.007zbMath1225.03009arXiv0904.0071OpenAlexW2112507467MaRDI QIDQ636371
Danko Ilik, Gyesik Lee, Hugo Herbelin
Publication date: 26 August 2011
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0904.0071
sequent calculusKripke modelclassical logicnormalization by evaluationclassical realizabilitylambda-mu calculus
Related Items
A pure view of ecumenical modalities, Unnamed Item, Formalization of the resolution calculus for first-order logic, An ecumenical notion of entailment, Constructive Formalization of Hybrid Logic with Eventualities, On the unification of classical, intuitionistic and affine logics
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Constructions of classical models by means of Kripke models (Survey)
- Constructivism in mathematics. An introduction. Volume II
- On theorems of Gödel and Kreisel: Completeness and Markov's principle
- Algebraic proofs of cut elimination
- Computational isomorphisms in classical logic
- A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Intuitionistic completeness and classical logic
- Krivine's intuitionistic proof of classical completeness (for countable languages)
- Remarks on isomorphisms in typed lambda calculi with empty and sum types
- The duality of computation
- Une Preuve Formelle et Intuitionniste du Théorème de Complétude de la Logique Classique
- A completeness theorem in modal logic
- Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
- Typed Applicative Structures and Normalization by Evaluation for System F ω
- An intuitiomstic completeness theorem for intuitionistic predicate logic
- Foundations of Software Science and Computation Structures
- Theoretical Computer Science
- On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
- On weak completeness of intuitionistic predicate logic
