En la teoría de la prueba , las redes de prueba son un método geométrico de representar pruebas que elimina dos formas de burocracia que diferencia las pruebas: (A) características sintácticas irrelevantes de los cálculos de prueba regulares, como el cálculo de deducción natural y el cálculo secuencial , y (B) el orden de reglas aplicadas en una derivación. De esta manera, las propiedades formales de la identidad de prueba se corresponden más estrechamente con las propiedades intuitivamente deseables. Las redes de prueba fueron introducidas por Jean-Yves Girard .
Por ejemplo, estas dos pruebas de lógica lineal son idénticas:
|
|
Y sus redes correspondientes serán las mismas.
Criterios de corrección
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 en realidad 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 .
Ver también
Referencias
- ^ Girard, Jean-Yves. Lógica lineal , Informática teórica, Vol 50, no 1, págs. 1–102, 1987
Fuentes
- Pruebas y tipos . Girard JY, Lafont Y y Taylor P. Cambridge Press, 1989.
- Roberto Di Cosmo y Vincent Danos, The Linear Logic Primer
- Sean A. Fulop, un estudio de redes de prueba y matrices para lógicas subestructurales