Тема посвящена рассмотрению метода доказательства того, что формула G является логическим следствием формул F1,F2,...,Fk, который называется методом резолюций. Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула G есть логическое следствие формул F1,F2,...,Fk тогда и только тогда, когда множество формул {F1,F2,...,Fk,ØG} невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода. Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).
Относительно переменных в дизъюнктах будем предполагать, что они связаны кванторами общности, но сами кванторы писать не будем. Отсюда следует, что две одинаковые переменные в разных дизъюнктах можно считать различными.
Заметим, прежде всего, что в логике первого порядка правило резолюций в прежнем виде уже не годится. Действительно, множество дизъюнктов S={P(x),ØP(a)} невыполнимо, (так как предполагается, что переменная х связана квантором общности). В то же время, если использовать правило резолюций для логики высказываний, то из S пустого дизъюнкта не получить. Содержательно понятно, что в этом случае надо сделать. Поскольку дизъюнкт P(x) можно прочитать так: для любого х истинно P(x), то P(x) истинно будет и для x=a. Сделав подстановку х=а, получим множество дизъюнктов S/={P(a),ØP(a)}. Множество S и S/ одновременно выполнимы (или невыполнимы). Но из S/ с помощью прежнего правила резолюций выводится тривиальным образом. Этот пример подсказывает, что в логике первого порядка правило резолюций надо дополнить возможностью делать подстановку.
Дадим необходимые определения.
Определение.Подстановкой называется множество равенств s={x1=t1, x2=t2,…, xn=tn}, где x1,x2,…,xn – различные переменные, t1,t2,…,tn – термы, причем терм ti не содержит переменной xi (1£ i £ n).
Если s = (x1=t1,...,xn=tn) – подстановка, а F – дизъюнкт, то через s(F) будем обозначать дизъюнкт, полученный из F одновременной заменой x1 на t1; и т.д. xn на tn. Например, если s={x1=f(x2), x2=c, x3=g(x4)), F=R(x1,x2,x3)ÚØP(f(x2)), то s(F)=R(f(x2), c, g(x4))ÚØP(f(c). Аналогично определяется действие подстановки на терм.
Для удобства введем еще и пустую подстановку – подстановку, не содержащую равенств. Пустую подстановку будем обозначать через e.
Определение. Пусть {E1,…,Ek} – множество литералов или множество термов. Подстановка s называется унификатором этого множества, если s(E1)=s(E2)=…=s(Ek). Множество унифицируемо, если существует унификатор этого множества.
Например, множество атомарных формул {Q(a,x,f(x)), Q(u,у,z)} унифицируемо подстановкой {u=a, x=у,z=f(у)}, а множество {R(x,f(x)), R(u,u)} неунифицируемо. Действительно, если заменить х на u, то получим множество {R(u,f(u), R(u,u)}.
Проводить же замену u=f(u) запрещено определением подстановки, да и бесполезно, т.к. она приводит к формулам R(f(u), f(f(u))) и R(f(u), f(u)), которые тоже различны.
Если множество унифицируемо, то существует, как правило, не один унификатор этого множества, а несколько. Среди всех унификаторов данного множества выделяют так называемый наиболее общий унификатор.
Дадим необходимые определения.
Определение. Пусть x={x1=t1, x2=t2,…, xk=tk} и h={y1=s1, y2=s2,…, yl=sl} – две подстановки. Тогда произведением подстановок x и h называется подстановка, которая получается из последовательности равенств {x1=h(t1), x2=h(t2),…,xk=h(tk), y1=s1, y2=s2,…, yl=sl} (4) вычеркиванием равенств вида xi=xi для 1£ i£ k, yj=sj, если yjÎ{x1,…, xk}, для 1 £ j £ l.
Для обозначения результата действия подстановки на дизъюнкт мы применяем префиксную функциональную запись, поэтому произведение подстановок x и h будем обозначать через h◦x, подчеркивая тем самым, что сначала действует x, а потом h.
Рассмотрим пример. Пусть x = {x=f(y), z=y, u=g(d)}, h = {x=c, y=z}. Тогда последовательность равенств (4) из определения произведения имеет вид {x=f(y), z=z, u=g(d), x=c, y=z}.
В этой последовательности вычеркнем второе и четвертое равенство получим произведение h◦x = {x=f(y), u=g(d), y=z}.
Нетрудно показать, что произведение подстановок ассоциативно, т.е. для любых подстановок x,h,x выполняется равенство x◦(h◦z)=(x◦h)◦z, и что пустая подстановка является нейтральным элементом относительно умножения. Последнее означает выполнение равенств s◦e=e◦s=s для любой подстановки s.
Произведение подстановок s = {x1=t1}○{x2=t2}○…○{xn=tn} мы будем иногда задавать последовательностью равенств: s = (x1=t1, x2=t2,…, xn=tn). Действие подстановки &s на дизъюнкт (и на терм) в этом случае состоит в последовательной (а не одновременной) замене x1 на t1, x2на t2, и т.д., xn на tn.
Определение. Унификатор s множества литералов или термов называется наиболее общим унификатором этого множества, если для любого унификатора t того же множества литералов существует подстановка x такая, что t=x○s.
Например, для множества {P(x,f(а), g(z)), P(f(b),y,v)} наиболее общим унификатором является подстановка s={x=f(b), y=f(a), v=g(z)}. Если в качестве t взять унификатор {x=f(b), y=f(a), z=c, v=g(c)}, то x={z=c}.
Если множество литералов унифицируемо, то наиболее общий унификатор существует. Это утверждение мы докажем в конце параграфа. А сейчас приведем алгоритм нахождения наиболее общего унификатора. Алгоритм называется алгоритмом унификации. Для изложения алгоритма потребуется понятие множества рассогласований.
Определение. Пусть М – множество литералов или термов. Выделим первую слева позицию, в к торой не для всех литералов стоит один и тот же символ. Затем в каждом литерале выпишем выражение, которое начинается символом, занимающим эту позицию. (Этими выражениями могут быть сам литерал, атомарная формула или терм). Множество полученных выражений называется множеством рассогласований в М.
Например, если M={P(x, f(y), a), P(x,u, g(y)), P(x, c, v)}, то первая слева позиция, в которой не все литералы имеют один и тот же символ – пятая позиция. Множество рассогласований состоит из термов f(y), u, c. Множество рассогласований {P(x, y), ØP(a, g(z))} есть само множество. Если M={ØP(x, y),ØQ(a, v)}, то множество рассогласований равно {P(x, y), Q(a, v)}.
