En el cálculo proposicional y la complejidad de la 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, una pps es una función de tiempo polinomial P cuyo rango es el conjunto de todas las tautologías proposicionales (denotadas TAUT). [1] Si A es una fórmula, entonces cualquier x tal que P ( x ) = A se denomina P -prueba de A . La condición que define a pps se puede dividir de la siguiente manera:
En general, un sistema de prueba para un lenguaje L es una función de tiempo polinomial 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 ) decimos que x es una P -prueba de A . Se requiere que P se ejecute en tiempo polinomial y, además, debe cumplirse que A tiene una P -prueba si y solo si es una tautología.
Si P 1 es un pps según la primera definición, entonces P 2 se define 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 se define por
( P 1 toma pares como entrada) es un pps según la primera definición, donde es una tautología fija.
Se puede considerar la segunda definición como un algoritmo no determinista para resolver la pertenencia a TAUT. Esto significa que probar un límite inferior del tamaño de prueba superpolinomial para pps descartaría la existencia de una cierta clase de algoritmos de tiempo polinomial basados en ese pps.
Por ejemplo, los límites inferiores del tamaño de la prueba exponencial en la resolución para el principio del casillero implican que cualquier algoritmo basado en la resolución no puede decidir TAUT o SAT de manera eficiente y fallará en las tautologías del principio del casillero . Esto es significativo porque la clase de algoritmos basados en la resolución incluye la mayoría de los algoritmos de búsqueda de pruebas proposicionales actuales y los solucionadores SAT industriales modernos.
Históricamente, el cálculo proposicional de Frege fue el primer sistema de demostración proposicional. La definición general de un sistema de demostración proposicional se debe a Stephen Cook y Robert A. Reckhow (1979). [1]
El sistema de prueba proposicional puede compararse usando la noción de p-simulación. Un sistema de prueba proposicional P p-simula Q (escrito como P ≤ p Q ) cuando hay una función de tiempo polinomial F tal que P ( F ( x )) = Q ( x ) para cada x . [1] Es decir, dada una Q -prueba x , podemos encontrar en tiempo polinomial una P -prueba de la misma tautología. Si P ≤ p Q y Q ≤ p P , los sistemas de prueba P y Q son p-equivalentes . También hay una noción más débil de simulación: un pps P simula o p-simula débilmente un pps Q si hay un polinomio p tal que para cada Q -prueba x de una tautología A , hay una P -prueba y de A tal que la longitud de y , | y | es como máximo p (| x |). (Algunos autores utilizan las palabras p-simulación y simulación indistintamente para cualquiera de estos dos conceptos, generalmente el último).
Un sistema de prueba proposicional se denomina p-óptimo si p -simula todos los demás sistemas de prueba proposicional, y es óptimo si simula todos los demás pp. Un sistema de prueba proposicional P está polinomialmente acotado (también llamado super) si cada tautología tiene una P -prueba corta (es decir, de tamaño polinomial) .
Si P está acotado polinomialmente y Q simula P , entonces Q también está acotado polinomialmente.
El conjunto de tautologías proposicionales, TAUT, es un conjunto coNP -completo. Un sistema de prueba proposicional es un verificador de certificados para la pertenencia a TAUT. La existencia de un sistema de prueba proposicional acotado polinomialmente significa que hay un verificador con certificados de tamaño polinomial, es decir, TAUT está en NP . De hecho, estas dos afirmaciones son equivalentes, es decir, hay un sistema de prueba proposicional acotado polinomialmente si y solo si las clases de complejidad NP y coNP son iguales. [1]
Algunas clases de equivalencia de sistemas de prueba bajo simulación o p -simulación están estrechamente relacionadas con las teorías de la aritmética acotada ; son esencialmente versiones "no uniformes" de la aritmética acotada, de la misma manera que las clases de circuitos son versiones no uniformes de las clases de complejidad basadas en recursos. Los sistemas "Frege extendido" (que permiten la introducción de nuevas variables por definición) corresponden de esta manera a sistemas acotados polinomialmente, por ejemplo. Cuando la aritmética acotada a su vez corresponde a una clase de complejidad basada en circuitos, a menudo hay similitudes entre la teoría de sistemas de prueba y la teoría de las familias de circuitos, como la coincidencia de resultados de cota inferior y separaciones. Por ejemplo, así como el conteo no puede realizarse mediante una familia de circuitos de tamaño subexponencial, muchas tautologías relacionadas con el principio del palomar no pueden tener pruebas subexponenciales en un sistema de prueba basado en fórmulas de profundidad acotada (y en particular, no mediante sistemas basados en resolución, ya que se basan únicamente en fórmulas de profundidad 1).
Algunos ejemplos de sistemas de prueba proposicional estudiados son:
