Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Clement Houtmann Connect in order to contact the contributor
Submitted on : Tuesday, December 8, 2009 - 3:09:53 PM
Last modification on : Wednesday, February 2, 2022 - 3:51:39 PM
Long-term archiving on: : Saturday, November 26, 2016 - 3:38:30 PM


Files produced by the author(s)


  • HAL Id : inria-00426469, version 2



Clement Houtmann. Three Dimensional Proofnets for Classical Logic. 2009. ⟨inria-00426469v2⟩



Record views


Files downloads