La lógica lineal es una lógica subestructural propuesta por Jean-Yves Girard como un refinamiento de la lógica clásica e intuicionista , uniendo las dualidades de la primera con muchas de las propiedades constructivas de la segunda. [1] Aunque la lógica también se ha estudiado por sí misma, en términos más generales, las ideas de la lógica lineal han influido en campos como los lenguajes de programación , la semántica de juegos y la física cuántica (porque la lógica lineal puede verse como la lógica de la lógica cuántica). teoría de la información ), [2] así comolingüística , [3] particularmente debido a su énfasis en la limitación de recursos, la dualidad y la interacción.
La lógica lineal se presta a muchas presentaciones, explicaciones e intuiciones diferentes. En teoría , se deriva de un análisis del cálculo secuencial clásico en el que se controlan cuidadosamente los usos de la contracción y el debilitamiento (de las reglas estructurales ) . Desde el punto de vista operativo, esto significa que la deducción lógica ya no se trata simplemente de una colección en constante expansión de "verdades" persistentes, sino también de una forma de manipular recursos que no siempre pueden duplicarse o desecharse a voluntad. En términos de modelos denotacionales simples , se puede considerar que la lógica lineal refina la interpretación de la lógica intuicionista reemplazando categorías cartesianas (cerradas) por categorías simétricas monoidales (cerradas) , o la interpretación de la lógica clásica reemplazando las álgebras booleanas por álgebras C * . [ cita requerida ]
Conectividad, dualidad y polaridad
Sintaxis
El lenguaje de la lógica lineal clásica (CLL) se define inductivamente por la notación BNF
A | :: = | p ∣ p ⊥ |
∣ | A ⊗ A ∣ A ⊕ A | |
∣ | A y A ∣ A ⅋ A | |
∣ | 1 ∣ 0 ∣ ⊤ ∣ ⊥ | |
∣ | ! ¿A ∣? A |
Aquí p y p ⊥ se extienden sobre átomos lógicos . Por razones que se explicarán a continuación, las conectivas ⊗, ⅋, 1 y ⊥ se llaman multiplicativas , las conectivas &, ⊕, ⊤ y 0 se llaman aditivos , ¡y las conectivas! y ? se llaman exponenciales . Además, podemos emplear la siguiente terminología:
Símbolo | Nombre | ||
---|---|---|---|
⊗ | conjunción multiplicativa | veces | tensor |
⊕ | disyunción aditiva | más | |
Y | conjunción aditiva | con | |
⅋ | disyunción multiplicativa | par | |
! | por supuesto | estallido | |
? | Por qué no |
Los conectivos binarios ⊗, ⊕, & y ⅋ son asociativos y conmutativos; 1 es la unidad de ⊗, 0 es la unidad de ⊕, ⊥ es la unidad de ⅋ y ⊤ es la unidad de &.
Cada proposición A en CLL tiene un doble A ⊥ , definido de la siguiente manera:
( p ) ⊥ = p ⊥ | ( p ⊥ ) ⊥ = p | ||||
( UNA ⊗ B ) ⊥ = UNA ⊥ ⅋ B ⊥ | ( UNA ⅋ B ) ⊥ = UNA ⊥ ⊗ B ⊥ | ||||
( A ⊕ B ) ⊥ = A ⊥ y B ⊥ | ( A y B ) ⊥ = A ⊥ ⊕ B ⊥ | ||||
(1) ⊥ = ⊥ | (⊥) ⊥ = 1 | ||||
(0) ⊥ = ⊤ | (⊤) ⊥ = 0 | ||||
(! A ) ⊥ =? ( A ⊥ ) | (? A ) ⊥ =! ( A ⊥ ) |
agregar | mul | Exp | |
---|---|---|---|
pos | ⊕ 0 | ⊗ 1 | ! |
neg | & ⊤ | ⅋ ⊥ | ? |
Observe que (-) ⊥ es una involución , es decir, A ⊥⊥ = A para todas las proposiciones. A ⊥ es también llamada la negación lineal de A .
Las columnas de la tabla sugieren otra forma de clasificar las conectivas de la lógica lineal, denominada polaridad : las conectivas negadas en la columna de la izquierda (⊗, ⊕, 1, 0 ,! ) Se denominan positivas , mientras que sus dobles de la derecha (⅋, &, ⊥, ⊤,?) Se denominan negativos ; cf. mesa de la derecha.
Implicación lineal no está incluido en la gramática de conectivas, pero es definible en la LLC usando negación lineal y disyunción multiplicativo, por A ⊸ B : = A ⊥ ⅋ B . El conectivo ⊸ a veces se pronuncia " piruleta ", debido a su forma.
Presentación de cálculo secuencial
Una forma de definir la lógica lineal es como un cálculo secuencial . Usamos las letras Γ y Δ para abarcar la lista de proposiciones A 1 , ..., A n , también llamadas contextos . Un secuente coloca un contexto a la izquierda y a la derecha del torniquete , escrito ΓΔ . Intuitivamente, el secuente afirma que la conjunción de Γ implica la disyunción de Δ (aunque nos referimos a la conjunción y disyunción "multiplicativas", como se explica a continuación). Girard describe la lógica lineal clásica usando solo secuencias unilaterales (donde el contexto de la izquierda está vacío), y seguimos aquí esa presentación más económica. Esto es posible porque cualquier local a la izquierda de un torniquete siempre se puede mover al otro lado y dualizar.
Ahora damos reglas de inferencia que describen cómo construir pruebas de secuentes. [4]
Primero, para formalizar el hecho de que no nos importa el orden de las proposiciones dentro de un contexto, agregamos la regla estructural de intercambio :
Γ, A 1 , A 2 , Δ |
Γ, A 2 , A 1 , Δ |
Tenga en cuenta que no agregamos las reglas estructurales de debilitamiento y contracción, porque nos importa la ausencia de proposiciones en una secuencia y el número de copias presentes.
A continuación, agregamos secuencias y cortes iniciales :
|
|
La regla de corte puede verse como una forma de componer pruebas, y las secuencias iniciales sirven como unidades para la composición. En cierto sentido, estas reglas son redundantes: a medida que introducimos reglas adicionales para construir pruebas a continuación, mantendremos la propiedad de que las secuencias iniciales arbitrarias pueden derivarse de las secuencias iniciales atómicas, y que siempre que se pueda demostrar una secuencia, se le puede dar un corte. prueba gratis. En última instancia, esta propiedad de forma canónica (que se puede dividir en la completitud de las secuencias iniciales atómicas y el teorema de eliminación de cortes , que induce una noción de prueba analítica ) se encuentra detrás de las aplicaciones de la lógica lineal en la informática, ya que permite que la lógica sea se utiliza en la búsqueda de pruebas y como cálculo lambda consciente de los recursos .
Ahora, explicamos las conectivas dando reglas lógicas . Típicamente, en el cálculo secuencial uno da tanto "reglas de derecha" como "reglas de izquierda" para cada conectivo, esencialmente describiendo dos modos de razonamiento sobre proposiciones que involucran ese conectivo (por ejemplo, verificación y falsificación). En una presentación unilateral, en cambio, se hace uso de la negación: las reglas de la derecha para un conectivo (digamos ⅋) efectivamente juegan el papel de las reglas de la izquierda para su dual (⊗). Por tanto, deberíamos esperar una cierta "armonía" entre la (s) regla (s) para un conectivo y la (s) regla (s) para su dual.
Multiplicativos
Las reglas para la conjunción multiplicativa (⊗) y la disyunción (⅋):
|
|
y para sus unidades:
|
|
Observe que las reglas para la conjunción multiplicativa y la disyunción son admisibles para la conjunción simple y la disyunción bajo una interpretación clásica (es decir, son reglas admisibles en LK ).
Aditivos
Las reglas para la conjunción aditiva (&) y la disyunción (⊕):
|
|
|
y para sus unidades:
| (sin regla para 0 ) |
Observe que las reglas para la conjunción aditiva y la disyunción son nuevamente admisibles bajo una interpretación clásica. Pero ahora podemos explicar la base de la distinción multiplicativo / aditivo en las reglas para las dos versiones diferentes de conjunción: para el conectivo multiplicativo (⊗), el contexto de la conclusión ( Γ, Δ ) se divide entre las premisas, mientras que para el caso aditivo conectivo (&) el contexto de la conclusión ( Γ ) se lleva completo a ambas premisas.
Exponenciales
Las exponenciales se utilizan para dar acceso controlado al debilitamiento y la contracción. Específicamente, agregamos reglas estructurales de debilitamiento y contracción para las proposiciones? D: [5]
|
|
y utilice las siguientes reglas lógicas:
|
|
Se podría observar que las reglas para las exponenciales siguen un patrón diferente de las reglas para las otras conectivas, asemejándose a las reglas de inferencia que gobiernan las modalidades en las formaciones de cálculo secuenciales de la lógica modal normal S4, y que ya no existe una simetría tan clara entre las duales! y ?. Esta situación se remedia con presentaciones alternativas de CLL (por ejemplo, la presentación LU ).
Fórmulas notables
Además de las dualidades de De Morgan descritas anteriormente, algunas equivalencias importantes en lógica lineal incluyen:
- Distributividad
A ⊗ ( B ⊕ C ) ≣ ( A ⊗ B ) ⊕ ( A ⊗ C ) |
( A ⊕ B ) ⊗ C ≣ ( A ⊗ C ) ⊕ ( B ⊗ C ) |
A ⅋ ( B y C ) ≣ ( A ⅋ B ) y ( A ⅋ C ) |
( A y B ) ⅋ C ≣ ( A ⅋ C ) y ( B ⅋ C ) |
Por definición de A ⊸ B como A ⊥ ⅋ B , las dos últimas leyes de distributividad también dan:
A ⊸ ( B y C ) ≣ ( A ⊸ B ) y ( A ⊸ C ) |
( A ⊕ B ) ⊸ C ≣ ( A ⊸ C ) y ( B ⊸ C ) |
(Aquí A ≣ B es ( A ⊸ B ) y ( B ⊸ A ) .)
- Isomorfismo exponencial
! ( A y B ) ≣! ¡A ⊗! B |
? ( A ⊕ B ) ≣? ¿A ⅋? B |
- Distribuciones lineales
Un mapa que no es un isomorfismo pero que juega un papel crucial en la lógica lineal es:
( A ⊗ ( B ⅋ C )) ⊸ (( A ⊗ B ) ⅋ C ) |
Las distribuciones lineales son fundamentales en la teoría de la prueba de la lógica lineal. Las consecuencias de este mapa se investigaron por primera vez en [6] y se denominaron "distribución débil". En trabajos posteriores se le cambió el nombre a "distribución lineal" para reflejar la conexión fundamental con la lógica lineal.
- Otras implicaciones
Las siguientes fórmulas de distributividad no son en general una equivalencia, solo una implicación:
! ¡A ⊗! B ⊸! ( A ⊗ B ) |
! ¡A ⊕! B ⊸! ( A ⊕ B ) |
? ( A ⅋ B ) ⊸? ¿A ⅋? B |
? ( A y B ) ⊸? A &? B |
( A y B ) ⊗ C ⊸ ( A ⊗ C ) y ( B ⊗ C ) |
( A y B ) ⊕ C ⊸ ( A ⊕ C ) y ( B ⊕ C ) |
( UNA ⅋ C ) ⊕ ( B ⅋ C ) ⊸ ( A ⊕ B ) ⅋ C |
( A y C ) ⊕ ( B y C ) ⊸ ( A ⊕ B ) y C |
Codificación de lógica clásica / intuicionista en lógica lineal
Tanto la implicación intuicionista como la clásica se pueden recuperar de la implicación lineal insertando exponenciales: la implicación intuicionista se codifica como ! A ⊸ B , mientras que la implicación clásica se puede codificar como !? ¿A ⊸? B o ! ¡¿Un ⊸?! B (o una variedad de posibles traducciones alternativas). [7] La idea es que las exponenciales nos permiten usar una fórmula tantas veces como sea necesario, lo que siempre es posible en la lógica clásica e intuicionista.
Formalmente, existe una traducción de fórmulas de lógica intuicionista a fórmulas de lógica lineal de una manera que garantiza que la fórmula original sea demostrable en lógica intuicionista si y solo si la fórmula traducida es demostrable en lógica lineal. Usando la traducción negativa de Gödel-Gentzen , podemos incrustar la lógica clásica de primer orden en la lógica lineal de primer orden.
La interpretación de recursos
Lafont (1993) mostró por primera vez cómo la lógica lineal intuicionista puede explicarse como una lógica de recursos, proporcionando así al lenguaje lógico acceso a formalismos que pueden usarse para razonar sobre recursos dentro de la lógica misma, en lugar de, como en la lógica clásica, mediante por medio de relaciones y predicados no lógicos. El ejemplo clásico de Tony Hoare (1985) de la máquina expendedora puede utilizarse para ilustrar esta idea.
Suponga que representamos tener una barra de chocolate por la proposición atómica de caramelo y tener un dólar por $ 1 . Para afirmar el hecho de que un dólar le comprará una barra de chocolate, podríamos escribir la implicación $ 1 ⇒ caramelo . Pero en la lógica ordinaria (clásica o intuicionista), a partir de una y un ⇒ B se puede concluir A ∧ B . Entonces, ¡la lógica ordinaria nos lleva a creer que podemos comprar la barra de chocolate y mantener nuestro dólar! Por supuesto, podemos evitar este problema usando codificaciones más sofisticadas, [ aclaración necesaria ] aunque típicamente tales codificaciones adolecen del problema del marco . Sin embargo, el rechazo del debilitamiento y la contracción permite que la lógica lineal evite este tipo de razonamiento espurio incluso con la regla "ingenua". En lugar de $ 1 ⇒ caramelo , expresamos la propiedad de la máquina expendedora como una implicación lineal $ 1 ⊸ caramelo . De $ 1 y este hecho, podemos concluir dulces , pero no $ 1 ⊗ dulces . En general, podemos utilizar la proposición lógica lineal A ⊸ B para expresar la validez de la transformación de recursos A en recurso B .
Siguiendo el ejemplo de la máquina expendedora, considere las "interpretaciones de recursos" de los otros conectivos multiplicativos y aditivos. (Las exponenciales proporcionan los medios para combinar esta interpretación de recursos con la noción habitual de verdad lógica persistente ).
La conjunción multiplicativa ( A ⊗ B ) denota la ocurrencia simultánea de recursos, para ser utilizados como lo indique el consumidor. Por ejemplo, si compra una barra de chicle y una botella de refresco, entonces está solicitando chicle ⊗ bebida . La constante 1 denota la ausencia de cualquier recurso, por lo que funciona como la unidad de ⊗.
La conjunción aditiva ( A y B ) representa la ocurrencia alternativa de recursos, cuya elección controla el consumidor. Si en la máquina expendedora hay un paquete de papas fritas, una barra de chocolate y una lata de refresco, cada uno cuesta un dólar, entonces por ese precio puede comprar exactamente uno de estos productos. Por lo tanto escribimos $ 1 ⊸ ( dulces y patatas fritas y bebida ) . Nosotros no escribimos $ 1 ⊸ ( dulces ⊗ fichas ⊗ bebida ) , lo que implicaría que basta un dólar para la compra de los tres productos juntos. Sin embargo, a partir de $ 1 ⊸ ( dulces y patatas fritas y bebida ) , podemos deducir correctamente $ 3 ⊸ ( dulces ⊗ fichas ⊗ bebida ) , donde $ 3 : = $ 1 ⊗ $ 1 ⊗ $ 1 . La unidad ⊤ de conjunción aditiva puede verse como una papelera de recursos innecesarios. Por ejemplo, podemos escribir $ 3 ⊸ ( caramelo ⊗ ⊤) para expresar que con tres dólares puedes conseguir una barra de chocolate y algunas otras cosas, sin ser más específico (por ejemplo, papas fritas y una bebida, o $ 2, o $ 1 y papas fritas , etc.).
La disyunción aditiva ( A ⊕ B ) representa la ocurrencia alternativa de recursos, cuya elección controla la máquina. Por ejemplo, suponga que la máquina expendedora permite el juego: inserte un dólar y la máquina puede dispensar una barra de chocolate, un paquete de papas fritas o un refresco. Podemos expresar esta situación como $ 1 ⊸ ( caramelo ⊕ patatas fritas ⊕ bebida ) . La constante 0 representa un producto que no se puede fabricar y, por lo tanto, sirve como unidad de ⊕ (una máquina que podría producir A o 0 es tan buena como una máquina que siempre produce A porque nunca logrará producir un 0). Entonces, a diferencia de lo anterior, no podemos deducir $ 3 ⊸ ( dulces ⊗ chips ⊗ bebida ) de esto.
Disyunción multiplicativa ( A ⅋ B ) es más difícil de brillo en términos de la interpretación de recursos, aunque podemos codificar de nuevo en implicación lineal, ya sea como A ⊥ ⊸ B o B ⊥ ⊸ A .
Otros sistemas de prueba
Redes de prueba
Introducidas por Jean-Yves Girard , las redes de prueba se han creado para evitar la burocracia , es decir, todas las cosas que hacen que dos derivaciones sean diferentes en el punto de vista lógico, pero no en el punto de vista "moral".
Por ejemplo, estas dos pruebas son "moralmente" idénticas:
|
|
El objetivo de las redes de prueba es hacerlas idénticas creando una representación gráfica de ellas.
Semántica
Semántica algebraica
Decidibilidad / complejidad de la vinculación
La relación de vinculación en la CLL completa es indecidible . [8] Al considerar fragmentos de CLL, el problema de decisión tiene una complejidad variable:
- Lógica lineal multiplicativa (MLL): solo las conectivas multiplicativas. La implicación MLL es NP-completa , incluso restringida a cláusulas de Horn en el fragmento puramente implicativo, [9] oa fórmulas libres de átomos. [10]
- Lógica lineal multiplicativa-aditiva (MALL): solo multiplicativos y aditivos (es decir, libre de exponenciales). La vinculación de MALL está completa con PSPACE . [8]
- Lógica lineal multiplicativa-exponencial (MELL): solo multiplicativos y exponenciales. Al reducir el problema de la accesibilidad para las redes de Petri , [11] la vinculación MELL debe ser al menos EXPSPACE-hard , aunque la decidibilidad en sí ha tenido el estatus de un problema abierto de larga data. En 2015, se publicó una prueba de decidibilidad en la revista TCS , [12] pero luego se demostró que era errónea. [13]
- En 1995 se demostró que la lógica lineal afín (es decir, lógica lineal con debilitamiento, una extensión en lugar de un fragmento) era decidible. [14]
Variantes
Muchas variaciones de la lógica lineal surgen al seguir jugando con las reglas estructurales:
- Lógica afín , que prohíbe la contracción pero permite el debilitamiento global (una extensión decidible).
- Lógica estricta o lógica relevante , que prohíbe el debilitamiento pero permite la contracción global.
- Lógica no conmutativa o lógica ordenada, que elimina la regla del intercambio, además de prohibir el debilitamiento y la contracción. En la lógica ordenada, la implicación lineal se divide aún más en implicación izquierda e implicación derecha.
Se han considerado diferentes variantes intuicionistas de la lógica lineal. Cuando se basa en una presentación de cálculo secuencial de conclusión única, como en ILL (lógica lineal intuicionista), las conectivas ⅋, ⊥ y? están ausentes, y la implicación lineal se trata como un conectivo primitivo. En FILL (lógica lineal intuicionista completa) las conectivas, ⊥ y? están presentes, la implicación lineal es un conectivo primitivo y, de manera similar a lo que sucede en la lógica intuicionista, todos los conectivos (excepto la negación lineal) son independientes. También hay extensiones de la lógica lineal de primer orden y de orden superior , cuyo desarrollo formal es algo estándar (ver lógica de primer orden y lógica de orden superior ).
Ver también
- Sistema de tipo lineal , un sistema de tipo subestructura
- Lógica de la unidad (LU)
- Redes de prueba
- Geometría de interacción
- Semántica del juego
- Lógica intuicionista
- Lógica de computabilidad
- Lúdicos
- Espacios Chu
- Tipo de unicidad
- Programación lógica lineal
Referencias
- ^ Girard, Jean-Yves (1987). "Lógica lineal" (PDF) . Informática Teórica . 50 (1): 1–102. doi : 10.1016 / 0304-3975 (87) 90045-4 . hdl : 10338.dmlcz / 120513 .
- ^ Báez, Juan ; Quédate, Mike (2008). Bob Coecke (ed.). "Física, topología, lógica y computación: una piedra de Rosetta" (PDF) . Nuevas estructuras de la física .
- ^ de Paiva, V .; van Genabith, J .; Ritter, E. (1999). Seminario Dagstuhl 99341 sobre lógica lineal y aplicaciones (PDF) .
- ↑ Girard (1987), p.22, Def.1.15
- ↑ Girard (1987), p.25-26, Def.1.21
- ^ J. Robin Cockett y Robert Seely "Categorías débilmente distributivas" Diario de álgebra pura y aplicada 114 (2) 133-173, 1997
- ^ Di Cosmo, Roberto. La cartilla de lógica lineal . Notas del curso; Capitulo 2.
- ^ a b Para obtener este resultado y la discusión de algunos de los fragmentos a continuación, consulte: Lincoln, Patrick; Mitchell, John; Scedrov, Andre; Shankar, Natarajan (1992). "Problemas de decisión para la lógica lineal proposicional" . Anales de lógica pura y aplicada . 56 (1-3): 239-311. doi : 10.1016 / 0168-0072 (92) 90075-B .
- ^ Kanovich, Max I. (22 de junio de 1992). "La programación de la bocina en lógica lineal es NP-completa". Séptimo Simposio Anual de IEEE sobre Lógica en Ciencias de la Computación, 1992. LICS '92. Actas . Séptimo Simposio Anual de IEEE sobre Lógica en Ciencias de la Computación, 1992. LICS '92. Actas. págs. 200–210. doi : 10.1109 / LICS.1992.185533 .
- ^ Lincoln, Patrick; Winkler, Timothy (1994). "La lógica lineal multiplicativa de sólo constante es NP-completa" . Informática Teórica . 135 : 155-169. doi : 10.1016 / 0304-3975 (94) 00108-1 .
- ^ Gunter, CA; Gehlot, V. (1989). Décimo Congreso Internacional de Aplicación y Teoría de las Redes de Petri. Actas. págs. 174-191. Falta o vacío
|title=
( ayuda ) - ^ Bimbó, Katalin ( 13 de septiembre de 2015 ). "La decidibilidad del fragmento intensional de la lógica lineal clásica" . Informática Teórica . 597 : 1-17. doi : 10.1016 / j.tcs.2015.06.019 . ISSN 0304-3975 .
- ^ Straßburger, Lutz (10 de mayo de 2019). "Sobre el problema de decisión para MELL" . Informática Teórica . 768 : 91–98. doi : 10.1016 / j.tcs.2019.02.022 . ISSN 0304-3975 .
- ^ Kopylov, AP (1 de junio de 1995). "Decidibilidad de la lógica afín lineal". Décimo Simposio Anual de IEEE sobre Lógica en Ciencias de la Computación, 1995. LICS '95. Actas . Décimo Simposio Anual de IEEE sobre Lógica en Ciencias de la Computación, 1995. LICS '95. Actas. págs. 496–504. CiteSeerX 10.1.1.23.9226 . doi : 10.1109 / LICS.1995.523283 .
Otras lecturas
- Girard, Jean-Yves. Lógica lineal , Theoretical Computer Science, Vol 50, no 1, pp. 1–102, 1987.
- Girard, Jean-Yves, Lafont, Yves y Taylor, Paul. Pruebas y tipos . Cambridge Press, 1989.
- Hoare, CAR, 1985. Comunicando procesos secuenciales . Prentice-Hall International. ISBN 0-13-153271-5
- Lafont, Yves, 1993. Introducción a la lógica lineal . Notas de la conferencia de la Escuela de verano TEMPUS sobre métodos algebraicos y categóricos en informática , Brno, República Checa.
- Troelstra, AS Conferencias sobre lógica lineal . CSLI (Centro para el estudio del lenguaje y la información) Lecture Notes No. 29. Stanford, 1992.
- AS Troelstra , H. Schwichtenberg (1996). Teoría básica de la prueba . En la serie Cambridge Tracts in Theoretical Computer Science , Cambridge University Press, ISBN 0-521-77911-1 .
- Di Cosmo, Roberto y Danos, Vincent. La cartilla de lógica lineal .
- Introducción a la lógica lineal (posdata) por Patrick Lincoln
- Introducción a la lógica lineal por Torben Brauner
- Una muestra de lógica lineal por Philip Wadler
- Lógica lineal de Roberto Di Cosmo y Dale Miller . La Enciclopedia de Filosofía de Stanford (edición de otoño de 2006), Edward N. Zalta (ed.).
- Descripción general de la programación lógica lineal por Dale Miller . En Linear Logic in Computer Science , editado por Ehrhard, Girard, Ruet y Scott. Prensa de la Universidad de Cambridge. Notas de la conferencia de la Sociedad Matemática de Londres, volumen 316, 2004.
- Wiki de Lógica Lineal
enlaces externos
- Medios relacionados con la lógica lineal en Wikimedia Commons
- Un probador de lógica lineal (llprover) , disponible para su uso en línea, de: Naoyuki Tamura / Dept of CS / Kobe University / Japón