Sistema de prueba proposicional

En cálculo proposicional y complejidad de la demostración , un sistema de demostración proposicional ( pps ), también llamado sistema de demostración proposicional de Cook-Reckhow , es un sistema para demostrar 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 prueba P de A. La condición que define las pps se puede descomponer de la siguiente manera:

• Completitud : toda tautología proposicional tiene una prueba P ,
• Solidez : si una fórmula proposicional tiene una prueba P, entonces es una tautología,
• Eficiencia : P se ejecuta en tiempo polinomial .

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.

En ocasiones, se considera la siguiente definición alternativa: un pps se define como un algoritmo de verificación de pruebas 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 cumplir que A tiene una prueba P si y solo si es una tautología.

Si P ₁ es un pps según la primera definición, entonces P ₂ definido por P ₂ ( A , x ) si y solo si P ₁ ( x ) = A es un pps según la segunda definición. Recíprocamente, si P ₂ es un pps según la segunda definición, entonces P ₁ definido por

${\displaystyle P_{1}(\langle x,A\rangle )={\begin{cases}A&{\text{si }}P_{2}(A,x)\\\top &{\text{en otro caso}}\end{cases}}}$

( P ₁ toma pares como entrada) es un pps según la primera definición, donde${\displaystyle \top }$es una tautología fija.

La segunda definición puede interpretarse como un algoritmo no determinista para resolver problemas de pertenencia a TAUT. Esto significa que demostrar una cota inferior superpolinómica para el tamaño de la prueba en pps descartaría la existencia de una determinada clase de algoritmos de tiempo polinomial basados ​​en dicho pps.

Por ejemplo, los límites inferiores exponenciales del tamaño de la prueba en la resolución del principio del palomar implican que cualquier algoritmo basado en la resolución no puede resolver TAUT o SAT de manera eficiente y fallará ante tautologías del principio del palomar . Esto es significativo porque la clase de algoritmos basados ​​en la resolución incluye la mayoría de los algoritmos actuales de búsqueda de pruebas proposicionales 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 un sistema de prueba proposicional se debe a Stephen Cook y Robert A. Reckhow (1979). ^{[ 1 ]}

Los sistemas de prueba proposicionales se pueden comparar utilizando la noción de p-simulación . Un sistema de prueba proposicional P p-simula Q (escrito como P  ≤ _p Q ) cuando existe una función de tiempo polinomial F tal que P ( F ( x )) = Q ( x ) para todo 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 existe una noción más débil de simulación: un pps P simula o p-simula débilmente un pps Q si existe un polinomio p tal que para cada Q -prueba x de una tautología A , existe una P -prueba y de A tal que la longitud de y , | y | es como máximo p (| x |). (Algunos autores utilizan los términos p-simulación y simulación indistintamente para referirse a cualquiera de estos dos conceptos, generalmente al segundo).

Un sistema de prueba proposicional se denomina p-óptimo si simula p a todos los demás sistemas de prueba proposicionales, y es óptimo si simula a todos los demás sistemas de prueba proposicionales. Un sistema de prueba proposicional P está acotado polinomialmente (también llamado super) si toda tautología tiene una prueba P corta (es decir, de tamaño polinomial) .

Si P está acotada polinómicamente y Q simula P , entonces Q también está acotada polinómicamente.

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 existe 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 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 teorías de 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 la introducción de nuevas variables por definición) corresponden de esta manera a sistemas acotados polinomialmente, por ejemplo. Donde 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 coincidencia de resultados de cotas inferiores y separaciones. Por ejemplo, así como el conteo no puede ser realizado por un${\displaystyle \mathbf {AC} ^{0}}$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 limitada (y en particular, no por 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:

• Resolución proposicional y diversas restricciones y extensiones de la misma, como el algoritmo DPLL.
• Deducción natural
• Cálculo de secuencias
• Sistema Frege
• Sistema Frege extendido
• Cálculo polinomial
• Sistema de Nullstellensatz
• Método del plano de corte
• Cuadro semántico

• Samuel Buss (1998), "Una introducción a la teoría de la demostración", en: Manual de teoría de la demostración (ed. SRBuss), Elsevier (1998).
• P. Pudlák (1998), " La longitud de las demostraciones ", en: Handbook of Proof Theory (ed. SRBuss), Elsevier, (1998).
• P. Beame y T. Pitassi (1998). Complejidad de las pruebas proposicionales: pasado, presente y futuro . Informe técnico TR98-067, Coloquio electrónico sobre complejidad computacional.
• Nathan Segerlind (2007) "La complejidad de las pruebas proposicionales" , Boletín de lógica simbólica 13(4): 417–481
• J. Krajíček (1995), Aritmética acotada, lógica proposicional y teoría de la complejidad , Cambridge University Press.
• J. Krajíček, Complejidad de las pruebas , en: Actas del 4º Congreso Europeo de Matemáticas (ed. A. Laptev), EMS, Zúrich, págs.  221–231, (2005).
• Alexander A. Razborov, Complejidad de la prueba proposicional , en: Actas del 8.º Congreso Europeo de Matemáticas , EMS, Portorož, págs.  439–464, (2023).
• J. Krajíček, Complejidad de la prueba proposicional I. y Complejidad de la prueba y aritmética .
• Stephen Cook y Phuong Nguyen, Fundamentos lógicos de la complejidad de las pruebas , Cambridge University Press, 2010 ( borrador de 2008 )
• Robert Reckhow, Sobre la longitud de las demostraciones en el cálculo proposicional , Tesis doctoral, 1975.

• Complejidad de la prueba