A semantics of realisability for the classical propositional natural deduction

MaRDI QIDQ2851691zbMATH OpenFDO

Authors Khelifa Saber, Karim Nour

Publication date 2 October 2013

Full work available at URL https://arxiv.org/abs/0905.1555, http://www.sciencedirect.com/science/article/pii/S1571066105051248

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Abstract: In this paper, we introduce a semantics of realisability for the classical propositional natural deduction and we prove a correctness theorem. This allows to characterize the operational behaviour of some typed terms.

Recommendations

• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• scientific article; zbMATH DE number 1104448
• A Survey of Classical Realizability
• scientific article; zbMATH DE number 1337625
• On semantics of a term calculus for classical logic

Cited in

(5)

• Strong normalization of classical natural deduction with disjunctions
• A Classical Realizability Model for a Semantical Value Restriction
• scientific article; zbMATH DE number 5851813 (Why is no real title available?)
• Towards a Canonical Classical Natural Deduction System
• A completeness result for the simply typed \(\lambda \mu \)-calculus

This page was built for publication: A semantics of realisability for the classical propositional natural deduction

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