Rozwinięcie Herbranda

Rozwinięcie Herbranda dla formuły rachunku predykatów pierwszego rzędu to formuła, w której wszystkie kwantyfikatory ogólne (a także zmienne wolne) $\forall x . \phi(x)$ zostały zastąpione przez koniunkcje $\phi(t_1) \and \phi(t_2) \and \cdots \and \phi(t_n)$ natomiast egzystencjalne $\exists x . \phi(x)$ przez alternatywę $\phi(t_1) \or \phi(t_2) \or \cdots \or \phi(t_n)$ , gdzie $t_1, t_2, \dots, t_n$ to pewien podzbiór skończony uniwersum Herbranda.