Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Proof Normalisation in a Logic Identifying Isomorphic Propositions

Abstract : We define a fragment of propositional logic where isomorphic propositions, such as A ∧ B and B ∧ A, or A ⇒ (B ∧ C) and (A ⇒ B) ∧ (A ⇒ C) are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.
Document type :
Conference papers
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Gilles Dowek Connect in order to contact the contributor
Submitted on : Thursday, July 30, 2020 - 9:24:41 AM
Last modification on : Friday, January 21, 2022 - 3:15:31 AM
Long-term archiving on: : Tuesday, December 1, 2020 - 9:54:04 AM


Files produced by the author(s)


  • HAL Id : hal-02909135, version 1



Alejandro Díaz-Caro, Gilles Dowek. Proof Normalisation in a Logic Identifying Isomorphic Propositions. FSCD 2019 - International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨hal-02909135⟩



Record views


Files downloads