Rozwinięcie Herbranda
Z Wikipedii
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) zostały zastąpione przez koniunkcje natomiast egzystencjalne przez alternatywę , gdzie to pewien podzbiór skończony uniwersum Herbranda.
Taka formuła - bez zmiennych i kwantyfikatorów jest w praktyce równoważna pewnej formule rachunku zdań.
Zbiór rozwinięć Herbranda jest co najwyżej przeliczalny.