Linear logic: Difference between revisions

Revision as of 19:02, 4 January 2021

Revision as of 15:13, 6 January 2021

Line 1:

{{shortShort description|System of resource-aware logic}}

{{Redirect|⅋|the EP|⅋ (EP)}}

'''Linear logic''' is a [[substructural logic]] proposed by [[Jean-Yves Girard]] as a refinement of [[classical logic|classical]] and [[intuitionistic logic]], joining the [[Duality (mathematics)|dualities]] of the former with many of the [[Constructivism (mathematics)|constructive]] properties of the latter.<ref>{{cite journal|last1=Girard|first1=Jean-Yves|year=1987|title=Linear logic|url=http://girard.perso.math.cnrs.fr/linear.pdf|journal=Theoretical Computer Science|volume=50|issue=1|pages=1–102|doi=10.1016/0304-3975(87)90045-4|hdl=10338.dmlcz/120513|author1-link=Jean-Yves Girard}}</ref> Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as [[programming languages]], [[game semantics]], and [[quantum physics]] (because linear logic can be seen as the logic of [[quantum information theory]]),<ref>{{cite journal|first1=John|last1=Baez|author1-link=John Baez|first2=Mike|last2=Stay|year=2008|title=Physics, Topology, Logic and Computation: A Rosetta Stone|editor=[[Bob Coecke]]|editor-link=Bob Coecke|journal=New Structures of Physics|url=http://math.ucr.edu/home/baez/rosetta.pdf}}</ref> as well as [[linguistics]],<ref>{{cite book|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|first1=V.|last1=de Paiva|author1-link= Valeria de Paiva |first2=J.|last2=van Genabith|first3=E.|last3=Ritter|year=1999|url=http://www.dagstuhl.de/Reports/99/99341.pdf}}</ref> particularly because of its emphasis on resource-boundedness, duality, and interaction.

{{short description|System of resource-aware logic}}

'''Linear logic''' is a [[substructural logic]] proposed by [[Jean-Yves Girard]] as a refinement of [[classical logic|classical]] and [[intuitionistic logic]], joining the [[Duality (mathematics)|dualities]] of the former with many of the [[Constructivism (mathematics)|constructive]] properties of the latter.<ref>{{cite journal|last1=Girard|first1=Jean-Yves|year=1987|title=Linear logic|url=http://girard.perso.math.cnrs.fr/linear.pdf|journal=Theoretical Computer Science|volume=50|issue=1|pages=1–102|doi=10.1016/0304-3975(87)90045-4|hdl=10338.dmlcz/120513|author1-link=Jean-Yves Girard}}</ref> Although the logic has also been studied for its own sake, more broadly, ideas from linear logic have been influential in fields such as [[programming languages]], [[game semantics]], and [[quantum physics]] (because linear logic can be seen as the logic of [[quantum information theory]]),<ref>{{cite journal|first1=John|last1=Baez|author1-link=John Baez|first2=Mike|last2=Stay|year=2008|title=Physics, Topology, Logic and Computation: A Rosetta Stone|editor=[[Bob Coecke]]|journal=New Structures of Physics|url=http://math.ucr.edu/home/baez/rosetta.pdf}}</ref> as well as [[linguistics]],<ref>{{cite book|title=Dagstuhl Seminar 99341 on Linear Logic and Applications|first1=V.|last1=de Paiva|author1-link= Valeria de Paiva |first2=J.|last2=van Genabith|first3=E.|last3=Ritter|year=1999|url=http://www.dagstuhl.de/Reports/99/99341.pdf}}</ref> particularly because of its emphasis on resource-boundedness, duality, and interaction.

Linear logic lends itself to many different presentations, explanations and intuitions.

Line 455:

=== Algebraic semantics ===

{{seeSee also|Quantale}}

==Decidability/complexity of entailment==

Line 512:

==External links==

*{{CommonscatCommons category-inline}}

*[https://web.archive.org/web/20160404181455/http://bach.istc.kobe-u.ac.jp/llprover/ A Linear Logic Prover (llprover)], available for use online, from: Naoyuki Tamura / Dept of CS / Kobe University / Japan