Método de Herbrand

Una técnica proof-teórica que reduce la satisfactibilidad de primer orden a la satisfactibilidad proposicional construyendo conjuntos finitos (o efectivamente enumerables) de instancias ground — expansiones de Herbrand — basadas en el universo de Herbrand.