Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Théorème de Herbrand
Résumé
En logique, le théorème de Herbrand, publié en 1930 par Jacques Herbrand, établit un lien entre la logique du premier ordre et la logique propositionnelle (qui peut-être vu comme la logique d'ordre zéro). La validité (ou prouvabilité) d’une formule du premier ordre se ramène à la validité (ou prouvabilité) d'un ensemble fini de formules propositionnelles.
Alors qu'il est possible de déterminer algorithmiquement si une formule propositionnelle est démontrable ou pas, on sait — depuis les travaux de Gödel, Tarski, Church, Turing et autres — que la même question pour les formules du premier ordre est indécidable. Le théorème de Herbrand montre qu’elle est cependant semi-décidable : bien qu’il n’existe pas d’algorithme qui détermine si une formule donnée est prouvable ou pas, il existe une procédure qui résout partiellement la question en répondant « oui » si et seulement si la formule donnée est prouvable (pour certaines formules non prouvables, le calcul ne s'arrête pas).
Une formule du calcul des prédicats est prénexe si tous les quantificateurs qu'elle contient se trouvent au début de la formule. Toute formule admet une formule prénexe équivalente. Par exemple, la formule est équivalente successivement à , , et enfin (où , , , , désignent respectivement l'implication, la négation, la disjonction, le quantificateur existentiel et le quantificateur universel, et et sont des prédicats unaires).
Une formule prénexe est universelle si elle ne possède que des quantificateurs universels (symbole ). Il est possible d'associer à une formule quelconque une formule universelle en appliquant une transformation appelée skolémisation. Elle consiste à introduire de nouveaux symboles de fonction pour chaque quantificateur existentiel (symbole ). Par exemple, la forme skolémisée de est . Intuitivement, si pour chaque , il existe tel qu'une propriété soit vérifiée, alors on peut introduire une fonction telle que, pour tout , est vérifiée. On montre que la formule initiale admet un modèle si et seulement si sa forme skolémisée en admet un.
Source officielle
À propos de ce résultat
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.