En cálculo proposicional y complejidad de la prueba, un sistema de prueba proposicional ( pps ), también llamado sistema de prueba proposicional de Cook-Reckhow , es un sistema para demostrar tautologías proposicionales clásicas .
Formalmente, un 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 prueba P 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 polinomial cuyo rango es L. Por 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 prueba P de A. Se requiere que P se ejecute en tiempo polinomial y, además, debe cumplirse que A tiene una prueba P si y sólo 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 sólo 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.
Se puede ver la segunda definición como un algoritmo no determinista para resolver la membresía en TAUT. Esto significa que demostrar un tamaño de prueba superpolinómico en un límite inferior para pps descartaría la existencia de una determinada clase de algoritmos de tiempo polinomial basados en esos pps.
Como ejemplo, los límites inferiores del tamaño de 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 importante porque la clase de algoritmos basados en resolución incluye la mayoría de los algoritmos de búsqueda de prueba proposicional actuales y los solucionadores SAT industriales modernos.
Históricamente, el cálculo proposicional de Frege fue el primer sistema de prueba proposicional. La definición general de sistema de prueba proposicional se debe a Stephen Cook y Robert A. Reckhow (1979). [1]
El sistema de prueba proposicional se puede comparar utilizando la noción de simulación p. 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 prueba Q x , podemos encontrar en tiempo polinomial una prueba P 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 existe 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 usan las palabras simulación p y simulación indistintamente para cualquiera de estos dos conceptos, generalmente el último).
Un sistema de prueba proposicional se llama p-óptimo si p -simula todos los demás sistemas de prueba proposicional, y es óptimo si simula todos los demás pps. Un sistema de prueba proposicional P está acotado polinomialmente (también llamado super) si cada tautología tiene una prueba P 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 de membresía en 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, existe un sistema de prueba proposicional acotado polinomialmente si y sólo 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 clases de complejidad basadas en recursos. Los sistemas "Frege extendidos" (que permiten por definición la introducción de nuevas variables) corresponden de este modo a sistemas acotados polinómicamente, por ejemplo. Cuando la aritmética acotada, a su vez, corresponde a una clase de complejidad basada en circuitos, a menudo existen similitudes entre la teoría de los sistemas de prueba y la teoría de las familias de circuitos, como la comparación de resultados y separaciones de límites inferiores. Por ejemplo, así como el conteo no se puede realizar mediante una familia de circuitos de tamaño subexponencial, muchas tautologías relacionadas con el principio del casillero no pueden tener pruebas subexponenciales en un sistema de prueba basado en fórmulas de profundidad limitada (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 proposicionales estudiados son:
