Hostname: page-component-cd9895bd7-hc48f Total loading time: 0 Render date: 2024-12-28T13:52:41.739Z Has data issue: false hasContentIssue false
  • English
  • Français

A new correctness criterion for the proof nets of non-commutative multiplicative linear logics

Published online by Cambridge University Press:  12 March 2014

Misao Nagayama  and
Mitsuhiro Okada
Misao Nagayama
Affiliation:
Tokyo Woman's Christian University, Department of Mathematics, Suginami-Ku, Tokyo, Japan, E-Mail: [email protected]
Mitsuhiro Okada
Affiliation:
Keio University, Department of Philosophy, Keio, Japan, E-Mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract.

This paper presents a new correctness criterion for marked Danos-Reginer graphs (D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL.

As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 66 , Issue 4 , December 2001 , pp. 1524 - 1542
Copyright
Copyright © Association for Symbolic Logic 2001

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Abrusci, V. M., Non-commutative proof nets. Advances in Linear Logic. London Mathematical Society Lecture Notes, vol. 222, 1995, pp. 271–296.CrossRefGoogle Scholar
[2]Abrusci, V. M. and Ruet, P., Non-commutative logic I: The multiplicative fragment. Annals of Pure and Applied Logic, (1999).CrossRefGoogle Scholar
[3]Danos, V., La Logique Linéaire appliquée a l'étude de divers processus de normalisation (principalement du X-calcul), Ph.D. thesis. Université de Paris 7, 1990.Google Scholar
[4]Danos, V. and Regnier, L., The structure of multiplicatives. Archive for Mathematical Logic, vol. 28 (1989), pp. 181–203.CrossRefGoogle Scholar
[5]Even, S., Graph Algorithms. Pitman Publishing Ltd., 1979.Google Scholar
[6]Girard, J.-Y., Linear Logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.CrossRefGoogle Scholar
[7]Guerrini, S., Correctness of multiplicative Proof nets is linear. Proceedings for 14th Annual IEEE Symposium on Logic in Computer Science, 1999.Google Scholar
[8]Lafont, Y., From Proof-Nets to Interaction Nets, Advances in Linear Logic, London Mathematical Society Lecture Notes, vol. 222, 1995, pp. 225–247.CrossRefGoogle Scholar
[9]Lambek, J., The mathematics of sentence structure, American Mathematical Monthly, vol. 65 (1958), pp. 154–170.CrossRefGoogle Scholar
[10]Metayer, F., Exchange and Cyclic Linear Logic. Electronic Note of Theoretical Computer Science (Specialissue on Linear Logic 96 Tokyo Meeting), vol. 3 (1996).Google Scholar
[11]Nagayama, M. and Okada, M., A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic. Theoretical Computer Science, to appear.Google Scholar
[12]Nagayama, M. and Okada, M., A graph-theoretic characterization theorem for multiplicative fragment of non-commutative linear logic (Extended abstract). Electronic Note of Theoretical Computer Science (Special issue on Linear Logic 96 Tokyo Meeting), vol. 3 (1996).Google Scholar
[13]Nagayama, M. and Okada, M., Characterization theorems for multiplicative fragment of intuitionistic non-commutative linear logic, Preoceedings of RIMS, 1997, Preliminary Report, pp. 55–69.Google Scholar
[14]Roorda, D., Proof nets for Lambek Calculus, Journal of Logic and Computation, vol. 2 (1992), pp. 211–231.CrossRefGoogle Scholar
[15]Ruet, P.. Non-commutative logic II: Sequent calculus and phase semantics. Mathematical structures in computer science. 1999.Google Scholar
[16]Yetter, D. N., Quantales and (non-commutative) linear logic, this Journal, vol. 55 (1990), pp. 41–64.Google Scholar