Sistema de prueba de proposiciones
En cálculo proposicional y complejidad de prueba, un sistema de prueba proposicional ( pps ), también llamado sistema de prueba proposicional de Cook-Reckhow , es un sistema para probar tautologías proposicionales clásicas .
Formalmente a pps es una función de tiempo polinomial P cuyo rango es el conjunto de todas las tautologías proposicionales (denotado TAUT). [1] Si A es una fórmula, entonces cualquier x tal que P ( x ) = A se denomina P -proof de A . La condición que define pps se puede dividir de la siguiente manera:
En general, un sistema de prueba para un lenguaje L es una función de tiempo polinómico cuyo rango es L . Por lo tanto, un sistema de prueba proposicional es un sistema de prueba para TAUT.
A veces se considera la siguiente definición alternativa: un pps se da como un algoritmo de verificación de prueba P ( A , x ) con dos entradas. Si P acepta el par ( A , x ) se dice que x es un P -proof de A . Se requiere que P se ejecute en tiempo polinomial y, además, debe sostener que A tiene una prueba P si y solo si es una tautología.
Si P 1 es un pps según la primera definición, entonces P 2 definido por P 2 ( A , x ) si y solo si P 1 ( x ) = A es un pps según la segunda definición. Por el contrario, si P 2 es un pps según la segunda definición, entonces P 1 definido por
( P 1 toma pares como entrada) es un pps según la primera definición, donde es una tautología fija.
