Three Dimensional Proofnets for Classical Logic - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Preprints, Working Papers, ... Year : 2009

Three Dimensional Proofnets for Classical Logic

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.
Fichier principal
Vignette du fichier
3dnets.pdf (358.65 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00426469 , version 1 (26-10-2009)
inria-00426469 , version 2 (08-12-2009)

Identifiers

  • HAL Id : inria-00426469 , version 2

Cite

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

Share

Gmail Facebook X LinkedIn More