Three Dimensional Proofnets for Classical Logic

Clement Houtmann (1)

1 PAREO - Formal islands: foundations and applications

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.

Mots clés: Proofnets; Classical Logic; Sequent Calculus

Domaines: Logique en informatique [cs.LO]

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