Abstract.
We propose a connection-based characterization of the multiplicative fragment of non-commutative logic (MNL), that is a conservative extension of both commutative (MLL) and non-commutative or cyclic (MCyLL) linear logic. It is based on a characterization for MLL together with the introduction of labels and constraints from a formula polarization process. We also study a similar characterization for the intuitionistic fragment of MNL. Finally, we consider the relationships between these results and proof nets construction in MNL based on labels and constraints.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abrusci, M., Ruet, P.: Non-commutative logic I: the multiplicative fragment. Annals of Pure and Applied Logic 101, 29–64 (2000)
Andreoli, J.M.: Focussing and Proof construction. Annals of Pure and Applied Logic 107, 131–163 (2001)
Andreoli, J.M.: Focusing proof-net construction as a middleware paradigm. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 501–516. Springer, Heidelberg (2002)
Faggian, C.: Proof construction and non-commutativity: a cluster calculus. In: International Conference on Principles and Practice of Declarative Programming, PPDP 2000. ACM Press, New York (2000)
Galmiche, D.: Connection Methods in Linear Logic and Proof nets Construction. Theoretical Computer Science 232(1-2), 231–272 (2000)
Galmiche, D., Méry, D.: Connection-based proof search in propositional BI logic. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 111–128. Springer, Heidelberg (2002)
Galmiche, D., Notin, J.M.: Proof-search and Proof nets in Mixed Linear Logic. Electronic Notes in Theoretical Computer Science 37 (2000)
Galmiche, D., Notin, J.M.: Calculi with Dependency Relations for Mixed Linear Logic. In: International Workshop on Logic and Complexity in Computer Science, LCCS 2001, Créteil, France, pp. 81–102 (2001)
Galmiche, D., Perrier, G.: A procedure for automatic proof nets construction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 42–53. Springer, Heidelberg (1992)
Girard, J.Y.: Linear Logic: its Syntax and Semantics. In: Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 1–42. Cambridge University Press, Cambridge (1995)
Girard, J.Y.: Proof nets: the parallel syntax for proof theory. In: Ursini, A., Agliano, P. (eds.) Logic and Algebra. M. Dekker, New York (1995)
Gray, D., Hamilton, G., Power, J., Sinclair, D.: Specifying and verifying TCP/IP using Mixed Intuitionistic Linear Logic. Technical report, Dublin City Univ. (2001)
Kreitz, C., Mantel, H., Otten, J., Schmitt, S.: Connection-based proof construction in Linear Logic. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 207–221. Springer, Heidelberg (1997)
Mogbil, V.: Quadratic correctness criterion for non commutative logic. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 69–83. Springer, Heidelberg (2001)
Murawski, S., Ong, C.-H.L.: Dominator trees and fast verification of proof net. In: 15th IEEE Symposium on Logic in Computer Science, Santa Barbara, California (June 2000)
O’Hearn, P.W., Pym, D.: The Logic of Bunched Implications. Bulletin of Symbolic Logic 5(2), 215–244 (1999)
Ruet, P.: Non-commutative logic II: sequent calculus and phase semantics. Math. Struct. in Comp. Science 10, 277–312 (2000)
Ruet, P., Fages, F.: Concurrent constraint programming and non-commutative logic. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 406–423. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Galmiche, D., Notin, J.M. (2003). Connection-Based Proof Construction in Non-commutative Logic. In: Vardi, M.Y., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2003. Lecture Notes in Computer Science(), vol 2850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39813-4_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-39813-4_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20101-4
Online ISBN: 978-3-540-39813-4
eBook Packages: Springer Book Archive