Hostname: page-component-7b7567c8c-mnklg Total loading time: 0 Render date: 2026-11-12T10:24:10.439Z Has data issue: false hasContentIssue false

Minimality of the correctness criterion for multiplicative proof nets

Published online by Cambridge University Press:  01 December 1998

DENIS BECHET
Affiliation:
5, Avenue Jean Monnet, 92160 Antony, France. Email: dbechet@club-internet.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

Almost a decade ago, Girard invented linear logic with the notion of a proof-net. Proof-nets are special graphs built from formulas, links and boxes. However, not all nets are proof-nets. First, they must be well constructed (we say that such graphs are proof-structures). Second, a proof-net is a proof-structure that corresponds to a sequential proof. It must satisfy a correctness criterion. One may wonder what this static criterion means for cut-elimination. We prove that every incorrect proof-structure (without cut) can be put in an environment where reductions lead to two kinds of basically wrong configurations: deadlocks and disconnected proof-structures. Thus, this proof says that there does not exist a bigger class of proof-structures than proof-nets where normalization does not lead to obviously bad configurations.

Information

Type
Research Article
Copyright
© 1998 Cambridge University Press