Complexité des preuves
En informatique théorique, la complexité des preuves ou complexité des démonstrations est le domaine qui étudie les ressources nécessaires pour prouver ou réfuter un énoncé mathématique.
Le démarche classique du domaine est de fixer une sorte de preuve, puis de montrer des bornes sur la longueur des preuves pour certains énoncés. La sorte de preuve peut être d'origine logique, comme la déduction naturelle, le calcul des séquents, des systèmes basés sur la règle de résolution, ou plus combinatoire, comme l'algorithme DPLL et la méthode des plans sécants[1]. Pour chacun il faut définir une notion de longueur pertinente.
Le domaine est lié à la théorie de la complexité et aux assistants de preuve. Il a aussi de fortes relations avec les circuits booléens[1].
Notes et références
- Paul Beame et Toniann Pitassi, « Propositional proof complexity: past, present, and future », Bulletin of the European Association for Theoretical Computer Science, no 65,‎ , p. 66-89.