Cálculo de estructuras

En lógica matemática , el cálculo de estructuras (CdS) es un cálculo de demostración con inferencia profunda para el estudio de la teoría de la demostración estructural de la lógica no conmutativa . Este cálculo se ha aplicado posteriormente al estudio de la lógica lineal , la lógica clásica , la lógica modal y los cálculos de procesos , y se afirma que estas investigaciones obtienen numerosos beneficios gracias a la forma en que el cálculo proporciona inferencia profunda.

Fue introducido por primera vez en 2001 en el artículo A System of Interaction and Structure de Alessio Guglielmo de la Universidad de Bath . ^{[ 1 ]}^{[ 2 ]}

Definiciones

Una fórmula es una cadena ( bien formada ) de símbolos lógicos. Por ejemplo, $((a\land b)\land \neg c)\lor d$ es una fórmula.

Una teoría de ecuaciones es un conjunto de ecuaciones que describen una relación de equivalencia en el conjunto de todas las fórmulas. Las ecuaciones más comunes son la asociatividad, la conmutatividad y las ecuaciones para constantes lógicas.

Una estructura es una clase de equivalencia de fórmulas. El término "estructura" subraya que CoS no distingue entre secuencias y fórmulas, sino que utiliza un único objeto para realizar ambas funciones en el cálculo de secuencias. En concreto, una estructura puede considerarse una clase de equivalencia de fórmulas.

Un contexto es una estructura a la que se le ha eliminado una subestructura. Por ejemplo, $A\land -$ es un contexto, donde el $-$ denota una subestructura eliminada. Los contextos se escriben como $S\{-\}$ , por ejemplo, si $S\{-\}:=A\land -$ , entonces $S\{B\}$ se define como $A\land B$ .

Una regla de inferencia tiene la forma ${\frac {S\{A\}}{S\{B\}}}$ , dónde $A,B$ son subestructuras y $S\{\}$ No es ninguna fórmula en particular, sino más bien una indicación de que "aquí puede ir cualquier contexto". Podemos presentarlo de forma simplificada como ${\frac {A}{B}}$ , partida $S\{\}$ implícito. Por defecto, los contextos que aparecen en las reglas de inferencia deben tener polaridad positiva.

Un contexto tiene una polaridad . La polaridad de un contexto es positiva o negativa . Por ejemplo, $A\lor -$ es un contexto positivo, pero $A\lor \neg -$ es un contexto negativo, pero $(A\lor \neg -)\to C$ es de nuevo un contexto positivo. La positividad o negatividad de un contexto se denomina su polaridad . Por ejemplo, decimos " $A\lor -$ tiene polaridad positiva", y " $A\lor \neg -$ tiene polaridad negativa".

Dos estructuras pueden ser duales entre sí. De manera similar, dos reglas de inferencia ${\frac {S\{A\}}{S\{B\}}},\;{\frac {S\{B'\}}{S\{A'\}}}$ También pueden ser duales entre sí, si es posible escribir $A'$ como un dual a $A$ , y $B'$ como un dual a $B$ La contraposición clásica es un ejemplo de esta dualidad.

Una convención es escribir $()$ para una conjunción, y $[]$ para una disyunción. Por ejemplo, en lógica lineal, se escribe $(A_{1},\dots ,A_{n})$ para $A_{1}\otimes \dots \otimes A_{n}$ , y $[A_{1},\dots ,A_{n}]$ para $A_{1}\mathbin {\mbox{⅋}} \dots \mathbin {\mbox{⅋}} A_{n}$ .

Ideas

Inferencia profunda

En el cálculo secuencial , cada regla de inferencia solo puede producir o eliminar conectores lógicos en el nivel más externo de una fórmula. En particular, esto significa que la mayoría de las subfórmulas permanecen inalteradas. En la inferencia profunda, cada regla de inferencia puede reescribir subfórmulas en cualquier nivel.

Por ejemplo, en el cálculo de secuentes para la lógica clásica, la regla ${\frac {\Gamma ,A,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}$ hojas $A,B$ y todas sus subfórmulas sin cambios. Solo el conector lógico más externo de $A\land B$ se produce.

Para la inferencia profunda, las reglas de inferencia pueden aplicarse a cualquier subfórmula, arbitrariamente profunda dentro del árbol de sintaxis. En otras palabras, de todos los nodos en el árbol de sintaxis de $A\land B$ Una regla de inferencia solo puede manipular el nodo más externo. La inferencia profunda permite que una regla manipule cualquier nodo dentro del árbol de sintaxis.

Simetría de arriba hacia abajo

En el cálculo de secuentes y la deducción natural , una demostración es un árbol de reglas de inferencia. Esto genera una asimetría fundamental: la parte superior de un árbol de demostración está formada por múltiples secuentes hoja, mientras que la parte inferior consta de un único secuente final. Sin embargo, muchas reglas de inferencia son simétricas: la mitad superior y la mitad inferior son mutuamente derivables.

Por ejemplo, si se puede aplicar una regla ${\frac {\Gamma \vdash A\quad \Gamma \vdash B}{\Gamma \vdash A\&B}}(\vdash \&)$ producir una prueba de $\Gamma \vdash A\&B$ , entonces también se puede producir una prueba de $\Gamma \vdash A$ y una prueba de $\Gamma \vdash B$ De esta manera, la regla de inferencia $\vdash \&$ tiene una simetría de arriba hacia abajo.

El formalismo del cálculo de secuencias hace implícita esta simetría de arriba hacia abajo, ya que la yuxtaposición de una secuencia $\Gamma \vdash A$ y otra secuencia $\Gamma \vdash B$ no es en sí mismo un secuente. Esto significa que esta simetría de arriba hacia abajo no está en el nivel de objeto del cálculo de demostración .

En el cálculo de secuencias, una demostración es una línea de reglas de inferencia. Esto sitúa la simetría descendente en el nivel del objeto.

SKSg

Definición

SKSg es un CoS para la lógica proposicional clásica.

Los símbolos de SKSg constan de:

Los átomos $a_{0},{\bar {a}}_{0},a_{1},{\bar {a}}_{1},\dots$ Decimos que $a_{i},{\bar {a}}_{i}$ son átomos que son duales entre sí.
Los conectores $\lor ,\land$ .
Las unidades $\top ,\bot$ .

La negación no existe en SKSg, ya que la hemos degradado de conector lógico a un mero emparejamiento entre átomos lógicos.

Una estructura de SKSg tiene la siguiente sintaxis en forma Backus-Naur : $F::=a|{\bar {a}}|\top |\bot |F\lor F|F\land F$ Sin negación, todos los contextos son positivos.

La dualidad para las estructuras se define por: ${\begin{aligned}{\overline {a}}={\bar {a}},&\quad {\overline {\bar {a}}}=a\\{\overline {A\land B}}={\overline {A}}\lor {\overline {B}},&\quad {\overline {A\lor B}}={\overline {A}}\land {\overline {B}}\end{aligned}}$ Las reglas de inferencia estructural se presentan en 3 pares duales:

Las dos reglas de inferencia lógica son autoduales:

Además de estas reglas, existen las siguientes ecuaciones: ${\begin{array}{rcl}A\lor B&=&B\lor A\\A\land B&=&B\land A\\(A\lor B)\lor C&=&A\lor (B\lor C)\\(A\land B)\land C&=&A\land (B\land C)\end{array}}\qquad {\begin{array}{rcl}A\lor \bot &=&A\\A\land \top &=&A\\\top \lor \top &=&\top \\\bot \land \bot &=&\bot \end{array}}\quad$ Todas las ecuaciones del sistema SKSg pueden reemplazarse por reglas de inferencia. El sistema resultante, sin ecuaciones, es SKS.

Propiedades

Esta es una derivación válida: ${\begin{array}{c}(a\lor b)\land a\\\Vert \\((a\lor b)\land a)\land ((a\lor b)\land a)\end{array}}\equiv \left({\frac {\left({\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )\right)\lor \left({\frac {b}{b\land b}}\;(\mathrm {c} \uparrow )\right)}{(a\lor b)\land (a\lor b)}}\;(\mathrm {m} )\right)\land \left({\frac {a}{a\land a}}\;(\mathrm {c} \uparrow )\right)\quad .$ Este es un principio general en la inferencia profunda: regla estructuralLas s en fórmulas genéricas pueden ser reemplazadas por la misma regla estructural en átomos. En este caso, cocontracción.

Una derivación sin cortes es una derivación donde $\mathrm {i} \uparrow$ no se utiliza. Se pueden eliminar los cortes mediante una técnica llamada división . ^{[ 3 ]}^{[ 4 ]}

MLL⁻

Definimos MLL⁻ como el sistema de prueba de lógica lineal multiplicativa sin unidades .

Una fórmula consta de $F::=a|{\bar {a}}|F\mathbin {\mbox{⅋}} F|F\times F$ . Aquí, $a$ y ${\bar {a}}$ son átomos duales. Las ecuaciones de dualidad son $(A\otimes B)^{\bot }=A^{\bot }\mathbin {\mbox{⅋}} B^{\bot },\quad (A\mathbin {\mbox{⅋}} B)^{\bot }=A^{\bot }\otimes B^{\bot }$ En particular, la negación ya no existe, puesto que la hemos degradado de un conector lógico a una mera dualidad entre pares de átomos lógicos. Por definición, ${\bar {\bar {a}}}=a$ .

El sistema tiene el siguiente CoS: ^{[ 4 ]} ${\begin{aligned}&\mathrm {i} \downarrow \;{\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}&&\mathrm {i} \uparrow \;{\frac {A\otimes A^{\perp }}{}}\\&\mathrm {i} \downarrow \;{\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}&&\mathrm {i} \uparrow \;{\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}\\&\sigma \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} B\}}{S\{B\mathbin {\mbox{⅋}} A\}}}&&\sigma \uparrow \;{\frac {S\{A\otimes B\}}{S\{B\otimes A\}}}\\&\alpha \downarrow \;{\frac {S\{A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C\}}}&&\alpha \uparrow \;{\frac {S\{A\otimes (B\otimes C)\}}{S\{(A\otimes B)\otimes C\}}}\\&\mathrm {s} \;{\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}\end{aligned}}$ Cada fila es un par de reglas duales. La regla de cambio es dual a sí misma.

Hay 4 reglas de iniciación, dos para i↑ y dos para i↓. La razón por la que hay dos en lugar de una es que el sistema no tiene unidades. $1,\bot$ . Con la unidad $1$ para $\otimes$ , uno puede simplemente subsumir ${\frac {}{A^{\perp }\mathbin {\mbox{⅋}} A}}$ como un caso especial de ${\frac {S\{B\}}{S\{(A^{\perp }\mathbin {\mbox{⅋}} A)\otimes B\}}}$ , dónde $S\{-\}$ es el contexto vacío, y $B=1$ . De manera similar, con la unidad $\bot$ para $\mathbin {\mbox{⅋}}$ , uno puede subsumir ${\frac {A\otimes A^{\bot }}{}}$ bajo ${\frac {S\{B\mathbin {\mbox{⅋}} (A\otimes A^{\perp })\}}{S\{B\}}}$ .

Las reglas de asociación $\alpha$ y conmutación $\sigma$ significa que ambos conectores son asociativos y conmutativos. Estas reglas pueden ser reemplazadas por las ecuaciones $(A\otimes B)\otimes C=A\otimes (B\otimes C)$ , etc.

i↑ corresponde al axioma de identidad en el cálculo de secuentes: $A\vdash A$ , o equivalentemente, $\vdash A^{\bot },A$ .

i↓ corresponde a la regla de corte: ${\frac {\Gamma \vdash \Delta ,A\quad A,\Gamma '\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}$ .

La regla del interruptor ${\frac {S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}}{S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}}}$ es más sutil. Corresponde a $S\{A\otimes (B\mathbin {\mbox{⅋}} C)\}\vdash S\{(A\otimes B)\mathbin {\mbox{⅋}} C\}$ En general, una regla de inferencia de un CoS puede leerse como una secuencia demostrable en un cálculo de secuencias, "rotándola 90 grados".

Interpretación

En MLL⁻, los símbolos $\otimes ,\mathbin {\mbox{⅋}}$ son conectores lógicos (conjunción, disyunción) y solo pueden aparecer a nivel de fórmulas. A nivel de secuencias, la coma se comporta esencialmente igual que $\mathbin {\mbox{⅋}}$ , puesto que tenemos la siguiente regla de inferencia ${\frac {\vdash \Gamma ,A,B,\Delta }{\vdash \Gamma ,A\mathbin {\mbox{⅋}} B,\Delta }}$ pero aparece a nivel de secuencias. De manera similar, escribir dos secuencias una al lado de la otra dentro de un árbol de prueba tiene esencialmente el mismo comportamiento que $\otimes$ , puesto que tenemos la siguiente regla de inferencia ${\frac {\vdash \Gamma ,A\quad \vdash B,\Delta }{\vdash \Gamma ,A\otimes B,\Delta }}$ pero parece estar al nivel de las pruebas.

En el CoS para MLL⁻, el símbolo $\otimes$ son manipulados según reglas de tal manera que puedan realizar el trabajo del conector lógico. $\otimes$ y la colocación lado a lado de secuencias. De manera similar para $\mathbin {\mbox{⅋}}$ .

En particular, dado un árbol de prueba en cálculo de secuencias MLL⁻, se puede convertir en una prueba en MLL⁻ CoS si se convierte cada secuencia $\vdash A_{1},\dots ,A_{n}$ en $A_{1}\mathbin {\mbox{⅋}} \dots \mathbin {\mbox{⅋}} A_{n}$ , luego convierte cada colocación lado a lado de secuencias $\vdash \Gamma _{1}\quad \dots \quad \vdash \Gamma _{n}$ con $\Gamma _{1}\otimes \dots \otimes \Gamma _{n}$ Luego, reemplace cada uso de regla de inferencia en el cálculo de secuencias con el uso de varias reglas de inferencia en el CoS. Esto demuestra que las estructuras no son una mera replicación de fórmulas o secuencias, ya que poseen características de ambas.

La eliminación de cortes corresponde a la eliminación i↓.

SLLS

El sistema SLLS es la versión CoS de la lógica lineal completa . Es mucho más grande que el CoS para MLL⁻. ^{[ 5 ]} ${\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {1}{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\bot }}\\&\mathrm {d} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\mathbin {\&} (C\mathbin {\mbox{⅋}} D)}{(A\mathbin {\&} C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {d} \uparrow \;{\frac {(A\oplus B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\oplus (B\otimes D)}}\\&\mathrm {p} \downarrow \;{\frac {!(R\mathbin {\mbox{⅋}} T)}{!R\mathbin {\mbox{⅋}} ?T}}&&\mathrm {p} \uparrow \;{\frac {!R\otimes ?T}{?(R\otimes T)}}\\&\mathrm {aw} \downarrow \;{\frac {0}{a}}&&\mathrm {ac} \downarrow \;{\frac {a\oplus a}{a}}&&\mathrm {ac} \uparrow \;{\frac {a}{a\mathbin {\&} a}}&&\mathrm {aw} \uparrow \;{\frac {a}{\top }}\\&\mathrm {nm} \downarrow \;{\frac {0}{0\mathbin {\&} 0}}&&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}&&\mathrm {m} \;{\frac {(A\mathbin {\&} B)\oplus (C\mathbin {\&} D)}{(A\oplus C)\mathbin {\&} (B\oplus D)}}&&\mathrm {nm} \uparrow \;{\frac {\top \oplus \top }{\top }}\\&\mathrm {nm} _{1}\downarrow \;{\frac {0}{0\mathbin {\mbox{⅋}} 0}}&&\mathrm {m} _{1}\downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\oplus (C\mathbin {\mbox{⅋}} D)}{(A\oplus C)\mathbin {\mbox{⅋}} (B\oplus D)}}&&\mathrm {m} _{1}\uparrow \;{\frac {(A\mathbin {\&} B)\otimes (C\mathbin {\&} D)}{(A\otimes C)\mathbin {\&} (B\otimes D)}}&&\mathrm {nm} _{1}\uparrow \;{\frac {\top \otimes \top }{\top }}\\&\mathrm {nm} _{2}\downarrow \;{\frac {0}{0\otimes 0}}&&\mathrm {m} _{2}\downarrow \;{\frac {(A\otimes B)\oplus (C\otimes D)}{(A\oplus C)\otimes (B\oplus D)}}&&\mathrm {m} _{2}\uparrow \;{\frac {(A\mathbin {\&} B)\mathbin {\mbox{⅋}} (C\mathbin {\&} D)}{(A\mathbin {\mbox{⅋}} C)\mathbin {\&} (B\mathbin {\mbox{⅋}} D)}}&&\mathrm {nm} _{2}\uparrow \;{\frac {\top \mathbin {\mbox{⅋}} \top }{\top }}\\&\mathrm {nl} _{1}\downarrow \;{\frac {0}{?0}}&&\mathrm {l} _{1}\downarrow \;{\frac {?R\oplus ?T}{?(R\oplus T)}}&&\mathrm {l} _{1}\uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\mathbin {\&} !T}}&&\mathrm {nl} _{1}\uparrow \;{\frac {!\top }{\top }}\\&\mathrm {nl} _{2}\downarrow \;{\frac {0}{!0}}&&\mathrm {l} _{2}\downarrow \;{\frac {!R\oplus !T}{!(R\oplus T)}}&&\mathrm {l} _{2}\uparrow \;{\frac {?(R\mathbin {\&} T)}{?R\mathbin {\&} ?T}}&&\mathrm {nl} _{2}\uparrow \;{\frac {?\top }{\top }}\\&\mathrm {nz} \downarrow \;{\frac {\bot }{?0}}&&\mathrm {z} \downarrow \;{\frac {?R\mathbin {\mbox{⅋}} T}{?(R\oplus T)}}&&\mathrm {z} \uparrow \;{\frac {!(R\mathbin {\&} T)}{!R\otimes T}}&&\mathrm {nz} \uparrow \;{\frac {!\top }{1}}\end{aligned}}$

${\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes 1&=A\\A\mathbin {\&} B&=B\mathbin {\&} A&(A\mathbin {\&} B)\mathbin {\&} C&=A\mathbin {\&} (B\mathbin {\&} C)&A\mathbin {\&} \top &=A\\A\oplus B&=B\oplus A&(A\oplus B)\oplus C&=A\oplus (B\oplus C)&A\oplus 0&=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} 1&=\bot \\??R&=?R&!!R&=!R\\\bot \oplus \bot &=\bot =?\bot &1\mathbin {\&} 1&=1=!1\end{aligned}}$

BV

El sistema BV (Sistema Básico V) puede ser producido por este CoS: ^{[ 6 ]} ${\begin{aligned}&\mathrm {ai} \downarrow \;{\frac {\circ }{a\mathbin {\mbox{⅋}} {\bar {a}}}}&&\mathrm {ai} \uparrow \;{\frac {a\otimes {\bar {a}}}{\circ }}\\&\mathrm {s} \;{\frac {(A\mathbin {\mbox{⅋}} B)\otimes C}{(A\otimes C)\mathbin {\mbox{⅋}} B}}\\&\mathrm {q} \downarrow \;{\frac {(A\mathbin {\mbox{⅋}} B)\triangleleft (C\mathbin {\mbox{⅋}} D)}{(A\triangleleft C)\mathbin {\mbox{⅋}} (B\triangleleft D)}}&&\mathrm {q} \uparrow \;{\frac {(A\triangleleft B)\otimes (C\triangleleft D)}{(A\otimes C)\triangleleft (B\otimes D)}}\end{aligned}}$

${\begin{aligned}A\otimes B&=B\otimes A&\qquad (A\otimes B)\otimes C&=A\otimes (B\otimes C)&\qquad A\otimes \circ &=A\\A\mathbin {\mbox{⅋}} B&=B\mathbin {\mbox{⅋}} A&(A\mathbin {\mbox{⅋}} B)\mathbin {\mbox{⅋}} C&=A\mathbin {\mbox{⅋}} (B\mathbin {\mbox{⅋}} C)&A\mathbin {\mbox{⅋}} \circ &=A\\&&(A\triangleleft B)\triangleleft C&=A\triangleleft (B\triangleleft C)&A\triangleleft \circ &=A=\circ \triangleleft A\end{aligned}}$

Referencias

↑ Guglielmi, Alessio (2007-01-01). "Un sistema de interacción y estructura" . ACM Trans. Comput. Logic . 8 (1): 1–es. doi : 10.1145/1182613.1182614 . ISSN 1529-3785 .
↑ Novaković, Novak; Straßburger, Lutz (21 de abril de 2015). "Sobre el poder de la sustitución en el cálculo de estructuras" . ACM Trans. Comput. Logic . 16 (3): 19:1–19:20. doi : 10.1145/2701424 . ISSN 1529-3785 .
↑ "Inferencia profunda" . alessio.guglielmi.name . Consultado el 30 de abril de 2026 .
1 2 Strassburger, Lutz (2006-11-20), Proof Nets and the Identity of Proofs , arXiv, doi : 10.48550/arXiv.cs/0610123 , arXiv:cs/0610123
↑ Aler Tubella, Andrea; Straßburger, Lutz (2019). Introducción a la inferencia profunda: notas de clase para ESSLLI'19, 5-16 de agosto de 2019, Universidad de Letonia (PDF) (Informe).
↑ Guglielmi, Alessio (2007-01-01). "Un sistema de interacción y estructura" . ACM Trans. Comput. Logic . 8 (1): 1–es. doi : 10.1145/1182613.1182614 . ISSN 1529-3785 .

Lecturas adicionales

Kai Brünnler (2004). Inferencia profunda y simetría en demostraciones clásicas . Logos Verlag.

Enlaces externos

Página principal del cálculo de estructuras
CoS en Maude : página que documenta implementaciones de sistemas lógicos en el cálculo de estructuras, utilizando el sistema Maude .

[1] Guglielmi, Alessio (2007-01-01). "Un sistema de interacción y estructura" . ACM Trans. Comput. Logic . 8 (1): 1–es. doi : 10.1145/1182613.1182614 . ISSN 1529-3785 .

[:0-2] Novaković, Novak; Straßburger, Lutz (21 de abril de 2015). "Sobre el poder de la sustitución en el cálculo de estructuras" . ACM Trans. Comput. Logic . 16 (3): 19:1–19:20. doi : 10.1145/2701424 . ISSN 1529-3785 .

[3] "Inferencia profunda" . alessio.guglielmi.name . Consultado el 30 de abril de 2026 .

[:1-4] 1 2 Strassburger, Lutz (2006-11-20), Proof Nets and the Identity of Proofs , arXiv, doi : 10.48550/arXiv.cs/0610123 , arXiv:cs/0610123

[5] Aler Tubella, Andrea; Straßburger, Lutz (2019). Introducción a la inferencia profunda: notas de clase para ESSLLI'19, 5-16 de agosto de 2019, Universidad de Letonia (PDF) (Informe).

[6] Guglielmi, Alessio (2007-01-01). "Un sistema de interacción y estructura" . ACM Trans. Comput. Logic . 8 (1): 1–es. doi : 10.1145/1182613.1182614 . ISSN 1529-3785 .

[ 1 ]

[ 3 ]

[ 5 ]

[ 6 ]