Rozdział 3

Metoda rezolucji. Elementy logiki pierwszego rzędu

3.1    Metoda rezolucji dla logiki zdaniowej

3.1.1    Postać klauzulowa formuł

Definicja 3.1 Klauzulą nazywamy zbiór literałów, rozumiany domyślnie jako alternatywa tych literałów. Formułą w postaci klauzulowej nazywamy zbiór klauzul, rozumiany domyślnie jako koniunkcja tych klauzul.

Przykład 3.1 Formuła w koniunkcyjnej postaci normalnej

(~ q V ~ p V q) A {jp V ~ p V q)

ma równoważną postać klauzulową

{{~ q,~p,q},{p,~p,q}}-

3.1.2    Metoda rezolucji

Rezolucja¹ jest metodą dowodzenia przez zaprzeczenie. Korzysta ona z następujących twierdzeń:

Twierdzenie 3.1 Formuła F jest tautologią wtw, gdy ~ F jest niespeł-nialna (jest kontrtautologią).

‘John Alan Robinson, 1965.