In proof theory, proof nets are a geometrical method of representing proofs thateliminates two forms of bureaucracy that differentiate proofs: (A) irrelevant syntactical features of regular proof calculi, and (B) the order of rules applied in a derivation. In this way, the formal properties of proof identity correspond more closely to the intuitively desirable properties. Proof nets were introduced by Jean-Yves Girard. This distinguishes proof nets from regular proof calculi such as the natural deduction calculus and the sequent calculus, where these phenomena are present.
Attributes | Values |
---|
rdfs:label
| - Réseau de preuves (fr)
- Proof net (en)
|
rdfs:comment
| - Les réseaux de preuves, inventés par le logicien Jean-Yves Girard en 1986 dans le cadre de la logique linéaire, sont un outil de démonstration formel pour cette même logique (c'est-à-dire une alternative aux séquents qui sont aussi employés en logique classique et intuitionniste). Grossièrement, il s'agit d'un équivalent de la déduction naturelle de la logique intuitionniste adaptée à la logique linéaire. Ils s'en différencient cependant par le caractère géométrique de cette approche : une preuve est formée par un hypergraphe et le critère de correction peut s'exprimer comme un parcours de graphe. (fr)
- In proof theory, proof nets are a geometrical method of representing proofs thateliminates two forms of bureaucracy that differentiate proofs: (A) irrelevant syntactical features of regular proof calculi, and (B) the order of rules applied in a derivation. In this way, the formal properties of proof identity correspond more closely to the intuitively desirable properties. Proof nets were introduced by Jean-Yves Girard. This distinguishes proof nets from regular proof calculi such as the natural deduction calculus and the sequent calculus, where these phenomena are present. (en)
|
dcterms:subject
| |
Wikipage page ID
| |
Wikipage revision ID
| |
Link from a Wikipage to another Wikipage
| |
Link from a Wikipage to an external page
| |
sameAs
| |
dbp:wikiPageUsesTemplate
| |
has abstract
| - Les réseaux de preuves, inventés par le logicien Jean-Yves Girard en 1986 dans le cadre de la logique linéaire, sont un outil de démonstration formel pour cette même logique (c'est-à-dire une alternative aux séquents qui sont aussi employés en logique classique et intuitionniste). Grossièrement, il s'agit d'un équivalent de la déduction naturelle de la logique intuitionniste adaptée à la logique linéaire. Ils s'en différencient cependant par le caractère géométrique de cette approche : une preuve est formée par un hypergraphe et le critère de correction peut s'exprimer comme un parcours de graphe. (fr)
- In proof theory, proof nets are a geometrical method of representing proofs thateliminates two forms of bureaucracy that differentiate proofs: (A) irrelevant syntactical features of regular proof calculi, and (B) the order of rules applied in a derivation. In this way, the formal properties of proof identity correspond more closely to the intuitively desirable properties. Proof nets were introduced by Jean-Yves Girard. This distinguishes proof nets from regular proof calculi such as the natural deduction calculus and the sequent calculus, where these phenomena are present. For instance, these two linear logic proofs are identical: And their corresponding nets will be the same. (en)
|
prov:wasDerivedFrom
| |
page length (characters) of wiki page
| |
foaf:isPrimaryTopicOf
| |
is Link from a Wikipage to another Wikipage
of | |
is Wikipage redirect
of | |
is known for
of | |
is known for
of | |
is foaf:primaryTopic
of | |