Rozwinięcie Herbranda

Z Wikipedii, wolnej encyklopedii

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.

Zobacz też[edytuj | edytuj kod]