Système de preuve interactive

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie Ne doit pas être confondu avec assistant de preuve.

En théorie de la complexité des algorithmes, un système de preuve interactive est un protocole formel de démonstration de théorèmes qui fait intervenir deux participants qui échangent des messages. Cela permet de définir des classes de complexité intéressantes, notamment la classe IP qui est le modèle utilisé dans le théorème PCP qui caractérise la classe NP.

Définitions[modifier | modifier le code]

Formellement, un système de preuve interactive est une machine abstraite qui modélise un échange de messages entre deux protagonistes : un prouveur et un vérificateur ; ceux-ci communiquent afin que le prouveur convainque le vérificateur de l'appartenance ou de la non-appartenance d'une chaîne de caractères à un langage formel donné. Le prouveur a des ressources de calcul illimitées tandis que le vérificateur a des ressources limitées. Les deux protagonistes interagissent aussi longtemps qu'il est nécessaire au vérificateur pour trouver une réponse au problème et être convaincu qu'elle est la bonne.

Deux propriétés doivent être satisfaites :

  • complétude : si le fournisseur de preuve et le vérificateur suivent le protocole alors le vérificateur doit toujours accepter la preuve ;
  • correction : si la proposition est fausse, la probabilité qu'un fournisseur de preuve malveillant puisse convaincre un vérificateur que la proposition est vraie est infime.

Classes de complexité associées[modifier | modifier le code]

Notes et références[modifier | modifier le code]