A logic identifying isomorphic propositions

Alejandro Díaz-Caro (1, 2) , Gilles Dowek (3, 4)

1 UNQ - Universidad Nacional de Quilmes
2 ICC - Instituto de Investigación en Ciencias de la Computación [Buenos Aires]
3 LSV - Laboratoire Spécification et Vérification [Cachan]
4 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique

There is a mistake in the main proof (strong normalisation), and the system is actually not normalising in its current form, hence, we have withdrawn the draft until we have a fixed version.

Mots clés: normalisation; typed lambda calculus; deduction modulo; type isomorphisms

Domaines: Logique en informatique [cs.LO]

Alejandro Díaz-Caro, Gilles Dowek. A logic identifying isomorphic propositions. 2018. ⟨hal-01109104v5⟩