Complejidad de la prueba

En lógica e informática teórica , y específicamente en teoría de la prueba y teoría de la complejidad computacional , la complejidad de la prueba es el campo que tiene como objetivo comprender y analizar los recursos computacionales que se requieren para probar o refutar declaraciones. La investigación sobre la complejidad de la prueba se ocupa predominantemente de demostrar los límites superior e inferior de la longitud de la prueba en varios sistemas de prueba proposicionales . Por ejemplo, entre los principales desafíos de la complejidad de la prueba está mostrar que el sistema de Frege , el cálculo proposicional habitual , no admite pruebas de tamaño polinomial de todas las tautologías. Aquí el tamaño de la prueba es simplemente el número de símbolos que contiene, y se dice que una prueba es de tamaño polinómico si es polinómica en el tamaño de la tautología que demuestra.

El estudio sistemático de la complejidad de la prueba comenzó con el trabajo de Stephen Cook y Robert Reckhow (1979), quienes proporcionaron la definición básica de un sistema de prueba proposicional desde la perspectiva de la complejidad computacional. Específicamente, Cook y Reckhow observaron que demostrar límites inferiores del tamaño de la prueba en sistemas de prueba proposicionales cada vez más fuertes puede verse como un paso hacia la separación de NP de coNP (y por lo tanto P de NP), ya que existe un sistema de prueba proposicional que admite pruebas de tamaño polinómico. para todas las tautologías es equivalente a NP=coNP.

La investigación contemporánea sobre la complejidad de la prueba extrae ideas y métodos de muchas áreas de la complejidad computacional, los algoritmos y las matemáticas. Dado que muchos algoritmos y técnicas algorítmicas importantes pueden utilizarse como algoritmos de búsqueda de pruebas para ciertos sistemas de prueba, demostrar límites inferiores en los tamaños de prueba en estos sistemas implica límites inferiores en tiempo de ejecución en los algoritmos correspondientes. Esto conecta la complejidad de las pruebas con áreas más aplicadas, como la resolución SAT .

La lógica matemática también puede servir como marco para estudiar tamaños de prueba proposicionales. Las teorías de primer orden y, en particular, los fragmentos débiles de la aritmética de Peano , que reciben el nombre de aritmética acotada , sirven como versiones uniformes de los sistemas de prueba proposicional y proporcionan más antecedentes para interpretar pruebas proposicionales breves en términos de varios niveles de razonamiento factible.

Sistemas de prueba

Un sistema de prueba proposicional se proporciona 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 A es una tautología.

Ejemplos de sistemas de prueba proposicional incluyen cálculo secuencial , resolución , planos de corte y sistemas de Frege . Las teorías matemáticas sólidas como ZFC también inducen sistemas de prueba proposicionales: una prueba de una tautología en una interpretación proposicional de ZFC es una prueba ZFC de una declaración formalizada " es una tautología". ${\displaystyle \tau }$ ${\displaystyle \tau }$

Pruebas de tamaño polinomial y el problema NP versus coNP

La complejidad de la prueba mide la eficiencia del sistema de prueba generalmente en términos del tamaño mínimo de pruebas posibles en el sistema para una tautología determinada. El tamaño de una prueba (respectivamente fórmula) es el número de símbolos necesarios para representar la prueba (respectivamente fórmula). Un sistema de prueba proposicional P está acotado polinomialmente si existe una constante tal que cada tautología de tamaño tenga una prueba P de tamaño . Una cuestión central de la complejidad de la prueba es comprender si las tautologías admiten pruebas de tamaño polinómico. Formalmente, ${\displaystyle c}$ ${\displaystyle n}$ ${\displaystyle (n+c)^{c}}$

Problema (NP versus coNP)

¿Existe un sistema de prueba proposicional acotado polinomialmente?

Cook y Reckhow (1979) observaron que existe un sistema de prueba polinomialmente acotado si y sólo si NP=coNP. Por lo tanto, demostrar que sistemas de prueba específicos no admiten pruebas de tamaño polinómico puede verse como un progreso parcial hacia la separación de NP y coNP (y por tanto de P y NP). ^[1]

Optimidad y simulaciones entre sistemas de prueba.

La complejidad de la prueba compara la solidez de los sistemas de prueba utilizando la noción de simulación. Un sistema de prueba P p-simula un sistema de prueba Q si hay una función de tiempo polinomial que, dada una prueba Q de una tautología, genera una prueba P de la misma tautología. Si P p-simula Q y Q p-simula 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 sistema de prueba P simula un sistema de prueba 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 |).

Por ejemplo, el cálculo secuencial es p-equivalente a (todos) los sistemas de Frege. ^[2]

Un sistema de prueba es p-óptimo si p -simula todos los demás sistemas de prueba, y es óptimo si simula todos los demás sistemas de prueba. Es un problema abierto si existen tales sistemas de prueba:

Problema (optimidad)

¿Existe un sistema de prueba proposicional p-óptimo u óptimo?

Cada sistema de prueba proposicional P puede simularse mediante Frege extendido extendido con axiomas que postulan la solidez de P. ^[3] Se sabe que la existencia de un sistema de prueba óptimo (respectivamente p-óptimo) se deriva del supuesto de que NE = coNE (respectivamente E = NE ). ^[4]

Se sabe que muchos sistemas de prueba débiles no simulan ciertos sistemas más fuertes (ver más abajo). Sin embargo, la cuestión permanece abierta si se relaja la noción de simulación. Por ejemplo, está abierto si la resolución simula polinomialmente de manera efectiva la Frege extendida. ^[5]

Automatización de la búsqueda de pruebas

Una cuestión importante en la complejidad de las pruebas es comprender la complejidad de buscar pruebas en sistemas de prueba.

Problema (automatización)

¿Existen algoritmos eficientes que buscan pruebas en sistemas de prueba estándar como Resolución o el sistema Frege?

La cuestión puede formalizarse mediante la noción de automatizabilidad (también conocida como automatizabilidad). ^[6]

Un sistema de prueba P es automatizable si hay un algoritmo que, dada una tautología, genera una prueba P de en el tiempo polinomio en el tamaño y la longitud de la prueba P más corta de . Tenga en cuenta que si un sistema de prueba no está acotado polinomialmente, aún puede ser automatizable. Un sistema de prueba P es débilmente automatizable si hay un sistema de prueba R y un algoritmo que, dada una tautología, genera una prueba de R en el tiempo polinomio en el tamaño y la longitud de la prueba de P más corta . ${\displaystyle \tau }$ ${\displaystyle \tau }$ ${\displaystyle \tau }$ ${\displaystyle \tau }$ ${\displaystyle \tau }$ ${\displaystyle \tau }$ ${\displaystyle \tau }$ ${\displaystyle \tau }$

Se cree que muchos sistemas de prueba de interés no son automatizables. Sin embargo, actualmente sólo se conocen resultados negativos condicionales.

• Krajíček y Pudlák (1998) demostraron que Extended Frege no es débilmente automatizable a menos que RSA no sea seguro contra P/poly . ^[7]
• Bonet , Pitassi y Raz (2000) demostraron que el sistema -Frege no es débilmente automatizable a menos que el esquema Diffie-Hellman no sea seguro contra P/poly. ^[8] Esto fue ampliado por Bonet, Domingo, Gavaldá, Maciel y Pitassi (2004), quienes demostraron que los sistemas Frege de profundidad constante de al menos 2 no son débilmente automatizables a menos que el esquema Diffie-Hellman no sea seguro contra adversarios no uniformes que trabajen en tiempo subexponencial. ^[9] ${\displaystyle TC^{0}}$
• Alekhnovich y Razborov (2008) demostraron que la Resolución y la Resolución en forma de árbol no son automatizables a menos que FPT=W[P] . ^[10] Esto fue ampliado por Galesi y Lauria (2010), quienes demostraron que Nullstellensatz y el cálculo polinomial no son automatizables a menos que colapse la jerarquía de parámetros fijos. ^[11] Mertz, Pitassi y Wei (2019) demostraron que la resolución y la resolución en forma de árbol no son automatizables incluso en cierto tiempo cuasipolinomial, suponiendo la hipótesis del tiempo exponencial . ^[12]
• Atserias y Müller (2019) demostraron que la resolución no es automatizable a menos que P=NP. ^[13] Esto fue ampliado por de Rezende, Göös, Nordström, Pitassi, Robere y Sokolov (2020) a la dureza NP de la automatización del cálculo nullstellensatz y polinomial; ^[14] de Göös, Koroth, Mertz y Pitassi (2020) sobre la dureza NP de la automatización de planos de corte; ^[15] y por Garlík (2020) a NP-dureza de la automatización k - Resolución DNF . ^[dieciséis]

No se sabe si la débil automatizabilidad de la Resolución rompería cualquier suposición estándar de dureza de la teoría de la complejidad.

En el lado positivo,

• Beame y Pitassi (1996) demostraron que la resolución en forma de árbol es automatizable en tiempo cuasipolinomial y la resolución es automatizable en fórmulas de pequeño ancho en tiempo débilmente subexponencial. ^{[17] [18]}

aritmética acotada

Los sistemas de prueba proposicionales pueden interpretarse como equivalentes no uniformes de teorías de orden superior. La equivalencia se estudia con mayor frecuencia en el contexto de las teorías de la aritmética acotada . Por ejemplo, el sistema de Frege extendido corresponde a la teoría de Cook que formaliza el razonamiento en tiempo polinomial y el sistema de Frege corresponde a la teoría que formaliza el razonamiento. ${\displaystyle \mathrm {PV} _{1}}$ ${\displaystyle \mathrm {VNC} ^{1}}$ ${\displaystyle {\mathsf {NC}}^{1}}$

La correspondencia fue introducida por Stephen Cook (1975), quien demostró que los teoremas coNP, formalmente fórmulas, de la teoría se traducen en secuencias de tautologías con demostraciones de tamaño polinomial en Frege extendido. Además, Frege extendido es el sistema más débil: si otro sistema de prueba P tiene esta propiedad, entonces P simula Frege extendido. ^[19] ${\displaystyle \Pi _{1}^{b}}$ ${\displaystyle \mathrm {PV} _{1}}$

Una traducción alternativa entre enunciados de segundo orden y fórmulas proposicionales dada por Jeff Paris y Alex Wilkie (1985) ha sido más práctica para capturar subsistemas de Frege extendido como Frege o Frege de profundidad constante. ^{[20] [21]}

Si bien la correspondencia antes mencionada dice que las pruebas en una teoría se traducen en secuencias de pruebas breves en el sistema de prueba correspondiente, también se cumple una forma de implicación opuesta. Es posible derivar límites inferiores del tamaño de las pruebas en un sistema de prueba P construyendo modelos adecuados de una teoría T correspondiente al sistema P. Esto permite demostrar los límites inferiores de la complejidad mediante construcciones teóricas de modelos , un enfoque conocido como método de Ajtai . ^[22]

Solucionadores del SAT

Los sistemas de prueba proposicionales pueden interpretarse como algoritmos no deterministas para reconocer tautologías. Por lo tanto , demostrar un límite inferior superpolinomial en un sistema de prueba P descarta la existencia de un algoritmo de tiempo polinomial para SAT basado en P. Por ejemplo, las ejecuciones del algoritmo DPLL en instancias insatisfactorias corresponden a refutaciones de Resolución en forma de árbol. Por lo tanto, los límites inferiores exponenciales para la resolución en forma de árbol (ver más abajo) descartan la existencia de algoritmos DPLL eficientes para SAT. De manera similar, los límites inferiores de resolución exponencial implican que los solucionadores de SAT basados ​​en la resolución, como los algoritmos CDCL, no pueden resolver SAT de manera eficiente (en el peor de los casos).

límites inferiores

Por lo general, es muy difícil demostrar los límites inferiores de la longitud de las demostraciones proposicionales. Sin embargo, se han descubierto varios métodos para demostrar límites inferiores para sistemas de prueba débiles.

• Haken (1985) demostró un límite inferior exponencial para la resolución y el principio de casillero. ^[23]
• Ajtai (1988) demostró un límite inferior superpolinómico para el sistema de Frege de profundidad constante y el principio del casillero. ^[24] Esto fue reforzado hasta un límite inferior exponencial por Krajíček, Pudlák y Woods ^[25] y por Pitassi, Beame e Impagliazzo. ^[26] El límite inferior de Ajtai utiliza el método de restricciones aleatorias, que también se utilizó para derivar los límites inferiores de AC ⁰ en la complejidad del circuito .
• Krajíček (1994) ^[27] formuló un método de interpolación factible y luego lo utilizó para derivar nuevos límites inferiores para la resolución y otros sistemas de prueba. ^[28]
• Pudlák (1997) demostró límites inferiores exponenciales para planos de corte mediante una interpolación factible. ^[29]
• Ben-Sasson y Wigderson (1999) proporcionaron un método de prueba que reducía los límites inferiores del tamaño de las refutaciones de Resolución a límites inferiores de la amplitud de las refutaciones de Resolución, que capturaba muchas generalizaciones del límite inferior de Haken. ^[18]

Es un problema abierto desde hace mucho tiempo derivar un límite inferior no trivial para el sistema de Frege.

Interpolación factible

Consideremos una tautología de la forma . La tautología es cierta para cada elección de , y después de fijar la evaluación de y son independientes porque están definidas en conjuntos disjuntos de variables. Esto significa que es posible definir un circuito interpolante , de modo que ambos y se mantengan. El circuito interpolante decide si es falso o verdadero, considerando únicamente . La naturaleza del circuito interpolante puede ser arbitraria. Sin embargo, es posible utilizar una prueba de la tautología inicial como pista sobre cómo construir . Se dice que un sistema de prueba P tiene una interpolación factible si el interpolante es computable eficientemente a partir de cualquier prueba de la tautología en P. La eficiencia se mide con respecto a la duración de la prueba: es más fácil calcular interpoladores para pruebas más largas, por lo que esta propiedad parece ser antimonótona en la solidez del sistema de prueba. ${\displaystyle A(x,y)\rightarrow B(y,z)}$ ${\displaystyle y}$ ${\displaystyle y}$ ${\displaystyle A}$ ${\displaystyle B}$ ${\displaystyle C(y)}$ ${\displaystyle A(x,y)\rightarrow C(y)}$ ${\displaystyle C(y)\rightarrow B(y,z)}$ ${\displaystyle A(x,y)}$ ${\displaystyle B(y,z)}$ ${\displaystyle y}$ ${\displaystyle A(x,y)\rightarrow B(y,z)}$ ${\displaystyle C}$ ${\displaystyle C(y)}$ ${\displaystyle A(x,y)\rightarrow B(y,z)}$

Las siguientes tres afirmaciones no pueden ser simultáneamente verdaderas: (a) tiene una prueba corta en algún sistema de prueba; (b) dicho sistema de prueba tiene una interpolación factible; (c) el circuito interpolante resuelve un problema computacional difícil. Está claro que (a) y (b) implican que hay un pequeño circuito interpolante, lo que está en contradicción con (c). Dicha relación permite la conversión de los límites superiores de la longitud de la prueba en límites inferiores en los cálculos y, simultáneamente, convertir algoritmos de interpolación eficientes en límites inferiores de la longitud de la prueba. ${\displaystyle A(x,y)\rightarrow B(y,z)}$

Algunos sistemas de prueba, como Resolución y Planos de corte, admiten una interpolación factible o sus variantes. ^{[28] [29]}

La interpolación factible puede verse como una forma débil de automatizabilidad. De hecho, para muchos sistemas de prueba, como Extended Frege, la interpolación factible equivale a una automatizabilidad débil. Específicamente, muchos sistemas de prueba P son capaces de probar su propia solidez, lo cual es una tautología que afirma que "si es una prueba P de una fórmula, entonces se cumple". Aquí, están codificados por variables libres. Además, es posible generar P -pruebas de en tiempo polinómico dada la longitud de y . Por lo tanto, un interpolante eficiente resultante de pruebas P cortas de solidez de P decidiría si una fórmula dada admite una prueba P corta . Un interpolador de este tipo se puede utilizar para definir un sistema de prueba R que atestigua que P es débilmente automatizable. ^[30] Por otro lado, la débil automatizabilidad de un sistema de prueba P implica que P admite una interpolación factible. Sin embargo, si un sistema de prueba P no demuestra eficientemente su propia solidez, entonces podría no ser débilmente automatizable incluso si admite una interpolación factible. ${\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}$ ${\displaystyle \pi }$ ${\displaystyle \phi (x)}$ ${\displaystyle \phi (x)}$ ${\displaystyle \pi ,\phi ,x}$ ${\displaystyle \mathrm {Ref} _{P}(\pi ,\phi ,x)}$ ${\displaystyle \pi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \pi }$

Muchos resultados de no automatizabilidad proporcionan evidencia contra una interpolación factible en los sistemas respectivos.

• Krajíček y Pudlák (1998) demostraron que Extended Frege no admite una interpolación factible a menos que RSA no sea seguro contra P/poly. ^[31]
• Bonet, Pitassi y Raz (2000) demostraron que el sistema -Frege no admite una interpolación factible a menos que el esquema Diffie-Helman no sea seguro contra P/poly. ^[32] ${\displaystyle TC^{0}}$
• Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) demostraron que los sistemas de Frege de profundidad constante no admiten una interpolación factible a menos que el esquema Diffie-Helman no sea seguro contra adversarios no uniformes que trabajen en tiempo subexponencial. ^[33]

Lógicas no clásicas

La idea de comparar el tamaño de las pruebas se puede utilizar para cualquier procedimiento de razonamiento automatizado que genere una prueba. Se han realizado algunas investigaciones sobre el tamaño de las pruebas de lógicas proposicionales no clásicas , en particular, lógicas intuicionistas , modales y no monótonas .

Hrubeš (2007-2009) demostró límites inferiores exponenciales en el tamaño de las pruebas en el sistema de Frege extendido en algunas lógicas modales y en lógica intuicionista utilizando una versión de interpolación factible monótona. ^{[34] [35] [36]}

Ver también

• Complejidad computacional
• Complejidad del circuito
• Complejidad de la comunicación
• Lógica matemática
• Teoría de la prueba
• Clases de complejidad
• NP (complejidad)
• cNP

Referencias

1. Cocinero, Stephen ; Reckhow, Robert A. (1979). "La eficiencia relativa de los sistemas de prueba proposicional". Revista de Lógica Simbólica . 44 (1): 36–50. doi :10.2307/2273702. JSTOR  2273702. S2CID  2187041.
2. Reckhow, Robert A. (1976). Sobre la duración de las demostraciones en el cálculo proposicional (Tesis Doctoral). Universidad de Toronto.
3. Krajíček, enero (2019). Complejidad de la prueba . Prensa de la Universidad de Cambridge.
4. Krajíček, enero; Pudlák, Pavel (1989). "Sistemas de prueba proposicional, la consistencia de las teorías de primer orden y la complejidad de los cálculos". Revista de Lógica Simbólica . 54 (3): 1063–1079. doi :10.2307/2274765. JSTOR  2274765. S2CID  15093234.
5. Pitassi, Toniann ; Santhanam, Rahul (2010). "Simulaciones efectivamente polinomiales" (PDF) . ICS : 370–382.
6. Bonet, ML; Pitassi, Toniann ; Raz, corrió (2000). "Sobre interpolación y automatización del sistema de prueba de Frege". Revista SIAM de Computación . 29 (6): 1939-1967. doi :10.1137/S0097539798353230.
7. Krajíček, enero; Pudlák, Pavel (1998). "Algunas consecuencias de las conjeturas criptográficas para S 2 1 {\displaystyle S_{2}^{1}} y EF". Información y Computación . 140 (1): 82–94. doi : 10.1006/inco.1997.2674 .
8. Bonet, ML ; Pitassi, Toniann ; Raz, corrió (2000). "Sobre interpolación y automatización del sistema de prueba de Frege". Revista SIAM de Computación . 29 (6): 1939-1967. doi :10.1137/S0097539798353230.
9. Bonet, ML; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "No automatizabilidad de pruebas de Frege de profundidad limitada". Complejidad computacional . 13 (1–2): 47–68. doi :10.1007/s00037-004-0183-5. S2CID  1360759.
10. Alekhnovich, Michael; Razborov, Alejandro (2018). "La resolución no es automatizable a menos que W[P] sea manejable". Revista SIAM de Computación . 38 (4): 1347-1363. doi :10.1137/06066850X.
11. Galesi, Nicola; Lauria, Massimo (2010). "Sobre la automatizabilidad del cálculo polinomial". Teoría de los Sistemas Computacionales . 47 (2): 491–506. doi :10.1007/s00224-009-9195-5. S2CID  11602606.
12. Mertz, Ian; Pitassi, Toniann; Wei, Yuanhao (2019). "Es difícil encontrar pruebas breves". ICALP .
13. Atserias, Albert; Müller, Moritz (2019). "La automatización de la resolución es NP-difícil". Actas del 60º Simposio sobre fundamentos de la informática . págs. 498–509.
14. de Rezende, Susana; Göös, Mika; Nordström, Jakob; Pitassi, Tonniano; Robere, Robert; Sokolov, Dmitry (2020). "La automatización de sistemas de prueba algebraica es NP-difícil". ECCC .
15. Göös, Mika; Koroth, Sajín; Mertz, Ian; Pitassi, Tonniano (2020). "La automatización de planos de corte es NP-difícil". Actas del 52º Simposio Anual ACM SIGACT sobre Teoría de la Computación . págs. 68–77. arXiv : 2004.08037 . doi :10.1145/3357713.3384248. ISBN 9781450369794. S2CID  215814356.{{cite book}}: Mantenimiento CS1: fecha y año ( enlace )
16. Garlík, Michal (2020). "Fallo de la propiedad de disyunción factible para k -Resolución DNF y dureza NP de su automatización". ECCC . arXiv : 2003.10230 .
17. Hazme, Paul; Pitassi, Toniann (1996). "Límites inferiores de resolución simplificados y mejorados". 37º Simposio Anual sobre Fundamentos de la Informática : 274–282.
18. Ben-Sasson, Eli; Wigderson, Avi (1999). "Las pruebas breves son limitadas: la resolución es sencilla". Actas del 31º Simposio ACM sobre Teoría de la Computación . págs. 517–526.
19. Cocinero, Stephen (1975). "Pruebas factibles constructivas y cálculo de proposiciones". Actas del séptimo simposio anual de ACM sobre teoría de la computación . págs. 83–97.
20. París, Jeff ; Wilkie, Alex (1985). "Problemas de conteo en aritmética acotada". Métodos en lógica matemática . Apuntes de conferencias de matemáticas. vol. 1130. págs. 317–340. doi :10.1007/BFb0075316. ISBN 978-3-540-15236-1.
21. Cocinero, Stephen ; Nguyen, Phuong (2010). Fundamentos lógicos de la complejidad de la prueba . Perspectivas en lógica. Cambridge: Prensa de la Universidad de Cambridge. doi :10.1017/CBO9780511676277. ISBN 978-0-521-51729-4. SEÑOR  2589550.(borrador de 2008)
22. Ajtai, M. (1988). "La complejidad del principio del casillero". Actas del 29º Simposio Anual del IEEE sobre los fundamentos de la informática . págs. 346–355.
23. Haken, A. (1985). "La intratabilidad de la resolución". Informática Teórica . 39 : 297–308. doi :10.1016/0304-3975(85)90144-6.
24. Ajtai, M. (1988). "La complejidad del principio del casillero". Actas del 29º Simposio Anual del IEEE sobre los fundamentos de la informática . págs. 346–355.
25. Krajíček, enero; Pudlák, Pavel; Bosques, Alan (1995). "Un límite inferior exponencial del tamaño de las pruebas de Frege de profundidad acotada del principio de casillero". Estructuras aleatorias y algoritmos . 7 (1): 15–39. doi :10.1002/rsa.3240070103.
26. Pitassi, Toniann ; Haze, Paul; Impagliazzo, Russell (1993). "Límites inferiores exponenciales del principio del casillero". Complejidad computacional . 3 (2): 97–308. doi :10.1007/BF01200117. S2CID  1046674.
27. Krajíček, enero (1994). "Límites inferiores del tamaño de pruebas proposicionales de profundidad constante". Revista de Lógica Simbólica . 59 (1): 73–86. doi :10.2307/2275250. JSTOR  2275250. S2CID  44670202.
28. Krajíček, enero (1997). "Teoremas de interpolación, límites inferiores de sistemas de prueba y resultados de independencia para aritmética acotada". Revista de Lógica Simbólica . 62 (2): 69–83. doi :10.2307/2275541. JSTOR  2275541. S2CID  28517300.
29. Pudlák, Pavel (1997). "Límites inferiores para resolución y pruebas de planos de corte y cálculos monótonos". Revista de Lógica Simbólica . 62 (3): 981–998. doi :10.2307/2275583. JSTOR  2275583. S2CID  8450089.
30. Pudlák, Pavel (2003). "Sobre la reducibilidad y simetría de pares NP disjuntos". Informática Teórica . 295 : 323–339. doi :10.2307/2275583. JSTOR  2275583. S2CID  8450089.
31. Krajíček, enero; Pudlák, Pavel (1998). "Algunas consecuencias de las conjeturas criptográficas para S 2 1 {\displaystyle S_{2}^{1}} y EF". Información y Computación . 140 (1): 82–94. doi : 10.1006/inco.1997.2674 .
32. Bonet, ML; Pitassi, Toniann ; Raz, corrió (2000). "Sobre interpolación y automatización del sistema de prueba de Frege". Revista SIAM de Computación . 29 (6): 1939-1967. doi :10.1137/S0097539798353230.
33. Bonet, ML; Domingo, C.; Gavaldá, R.; Maciel, A.; Pitassi, Toniann (2004). "No automatizabilidad de pruebas de Frege de profundidad limitada". Complejidad computacional . 13 (1–2): 47–68. doi :10.1007/s00037-004-0183-5. S2CID  1360759.
34. Hrubeš, Pavel (2007). "Límites inferiores de la lógica modal". Revista de Lógica Simbólica . 72 (3): 941–958. doi : 10.2178/jsl/1191333849. S2CID  1743011.
35. Hrubeš, Pavel (2007). "Un límite inferior para la lógica intuicionista". Anales de lógica pura y aplicada . 146 (1): 72–90. doi :10.1016/j.apal.2007.01.001.
36. Hrubeš, Pavel (2009). "Sobre la duración de las pruebas en lógica no clásica". Anales de lógica pura y aplicada . 157 (2–3): 194–205. doi : 10.1016/j.apal.2008.09.013 .

Otras lecturas

• Haze, Paul; Pitassi, Toniann (1998), "Complejidad de la prueba proposicional: pasado, presente y futuro", Boletín de la Asociación Europea de Informática Teórica , 65 : 66–89, MR  1650939, ECCC  TR98-067
• Cocinero, Esteban ; Nguyen, Phuong (2010), Fundamentos lógicos de la complejidad de la prueba , Perspectivas en lógica, Cambridge: Cambridge University Press, doi :10.1017/CBO9780511676277, ISBN 978-0-521-51729-4, señor  2589550(borrador de 2008)
• Krajíček, Jan (1995), Aritmética limitada, lógica proposicional y teoría de la complejidad , Cambridge University Press
• Krajíček, Jan (2005), "Proof complex complex" (PDF) , en Laptev, A. (ed.), Actas del 4º Congreso Europeo de Matemáticas , Zúrich: Sociedad Matemática Europea, págs. 221–231, MR  2185746
• Krajíček, Jan, Complejidad de la prueba, Cambridge University Press, 2019.
• Pudlák, Pavel (1998), "La duración de las pruebas", en Buss, SR (ed.), Handbook of Proof Theory , Studies in Logic and the Foundations of Mathematics, vol. 137, Ámsterdam: Holanda Septentrional, págs. 547–637, doi :10.1016/S0049-237X(98)80023-2, MR  1640332

enlaces externos

• Complejidad de la prueba
• Lista de correo de complejidad de prueba.