Abstract
Since proof-nets for MLL- were introduced by Girard (1987), several studies have been made on 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. This paper extends these studies to obtain a proof of sequentialization theorem for N-Graphs, which is a symmetric natural deduction calculus for classical propositional logic that adopts Danos-Regnier's criteria and has defocussing switchable links, via sub-N-Graphs. © 2014 Springer-Verlag.
Author supplied keywords
Cite
CITATION STYLE
Carvalho, R., Andrade, L., De Oliveira, A., & De Queiroz, R. (2014). Sequentialization for N-graphs via sub-N-graphs. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8652 LNCS, pp. 94–108). Springer Verlag. https://doi.org/10.1007/978-3-662-44145-9_7
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
