La complejidad de la prueba es un área más básica de la teoría de la complejidad computacional. Un propósito final de esta área es probar , es decir, cualquier comprobador no puede dar una prueba de insatisfacción de la fórmula de entrada dada.
Un gráfico es uno de modelo formal de pruebas. Mi pregunta es sobre más restricciones a este modelo.
Una prueba se representa como un DAG. Los nodos con fan-in 0 tienen etiquetas axiom. El nodo único con despliegue 0 corresponde a "falso". Para las reglas de deducción de entrada dadas, cada nodo que tiene tanto en grado como fuera de grado tiene la etiqueta que representa la proposición.
Mi pregunta es:
¿Existen sistemas de prueba e investigaciones relacionadas en el caso de que la clase de DAG de prueba esté restringida? Los trabajos, la encuesta y la nota de lectura son bienvenidos.
¿Los sistemas de prueba previamente estudiados como Nullstellensatz, resolución, LS, AC0 Frege, RES (k), cálculo polinómico y planos de corte, tienen alguna caracterización teórica gráfica?
Müller y Szeider estudian pruebas de resolución donde el DAG de prueba tiene un ancho de árbol acotado o un ancho de ruta acotado (para extensiones adecuadas de estas medidas de complejidad de gráfico a gráficos dirigidos).
Muestran que el ancho de ruta del DAG es esencialmente el mismo que la complejidad espacial de la prueba, y definen una noción generalizada del espacio de prueba que es equivalente al ancho del árbol.
fuente
Para sistemas de prueba lo suficientemente fuertes, la representación gráfica de una prueba en el sistema parece menos consecuente, ya que (como Joshua Grochow ya comentó), las pruebas de Frege tipo DAG y tipo árbol son polinomialmente equivalentes (ver la monografía de Krajicek de 1995 para una prueba de este hecho )
Para sistemas de prueba más débiles, como la resolución, el tipo de árbol es exponencialmente más débil que las pruebas de tipo DAG (como Yuval Filmus describió anteriormente).
Beckmann y Buss [1] (siguiendo a Beckmann [2] ) consideraron restringir la altura (equivalentemente, profundidad) del gráfico de prueba de pruebas de Frege de profundidad constante e investigaron la relación entre DAG, tamaño de árbol y altura de profundidad constante Pruebas de frege. (Observe la distinción entre restringir la profundidad del gráfico de prueba y restringir la profundidad de un circuito que aparece en una línea de prueba).
También puede haber separaciones entre pruebas Nullstellensatz (y cálculo polinomial) tipo árbol y DAG, que actualmente no recuerdo.
fuente