nach oben

Journal of Automated Reasoning

Erschienen in:

22.05.2018

Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics

verfasst von: Matteo Acclavio

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Proof nets are a syntax for linear logic proofs which gives a coarser notion of proof equivalence with respect to syntactic equality together with an intuitive geometrical representation of proofs. In this paper we give an alternative 2-dimensional syntax for multiplicative linear logic derivations. The syntax of string diagrams authorizes the definition of a framework where the sequentializability of a term, i.e. deciding whether the term corresponds to a correct derivation, can be verified in linear time. Furthermore, we can use this syntax to define a denotational semantics for multiplicative linear logic with units by means of equivalence classes of proof diagrams modulo a terminating rewriting.

Vorheriger Artikel Linear Numeral Systems

Nächster Artikel QPCF: Higher-Order Languages and Quantum Circuits

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Abrusci, V.M.: Phase semantics and sequent calculus for pure noncommutative classical linear propositional logic. J. Symb. Logic 56(04), 1403–1451 (1991)MathSciNetCrossRef

Acclavio, M. : A complete proof of coherence for symmetric monoidal categories using rewriting. arXiv:1606.01722 (2016)

Acclavio, M.: Proof diagrams for multiplicative linear logic. arXiv:1606.09016 (2016)

John B.C., Lauda A.: A prehistory of n-categorical physics, pp. 13–128. Cambridge University Press, Cambridge (2011)

Burroni, A.: Higher-dimensional word problems with applications to equational logic. Theor. Comput. Sci. 115(1), 43–62 (1993)MathSciNetCrossRef

Danos, V., Regnier, L.: The structure of multiplicatives. Arch. Math. Logic 28(3), 181–203 (1989)MathSciNetCrossRef

De Falco, L.T.: Réseaux, cohérence et expériences obsessionnelles. Ph.D. thesis (2000)

Girard, J.-Y.: Linear logic. Theor. Comput. Sci. 50(1), 1–101 (1987)MathSciNetCrossRef

Girard, J.-Y.: A new constructive logic: classic logic. Math. Struct. Comput. Sci. 1(03), 255–296 (1991)CrossRef

10.

Girard, J.-Y.: Linear logic: its syntax and semantics. London Mathematical Society Lecture Note Series, pp. 1–42 (1995)

11.

Girard, J.-Y.: Proof-nets: the parallel syntax for proof-theory. Lecture Notes, Pure and Applied Mathematics, pp. 97–124 (1996)

12.

Guerrini, S., Masini, A.: Parsing MELL proof nets. Theor. Comput. Sci. 254(1), 317–335 (2001)MathSciNetCrossRef

13.

Guiraud, Y.: Termination orders for three-dimensional rewriting. J. Pure Appl. Algebra 207(2), 341–371 (2006)MathSciNetCrossRef

14.

Guiraud, Y: Catex Latex patch. https://www.irif.fr/~guiraud/catex/s (2007)

15.

Guiraud, Y., Malbos, P.: Higher-dimensional categories with finite derivation type. Theory Appl. Categ. 22(18), 420–478 (2009)MathSciNetMATH

16.

Heijltjes, W., Houston, R.: No proof nets for MLL with units: Proof equivalence in MLL is PSPACE-complete. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), p. 50. ACM, New York City (2014)

17.

Jimbo, M.: Introduction to the Yang–Baxter equation. Int. J. Mod. Phys. A 4(15), 3759–3777 (1989)MathSciNetCrossRef

18.

Joyal, André, Street, Ross: The geometry of tensor calculus I. Adv. Math. 88(1), 55–112 (1991)MathSciNetCrossRef

19.

Lafont, Y: From proof nets to interaction nets. London Mathematical Society Lecture Note Series, pp. 225–248 (1995)

20.

Lafont, Y.: Towards an algebraic theory of Boolean circuits. J. Pure Appl. Algebra 184(2), 257–310 (2003)MathSciNetCrossRef

21.

Mac Lane, S.: Categories for the Working Mathematician, vol. 5. Springer, Berlin (2013)MATH

22.

Mellies, P.-A.: Categorical semantics of linear logic. Interact. Models Comput. Program Behav. 27, 15–215 (2009)MathSciNetMATH

23.

Selinger, P.: A survey of graphical languages for monoidal categories. In: Coecke B. (ed.) New structures for physics. Lecture notes in Physics, vol 813, pp. 289–355. Springer, Berlin (2010)CrossRef

24.

Straßburger, L., Lamarche, F.: On proof nets for multiplicative linear logic with units. In: International Workshop on Computer Science Logic, pp. 145–159. Springer, Berlin (2004)CrossRef

25.

Street, R.: Limits indexed by category-valued 2-functors. J. Pure Appl. Algebra 8(2), 149–181 (1976)MathSciNetCrossRef

Titel: Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics
verfasst von: Matteo Acclavio
Publikationsdatum: 22.05.2018
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 4/2019
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-018-9466-4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 4/2019

Linear Numeral Systems

Efficient Active Automata Learning via Mutation Testing

Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants

Compositional Falsification of Cyber-Physical Systems with Machine Learning Components

QPCF: Higher-Order Languages and Quantum Circuits

Selected Extended Papers of NFM 2017: Preface