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
  1. 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.
  • Portail de l'informatique théorique
  • Portail de la logique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.