Une technique proof-théorique qui réduit la satisfiabilité du premier ordre à la satisfiabilité propositionnelle en construisant des ensembles finis (ou énumérables effectifs) d'instances sans variables — expansions de Herbrand — fondés sur l'univers de Herbrand.

Principe

Remplacer des formules quantifiées par des instances ground adéquatement instanciées issues de l'univers de Herbrand et tester la satisfiabilité propositionnelle des approximations finies obtenues ; une insatisfiabilité propositionnelle traduit l'insatisfiabilité du premier ordre sous les réductions standards.

Démonstration

Pour prouver l'insatisfiabilité de ∀x ∃y R(x,y) ∧ ∀x ¬R(x,c), générer des instances de Herbrand à partir des termes ground {c, f(c), …} et rechercher un ensemble fini contradictoire ; si une contradiction propositionnelle apparaît parmi les instances, l'ensemble premier-ordre est insatisfiable.

Mauvaise application

Prétendre qu'une seule expansion de Herbrand finie suffit toujours sans prévoir une recherche systématique ou ignorer la croissance de la complexité des termes ; interrompre prématurément la recherche peut mener à de fausses conclusions sur la satisfiabilité.

Conséquence

Transforme un problème de satisfiabilité du premier ordre en une famille (éventuellement infinie) de problèmes propositionnels attaquables par des prouveurs automatiques ; la découverte d'une expansion finie insatisfiable fournit une réfutation concrète en logique du premier ordre.

Inversion

Inversement, reconstituer des énoncés quantifiés à partir d'instanciations propositionnelles met en évidence les schémas de dépendance des quantificateurs ; la méthode aplatie les quantificateurs en termes concrets, la réversion rétablit le lien abstrait de liaison.

Limite

Efficace en logique classique du premier ordre et centrale pour le raisonnement automatique ; elle ne décide pas la satisfiabilité en général car l'expansion requise peut être non bornée, et elle doit être couplée à des stratégies de recherche, unification et conditions d'équité.

Tension sémantique

Tension entre la décidabilité propositionnelle (recherche finie par expansion) et l'indécidabilité du premier ordre (expansions potentiellement infinies), ainsi qu'entre témoins concrets ground et assertions quantifiées abstraites.

Synthèse

La méthode de Herbrand énumère systématiquement des instances ground à partir de l'univers de Herbrand pour réduire des problèmes du premier ordre à des vérifications propositionnelles : elle offre un pont constructif pour la réfutation et la recherche automatique de preuves, tout en exigeant une recherche disciplinée pour contrôler les expansions potentiellement infinies.