Rozpisując te wyrażenia będzie to:
– użyta substytucja,
– – najmniejszy unifikator i
lub też negacja będzie w zamiast w co nie zmienia dowodu.
Ponieważ i mają z definicji rozłączne zmienne Tak więc i można zunifikować w za pomocą Każdy unifikator można rozbić na najmniejszy wspólny unifikator i jakieś podstawienie – niech będzie najmniejszym wspólnym unifikatorem, a takim podstawieniem, że
Tak więc możemy zmienić ten dowód na: rezolwuje się z dając przez substytucję przechodzi w
Teraz (pamiętając o składaniu substytucji) dojdziemy w końcu do sytuacji gdzie przenosimy substytucję (która mogła już osiągnąć gigantyczne rozmiary) przez ostatnią rezolucje. Ponieważ jednak podstawienie to zachodzi dla klauzuli pustej – w rzeczywistości możemy je zupełnie odrzucić.
Tak więc rezolucja bez dodatkowych zasad jest zupełna.
Linki zewnętrzne
Kategoria:Logika matematyczna