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

https://hal.inria.fr/hal-02909135
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

File

proofnormalization.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02909135, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

26

Files downloads

7