Artículo

Proof Normalisation in a Logic Identifying Isomorphic Propositions

Díaz Caro, AlejandroIcon ; Dowek, Gilles
Fecha de publicación: 06/2019
Editorial: Schloss Dagstuhl. Leibniz-Zentrum für Informatik
Revista: Leibniz International Proceedings in Informatics, LIPIcs
ISSN: 1868-8969
Idioma: Inglés
Tipo de recurso: Artículo publicado
Clasificación temática:

Resumen

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.
Palabras clave: CUT-ELIMINATION , ISOMORPHISMS , LOGIC , PROOF-REDUCTION , SIMPLY TYPED LAMBDA CALCULUS
 
Archivos asociados
Thumbnail
 
Tamaño: 553.3Kb
Formato: PDF
.
Licencia
info:eu-repo/semantics/openAccess Excepto donde se diga explícitamente, este item se publica bajo la siguiente descripción: Creative Commons Attribution 2.5 Unported (CC BY 2.5)
Identificadores
URI: http://hdl.handle.net/11336/123317
URL: http://drops.dagstuhl.de/opus/volltexte/2019/10521/
DOI: http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.14
Colecciones
Articulos(ICC)
Articulos de INSTITUTO DE INVESTIGACION EN CIENCIAS DE LA COMPUTACION
Citación
Díaz Caro, Alejandro; Dowek, Gilles ; Proof Normalisation in a Logic Identifying Isomorphic Propositions; Schloss Dagstuhl. Leibniz-Zentrum für Informatik; Leibniz International Proceedings in Informatics, LIPIcs; 131; 6-2019; 1-23
Compartir
Altmétricas