Red de prueba

En teoría de la demostración , las redes de demostración son un método geométrico para representar demostraciones que elimina dos formas de burocracia que las diferencian: (A) características sintácticas irrelevantes de los cálculos de demostración regulares y (B) el orden de las reglas aplicadas en una derivación. De esta manera, las propiedades formales de la identidad de la demostración se corresponden más estrechamente con las propiedades intuitivamente deseables. Esto distingue a las redes de demostración de los cálculos de demostración regulares, como el cálculo de deducción natural y el cálculo de secuentes , donde estos fenómenos están presentes. Las redes de demostración fueron introducidas por Jean-Yves Girard .

A modo de ejemplo, estas dos demostraciones de lógica lineal son idénticas:

Y sus redes correspondientes serán las mismas.

Se conocen varios criterios de corrección para comprobar si una estructura de prueba secuencial (es decir, algo que parece ser una red de prueba) es realmente una estructura de prueba concreta (es decir, algo que codifica una derivación válida en lógica lineal). El primero de estos criterios es el criterio de viaje largo , ^{[ 1 ]} que fue descrito por Jean-Yves Girard .

• Lógica lineal
• Lúdicos
• Geometría de interacción
• Espacio coherente
• Inferencia profunda
• Redes de interacción

• Pruebas y tipos . Girard JY, Lafont Y y Taylor P. Cambridge Press, 1989.
• Roberto Di Cosmo y Vincent Danos, Introducción a la lógica lineal
• Sean A. Fulop, Un estudio de redes de prueba y matrices para lógicas subestructurales