|
| | | | |
| | | |
| Stat |
Members: 3645
Articles: 2'504'928
Articles rated: 2609
25 April 2024 |
|
| | | | |
|
Article overview
| |
|
|
Sequentialization for full N-Graphs via sub-N-Graphs | | Ruan V. B. Carvalho
; Lais S. Andrade
; Anjolina G. de Oliveira
; Ruy J. G. B. de Queiroz
; | | Date: |
1 Mar 2018 | | Abstract: | Since proof-nets for MLL- were introduced by Girard (1987), several studies
have appeared dealing with its soundness proof. Bellin & Van de Wiele (1995)
produced an elegant proof based on properties of subnets (empires and kingdoms)
and Robinson (2003) proposed a straightforward generalization of this
presentation for proof-nets from sequent calculus for classical logic. In 2014
it was presented an extension of these studies to obtain a proof of the
sequentialization theorem for the fragment of N-Graphs with conjunction,
disjunction and negation connectives, via the notion of sub-N-Graphs. N-Graphs
is a symmetric natural deduction calculus with multiple conclusions that adopts
Danos-Regnier’s criterion and has defocussing switchable links. In this paper,
we present a sequentization for full propositional classical N-Graphs, showing
how to find a split node in the middle of the proof even with a global rule for
discharging hypothesis. | | Source: | arXiv, 1803.0555 | | Services: | Forum | Review | PDF | Favorites | |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
browser Mozilla/5.0 AppleWebKit/537.36 (KHTML, like Gecko; compatible; ClaudeBot/1.0; +claudebot@anthropic.com)
|
| |
|
|
|
|
News, job offers and information for researchers and scientists:
| |
REGISTER