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 <>
Submitted on : Thursday, July 30, 2020 - 9:24:41 AM
Last modification on : Monday, August 3, 2020 - 3:24:21 PM
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

32

Files downloads

61