Représentation graphique des restrictions théoriques aux preuves dans la théorie de la complexité des preuves

La complexité de la preuve est l'un des domaines les plus élémentaires de la théorie de la complexité informatique. Un objectif ultime de ce domaine est de prouver , c'est-à-dire que tout prouveur ne peut pas fournir une preuve d'insatisfiabilité d'une formule d'entrée donnée. $NP\neq coNP$

Un graphique est l'un des modèles formels de preuves. Ma question porte sur une restriction supplémentaire à ce modèle.

Une preuve est représentée comme un DAG. Les nœuds avec fan-in 0 ont des étiquettes d'axiome. Le nœud unique avec fan-out 0 correspond à "false". Pour des règles de déduction d'entrée données, chaque nœud qui a à la fois un degré et un degré extérieur a l'étiquette représentant la proposition.

Ma question est:

Existe-t-il des systèmes de preuve et des recherches connexes dans le cas où la classe de preuves-DAG est restreinte? Les articles, sondages et notes de cours sont les bienvenus.

Les systèmes de preuve qui ont été étudiés précédemment tels que Nullstellensatz, Résolution, LS, Frege AC0, RES (k), Caluculus polynomial et Plans de coupe, ont-ils une certaine caractérisation théorique des graphes ??

La restriction la plus naturelle sur la preuve DAG est qu'il s'agit d'un arbre - c'est-à-dire que tout "lemme" (conclusion intermédiaire) n'est pas utilisé plus d'une fois. Cette propriété est appelée "arborescente". La résolution générale est exponentiellement plus puissante que la résolution arborescente, comme l'ont montré par exemple Ben-Sasson, Impagliazzo et Wigderson . Le concept a également été envisagé pour d'autres systèmes de preuve - il suffit de rechercher «X arborescent», où X est un système de preuve qui vous intéresse. Dans le cas particulier de la résolution, d'autres restrictions peuvent être envisagées. Voir par exemple un article d' Alekhnovich, Johannsen, Pitassi et Urquhart concernant la résolution régulière.

La résolution arborescente est particulièrement importante car les implémentations traditionnelles de DPLL correspondent à des réfutations de résolution arborescente. La technique d'apprentissage des clauses, qui est importante dans la pratique, correspond à autoriser les DAG généraux. Par conséquent, la structure du DAG de preuve dépend également fortement de l'algorithme qui le génère.

Müller et Szeider étudient les preuves de résolution où la preuve DAG a une largeur d'arbre bornée ou une largeur de chemin bornée (pour des extensions appropriées de ces mesures de complexité de graphe à des graphes dirigés.)

Ils montrent que la largeur de chemin du DAG est essentiellement la même que la complexité spatiale de la preuve et définissent une notion généralisée d'espace de preuve qui est équivalente à la largeur de l'arbre.

Pour les systèmes de preuve suffisamment forts, la représentation graphique d'une preuve dans le système semble moins conséquente, car (comme Joshua Grochow l'a déjà commenté), les preuves Frege de type DAG et arborescentes sont polynomialement équivalentes (voir la monographie de Krajicek de 1995 pour une preuve de ce fait). ).

Pour les systèmes de preuve plus faibles tels que la résolution, l'arborescence est exponentiellement plus faible que les épreuves de type DAG (comme Yuval Filmus décrit ci-dessus).

Beckmann et Buss [1] (suivant Beckmann [2] ) ont envisagé de restreindre la hauteur (de manière équivalente, la profondeur) du graphique d'épreuves des épreuves de Frege à profondeur constante et ont étudié la relation entre le type DAG, la taille de l'arbre et la hauteur à profondeur constante Preuve Frege. (Notez la distinction entre restreindre la profondeur du graphique d'épreuve et restreindre la profondeur d'un circuit apparaissant dans une ligne d'épreuve).

Il pourrait également y avoir des séparations entre les preuves Nullstellensatz (et calcul polynomial) arborescentes et DAG-like, dont je ne me souviens pas actuellement.