Kończąc naszą dyskusję na temat rozdzielczości, pokazujemy teraz, dlaczego PL-RESOLUTION jest kompletne. Aby to zrobić, wprowadzamy zamknięcie rozdzielczości RC(S) zbioru klauzul , który jest zbiorem wszystkich klauzul, które można wyprowadzić przez wielokrotne zastosowanie reguły rozwiązywania do klauzul w S lub ich pochodnych. Zamknięcie rozdzielczości jest tym, co PL-RESOLUTION oblicza jako końcową wartość klauzul zmiennych. Łatwo zauważyć, że RC(S) musi być skończony: dzięki etapowi rozkładania na czynniki istnieje tylko skończenie wiele odrębnych klauzul, które można skonstruować z symboli P1 … Pk występujących w S . Dlatego PL-RESOLUTION zawsze się kończy.
Twierdzenie o zupełności dla rozwiązania w logice zdań nazywa się twierdzeniem o rozdzielczości podstawowej: Jeśli zbiór klauzul jest niezadowalający, to zamknięcie rozdzielczości tych klauzul zawiera pustą klauzulę.
Twierdzenie to jest udowodnione przez wykazanie jego przeciwieństwa: jeśli domknięcie RC(S) nie zawiera pustego zdania, to S jest spełnialne. W rzeczywistości możemy skonstruować model dla S z odpowiednimi wartościami prawdy dla P1 … Pk. Procedura budowy wygląda następująco:
Dla od 1 do k ,
– Jeśli klauzula w RC(S) zawiera literał ¬Pi i wszystkie inne literały są fałszywe w ramach przypisania wybranego dla P1 … Pi-1 , przypisz false do Pi.
– W przeciwnym razie przypisz true do Pi .
To przypisanie do P1 … Pk jest modelem S . Aby to zobaczyć, załóżmy odwrotnie – że na pewnym etapie sekwencji przypisanie symbolu Pi powoduje, że pewna klauzula C staje się fałszywa. Aby tak się stało, musi być tak, że wszystkie inne literały w C muszą już zostać sfałszowane przez przypisania do Pi … Pi-1. Tak więc C musi teraz wyglądać albo (false V false V false … false V Pi) albo jak (false V false V false … false V ¬). Jeśli tylko jedna z tych dwóch klauzul jest w RC(S), algorytm przypisze odpowiednią wartość prawdy do Pi aby C była prawdziwa, więc C może zostać sfalsyfikowana tylko wtedy, gdy obie te klauzule są w RC(S). Teraz, ponieważ RC(S) jest zamykany podczas rozwiązywania, będzie zawierał rezolucję z tych dwóch klauzul, a ta rezolucja będzie miała wszystkie swoje literały już sfalsyfikowane przez przypisania do Pi…Pi-1 . Przeczy to naszemu założeniu, że pierwsze zdanie sfalsyfikowane pojawia się na etapie. Dlatego udowodniliśmy, że konstrukcja nigdy nie fałszuje zdania w RC(S); to znaczy tworzy model RC(S). Wreszcie, ponieważ S jest zawarty w RC(S), każdy model RC(S) jest modelem samego siebie S