References & Citations
Computer Science > Logic in Computer Science
Title: Proof Normalisation in a Logic Identifying Isomorphic Propositions
(Submitted on 25 Jan 2015 (v1), last revised 22 Apr 2019 (this version, v8))
Abstract: We define a fragment of propositional logic where isomorphic propositions, such as $A\land B$ and $B\land A$, or $A\Rightarrow (B\land C)$ and $(A\Rightarrow B)\land(A\Rightarrow C)$ are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.
Submission history
From: Alejandro Díaz-Caro [view email][v1] Sun, 25 Jan 2015 08:04:14 GMT (22kb)
[v2] Tue, 24 Feb 2015 10:00:31 GMT (21kb)
[v3] Mon, 15 Jun 2015 07:26:47 GMT (26kb)
[v4] Tue, 7 Aug 2018 13:48:29 GMT (40kb)
[v5] Fri, 10 Aug 2018 06:52:19 GMT (40kb)
[v6] Fri, 17 Aug 2018 19:10:10 GMT (0kb,I)
[v7] Tue, 12 Feb 2019 18:16:44 GMT (84kb,D)
[v8] Mon, 22 Apr 2019 11:10:47 GMT (97kb,D)
Link back to: arXiv, form interface, contact.