Definicja Twierdzenie Herbranda (Szukaj)

Twierdzenie Herbranda to jedno z najważniejszych twierdzeń konstruktywnych logiki pierwszego rzędu:

Formuła jest tautologiąTautologia to potocznie definicja, twierdzenie lub zdanie warunkowe, w którym występuje zapętlenie poprzez odniesienie do samego siebie. Natomiast w gramatyce tautologie są czasem stosowane dla podkreślenia czegoś, a pozorne tautologie, żeby użyć dwóch znaczeń tego samego słowa (na przykład "duże duże litery" oznacza kapitaliki dużych rozmiarów). Często jednak są po prostu błędem stylistycznym i należy starać się ich unikać....
[click for more] wtedy i tylko wtedy gdy taulogią jest pewne rozwinięcie Herbranda tej formuły.

Ponieważ każde rozwinięcie jest właściwie skończoną formułą rachunku zdań, a więc da się rozstrzygnąć w czasie skończonym (wykładniczym), ilość rozwinięć Herbranda dla formuły natomast jest zbiorem przeliczalnym, umożliwia to udowodnienie każdej tautologii logiki pierwszego rzędu, chociaż może to zająć nieograniczoną ilość czasu.

Algorytm ten wygląda tak:

n = 0;

udowodnione = false;

while(udowodnione == false)

{

Y = nte_rozwinięce_Herbranda(X,n);

Y' = przekształć_na_formułę_rachunku_zdań(Y);

if (jest_tautologią(Y'))

udowodnione = true;

else

n = n + 1;

}

wygeneruj dowód na podstawie Y;

Zobacz też: podstawowe zagadnienia z zakresu matematyki...
[click for more], Jacques Herbrand

Tresc udostepniana na licencji 'GNU Free Documentation License'.

Cache: OK - (Cache Hit) | Exec Czas: 0.026 | INTLinks: 8

Contakt: info AT definicja DOT com