Математическая логика и теория алгоритмов

1. Пустая подстановка е : So = 5 - не единичный дизъюнкт, следовательно, не получили наиболее общий унификатор, 2. Множество ра:ссогласования равно: fFo = {а. z), следовательно, 0) =s ° {a/z}, тогда = S ' Q , = {F(a, x,P(a,J{a), Ди))}, S\ - не единичный дизъюнкт. 3. Множество рассогласований для S\ равно: w, = {x,m}. тогда 02 = 01° {/(а)/х} = {a/z, J{a)/x}, и Si = S q ^ = {Р(а, Да)), Д^(у)), Р(а, Да), Дм))}. S2 - не единичный дизъюнкт. 4. Множество рассогласований для S2 равно: wi = {gO), тогда вновь строим: 0з = 02 ° {g(y)/ «] ~ {a/z,f{a)lx, g(y)lu} и = {Pici. Аа)\ Д^О)), Р{а, Да), Аё(У)))) = {Р(«, Д«), Д^О)))}- S-i - единичный дизъюнкт, следовательно, 0з наиболее общий унификатор. Рассмотрим еще пример. Пусть S = {Q(J{d), gix)), Q(y, у)}. Пус­ тая подстановка s; iSo = 5*- не единичный дизъюнкт и W q = {Да), у}, 01 = £ ° т/у) = miy)> = 5-0, = {qm> g{^)i qm> д ^ » } . - не единичный дизъюнкт; JVi = {g(x),Jla)}. В множестве Щ нет переменной как элемента этого множества. Следовательно, алгоритм унификации завершается, делаем заключе­ ние, что S не унифицируемо. Насколько я могу судить, это один из тех несложных случаев, которые чрезвычайно трудны (ШерлокХолмс). А. К, Дойль § 10. Метод резолюций в логике предикатов В логике высказываний метод резо/поций применялся к множеству дизъюнктов, которые были формулами логики высказываний. 110