Le théorème de Fagin est un résultat de théorie de la complexité des algorithmes, montrant l'égalité de la classe NP et de la classe des problèmes exprimables en logique du second ordre existentielle, c'est-à-dire en logique du premier ordre enrichie de quantifications existentielles sur les ensembles. C'est le résultat fondateur de la complexité descriptive.
Ce résultat est remarquable, puisqu'il caractérise la classe NP sans avoir recours à une notion de modèle de calcul comme la machine de Turing.
La preuve de ce résultat fut établie en 1973 par Ronald Fagin dans sa thèse de doctorat. Elle a été depuis reformulée et améliorée, notamment grâce au théorème de Lynch et à des résultats de Grandjean.
On trouve une preuve de ce théorème dans le livre de complexité descriptive de Neil Immerman.
vignette|Graphe coloriable avec 3 couleurs.
Le problème de 3-coloration est dans NP et est décrit par le langage {G | il existe une 3-coloration des sommets de G telle deux sommets adjacentes ne soient pas de la même couleur}. Le théorème de Fagin dit qu'il est décrit par une formule de la logique du second ordre existentielle. En fait, il est décrit par la formule suivante : .
Par exemple, le graphe ci-contre est un modèle de cette formule car il est coloriable avec trois couleurs.
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.
En informatique théorique, la complexité descriptive est une branche de la théorie de la complexité et de la théorie des modèles, qui caractérise les classes de complexité en termes de logique qui permet de décrire les problèmes. La complexité descriptive donne un nouveau point de vue car on définit des classes de complexité sans faire appel à une notion de machines comme les machines de Turing. Par exemple la classe NP correspond à l'ensemble des problèmes exprimables en logique du second ordre existentielle : c'est le théorème de Fagin.
In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory. First-order logic quantifies only variables that range over individuals (elements of the domain of discourse); second-order logic, in addition, also quantifies over relations. For example, the second-order sentence says that for every formula P, and every individual x, either Px is true or not(Px) is true (this is the law of excluded middle).