Three Dimensional Proofnets for Classical Logic

Clement Houtmann 1
1 PAREO - Formal islands: foundations and applications
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Classical logic and more precisely classical sequent calculi are currently the subject of several studies that aim at providing them with an algorithmic meaning. They are however ruled by an annoying syntactic bureaucracy which is a cause of pathologic non-confluence. An interesting patch consists in representing proofs using proofnets. This leads (at least in the propositional case) to cut-elimination procedures that remain confluent and strongly normalising without using any restricting reduction strategy. In this paper we describe a presentation of sequents in a two-dimensional space as well as a presentation of proofnets and sequent calculus derivations in a three-dimensional space. These renderings admit interesting geometrical properties: sequent occurrences appear as parallel segments in the case of three-dimensional sequent calculus derivations and the De Morgan duality is expressed by the fact that negation stands for a ninety degree rotation in the case of two-dimensional sequents and three-dimensional proofnets.
Type de document :
Pré-publication, Document de travail
2009
Liste complète des métadonnées

Littérature citée [17 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00426469
Contributeur : Clement Houtmann <>
Soumis le : mardi 8 décembre 2009 - 15:09:53
Dernière modification le : jeudi 11 janvier 2018 - 01:49:21
Document(s) archivé(s) le : samedi 26 novembre 2016 - 15:38:30

Fichier

3dnets.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00426469, version 2

Collections

Citation

Clement Houtmann. Three Dimensional Proofnets for Classical Logic. 2009. 〈inria-00426469v2〉

Partager

Métriques

Consultations de la notice

136

Téléchargements de fichiers

78