Méthode de Herbrand

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.