Una representación gráfica y canónica de pruebas en fragmentos de la lógica lineal donde fórmulas y sus conexiones aparecen como nodos y enlaces; las redes de prueba hacen explícito el paralelismo, eliminan la burocracia sintáctica de las pruebas en sequent y admiten criterios gráficos de corrección y eliminación de cortes como transformaciones locales de grafos.

Principio

Codificar una prueba como una estructura tipo grafo (enlaces para conectivos lógicos y enlaces axioma para pares atómicos) de modo que condiciones de corrección identifiquen los grafos que corresponden a pruebas sequent válidas; la eliminación de cortes se realiza mediante reescrituras locales del grafo que preservan la corrección.

Demostración

En lógica lineal multiplicativa, una derivación de A⊗B se dibuja como una red con un enlace tensor que une las subredes de A y B y enlaces axioma que emparejan átomos duales; una condición de corrección (aciclidad y conexidad bajo determinadas alternativas) certifica que el diagrama es una prueba válida y que las reescrituras del grafo llevan a la eliminación de cortes.

Aplicación incorrecta

Tratar como red de prueba a cualquier grafo arbitrario con grados similares sin verificar el criterio de corrección prescrito, o aplicar transformaciones de redes pertenecientes a un fragmento a otro fragmento incompatible, puede producir 'pruebas' insostenibles o romper invariantes de eliminación de cortes.

Consecuencia

Formadas correctamente, las redes de prueba proporcionan un testigo canónico y a menudo compacto de la demostrabilidad que hace explícito el paralelismo, simplifica la equivalencia de pruebas y convierte la eliminación de cortes en reescrituras locales y confluyentes del grafo, facilitando análisis de complejidad y normalización.

Inversión

La postura opuesta es la prueba secuencial en sequent: una derivación linealizada, regla por regla, que registra explícitamente el orden de aplicación de reglas. Las pruebas sequent hacen visible el contenido operativo pero ocultan la estructura paralela y admiten muchas variantes sintácticas de una misma red.

Límite

Las redes de prueba están bien desarrolladas para varios fragmentos de la lógica lineal (multiplicativo, multiplicativo-exponencial con precauciones) pero requieren esquemas de enlace y criterios de corrección adaptados a cada fragmento; no son una representación gráfica inmediata para lógicas no lineales o clásicas sin modificaciones.

Tensión semántica

Tensión entre redes de prueba y presentaciones en sequent: las redes subrayan estructura canónica y paralela, mientras que los sequent enfatizan el orden sintáctico de la derivación; la conversion (secuencialización) entre ambas es no trivial y depende del fragmento.

Síntesis

Las redes de prueba comprimen derivaciones sequent en objetos gráficos que identifican la estructura paralela esencial y el contenido canónico de las pruebas en lógica lineal: mediante criterios precisos de corrección y la interpretación de la eliminación de cortes como reescrituras de grafos, ofrecen una representación compacta y transparente de las pruebas y su normalización.