A complexidade da prova é uma área mais básica da teoria da complexidade computacional. Um objetivo final dessa área é provar , ou seja, qualquer provador não pode dar uma prova de insatisfação de determinada fórmula de entrada.
Um gráfico é um modelo formal de provas. Minha pergunta é sobre outras restrições a esse modelo.
Uma prova é representada como um DAG. Nós com fan-in 0 possuem rótulos de axioma. O nó exclusivo com fan-out 0 corresponde a "false". Para determinadas regras de dedução de entrada, cada nó que possui grau e grau externo tem o rótulo que representa a proposição.
Minha pergunta é:
Existem sistemas de prova e pesquisas relacionadas no caso de a classe de DAGs de prova ser restrita? Artigos, pesquisas e notas de aula são bem-vindos.
Os Sistemas de Prova estudados anteriormente, como Nullstellensatz, Resolução, LS, AC0 Frege, RES (k), Caluculus Polinomial e Planos de Corte, possuem alguma caracterização teórica gráfica?
Müller e Szeider estudam provas de resolução em que o DAG da prova delimita a largura da árvore ou a largura do caminho delimitado (para extensões adequadas dessas medidas de complexidade de gráficos em gráficos direcionados).
Eles mostram que a largura do caminho do DAG é essencialmente a mesma que a complexidade do espaço da prova e definem uma noção generalizada de espaço da prova que é equivalente à largura da árvore.
fonte
Para sistemas de prova suficientemente fortes, a representação gráfica de uma prova no sistema parece menos conseqüente, uma vez que (como Joshua Grochow já comentou), as provas de Frege do tipo DAG e do tipo árvore de Frege são polinomialmente equivalentes (consulte a monografia de Krajicek, de 1995, para uma prova desse fato). )
Para sistemas de prova mais fracos, como resolução, o tipo árvore é exponencialmente mais fraco que o tipo DAG (como Yuval Filmus descrito acima).
Beckmann e Buss [1] (seguindo Beckmann [2] ) consideraram restringir a altura (equivalentemente, profundidade) do gráfico de prova das provas de Frege de profundidade constante e investigaram a relação entre DAG, tamanho de árvore e altura de profundidade constante Provas de fraude. (Observe a distinção entre restringir a profundidade do gráfico de prova e restringir a profundidade de um circuito que aparece em uma linha de prova).
Também pode haver separações entre as provas Nullstellensatz (e cálculo polinomial), semelhantes a árvores e DAG, das quais atualmente não me lembro.
fonte