Problem sprawdzenia, czy formuła klasycznej logiki predykatów jest tautologią, jest nierozstrzygalny. Jeśli dana formuła rachunku predykatów jest tautologią, to umiemy się o tym przekonać w skończonym czasie. Jeśli jednak nie jest to tautologia, to nie ma takiej metody, która po skończonej liczbie kroków pozwoliłaby przerwać postępowanie i zdecydować, że to nie jest tautologia. J
Cytat pochodzi z ... 15_p5.html
Nie mogę zrozumieć dlaczego jest to problem nieroztrzygalny. Przecież wystarczy sprawdzić wszystkie możliwości, których jest \(\displaystyle{ 2^n}\) gdzie \(\displaystyle{ n}\) to ilość klauzul, które przyjmują wartość 0/1. Sprawdzamy wszystkie możliwości. Jeżeli któraś wyewaluuje nam wartość zdania do fałszu to mamy rozstrzygnięcie.
Masz rację. W takim razie nie mogę zrozumieć dlaczego niby jeżeli formuła jest tautologią to wtedy da się to sprawdzić. Przecież być może też należy sprawdzić wszystkie możliwości ( których jest nieskończenie wiele).
Da się sprawdzić, bo istnieje aksjomatyczne ujęcie rachunku predykatów. Takie, że każda tautologia da się wyprowadzić z aksjomatów przy pomocy skończonej liczby reguł wnioskowania, w skończenie wielu krokach. To jest wynik Goedla (zupełność klasycznego rachunku predykatów).
