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

https://hal.inria.fr/inria-00426469
Contributor : Clement Houtmann <>
Submitted on : Tuesday, December 8, 2009 - 3:09:53 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM
Long-term archiving on: : Saturday, November 26, 2016 - 3:38:30 PM

File

3dnets.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00426469, version 2

Collections

Citation

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

Share

Metrics

Record views

171

Files downloads

121