A semantics of realisability for the classical propositional natural deduction
Karim Nour (LAMA), Khelifa Saber (LAMA)
TL;DR
This paper introduces a realisability semantics for classical propositional natural deduction, providing a correctness theorem that characterizes the operational behavior of typed terms in this logical framework.
Contribution
It presents a novel semantics for classical propositional natural deduction and proves a correctness theorem linking semantics to operational behavior.
Findings
Semantics of realisability for classical propositional natural deduction established
Correctness theorem proven connecting semantics and operational behavior
Characterization of typed terms' operational behavior achieved
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Computability, Logic, AI Algorithms