stringtranslate.com

Red de prueba

En teoría de la prueba , las redes de prueba son un método geométrico de representación de pruebas que elimina dos formas de burocracia que diferencian las pruebas: (A) las características sintácticas irrelevantes de los cálculos de prueba regulares, y (B) el orden de las 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. Esto distingue a las redes de prueba de los cálculos de prueba regulares, como el cálculo de deducción natural y el cálculo de secuencias , donde estos fenómenos están presentes. Las redes de prueba fueron introducidas por Jean-Yves Girard .

A modo de ilustración, 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 del viaje largo [1] , que fue descrito por Jean-Yves Girard .

Véase también

Referencias

  1. ^ Girard, Jean-Yves. Lógica lineal , Theoretical Computer Science , vol. 50, n.º 1, págs. 1-102, 1987

Fuentes