Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

4. Множество рассогласований для S2 равно: ^2 = {g(y), и}, тогда ВНОВЬ строим: вз = 62 °{g(y)/u} = {a/z,f(a)/x, g(y)/u} и 8з= Se^ = {Р(а, f(a)), f(g(y)), Р(а, f(a), f(g(y)))} = {P(a, f(a), f(g(y)))} и S3- единичный дизъюнкт, следовательно, вз наиболее общий унификатор. Рассмотрим еще один пример. Пусть S = {Q(f(a), g(x)), Q(y, у)}. Пустая подстановка £ . 50 = S-HQ единичный дизъюнкт и ^0 = {f(a), у}, 01 = £ °{f(a)/y} = {f(a)/y}, 51 = = {Q(f(^)' g(^))' Q(f(^)'f(^))} и 5*7 - не единичный дизъюнкт. Wi = {g(x),f(a)}. В множестве Wj нет переменной как элемента этого множества. Следова­ тельно, алгоритм унификации завершается, и делаем заключение, что S не уни­ фицируемо. § 9. Метод резолюций в логике предикатов Метод резолюций в логике предикатов, как и логике высказываний, применяется к множеству дизъюнктов. Отличие метода резолюций в логике предикатов состоит в дополнительной процедуре работы с термами для унифи­ кации формул. Пусть имеем множество литер {Li}. Если для некоторого подмножества этого множества существует общий унификатор di, например, (Li) 0^ = (Ь2)$^ = то из этих трех литер достаточно оставить только одну. Если для некото­ рых оставшихся существует общий унификатор 62, например, (Ьз)0^ = (Ь4)0^, то тоже оставляем только одну из них и т.д. Пример. Пусть D = P(f(a)) vP(x) vQ(a,f(u)) vQ(x,f(b)) vQ(z,w). Тогда: в= {a/x, b/u, a/z,f(b)/w}, Dg= P(f(a)) vP (a) vQ (a ,f(b)). Если две или более литер дизъюнкта D имеют наиболее обпщй унификатор 9: (Li)e =(Lj)e =(L]^e , то оставление одного из этих литералов вместо всех них называют склейкой. Пусть имеем два дизъюнкта Dj я D2 я переменные, входящие в Z)^, не вхо­ дят в D2 и обратно. Если это не так, то переименованием переменных этого можно добиться. Пусть в Dj есть литера, например, Lj, а в - литера L2. Если Lj и —1L2 имеют наиболее общий унификатор в, т. е. (Li)e = (—^2)0, то новый дизъюнкт/?: 76