Логическо програмиране 2004/05 - упражнения

Да разгледаме следната задача:

Задача. Да се докаже, че дизюнктите D₁ = { p(X), p(f(Y)) } и D₂ = { !p(U), !p(f(V)) } са несъвместими.

Решение: Ако се опитаме да търсим резолвента на двата дизюнкта, ще стигнем отново до дизюнкт с два литерала. Въобще изглежда, че нямаме шанс да получим празния дизюнкт с резолюция. Въпреки това двата дизюнкта са несъвместими, в това може да се убедите, ако разгледате съответната формула $$(\forall X p(X) \vee \forall Y p(f(Y))) \& (\forall U \neg p(U) \vee \forall V \neg p(f(V)))$$.

Задачата се решава с колапс на дизюнкти. Казваме, че един дизюнкт D колабира, ако има два литерала $$L_1,L_2\in D$$, които могат да се унифицират. Тогава, ако $$\sigma$$ е общ унификатор на L₁ и L₂, то в частния случай $$D\sigma$$ съответните частни случаи на литералите L₁ и L₂ ще се слеят. Така ще получим дизюнкт с по-малко елементи. В случай можем да колабираме D₁ със $$\sigma_1 = [X/f(Y)]$$ и D₂ със $$\sigma_2 = [U/f(V)]$$. Тогава очевидно $$D_1\sigma_1 = \{ p(f(Y)) \}$$, а $$D_2\sigma_2 = \{ \neg p(f(V)) \}$$, които очевидно имат обща резолвента празния дизюнкт с помощта на субституцията [Y/V].