negacji drugim, w którym usunięte zostały wszystkie wystąpienia tego literału, oraz wszystkie klauzule zawierające jego negację usuwamy każdy zbiór klauzul zawierają klauzulę pustą – klauzula ta usuwa wszystkie inne przez subsumpcje i ma wartość fałsz, a co za tym idzie zbiór klauzul ma wartość fałsz, która jest nieistotna dla bloku będącego alternatywą
Jeśli w bloku nie ma już zbiorów klauzul twierdzenie zostało udowodnione (taki blok, jako alternatywa, jest fałszywy – skoro negacja formuły jest fałszywa, to twierdzenie to jest prawdziwe). Jeśli został jakiś pusty zbiór klauzul, twierdzenie to jest fałszywe (jego zaprzeczenie jest spełnialne).
Kategoria:Automatyczne dowodzenie twierdzeń