Teoria de Herbrand

A teoria de Herbrand foi criada por Jacques Herbrand (1908-1931), um matemático francês. Ela constata que um conjunto de ∀-sentenças Φ é insatisfatível (se tratando da lógica de primeira ordem) se e somente se existe um conjunto finito proposicionalmente instisfatível de instâncias básicas Φ₀ de Φ.

A teoria de Herbrand estabelece uma ligação entre a teoria da quantificação e a lógica sentencial. Essa ligação é importante por que proporciona um método para testar uma fórmula da teoria da quantificação por meio de testes sucessivos desta fórmula para a validação da sentença. Desde que testar a validação é um processo mecânico, o teorema de Herbrand é hoje de grande importancia para o desenvolvimente de softwares para demonstração automatizada de teoremas.