8. Подстановка и унификация

Тема посвящена рассмотрению метода доказательства того, что формула G является логическим следствием формул F₁,F₂,...,F_k, который называется методом резолюций. Отметим, что задача о логическом следствии сводится к задаче о выполнимости. Действительно, формула G есть логическое следствие формул F₁,F₂,...,F_k тогда и только тогда, когда множество формул {F₁,F₂,...,F_k,G} невыполнимо. Метод резолюций, если говорить более точно, устанавливает невыполнимость. Это первая особенность метода. Вторая особенность метода состоит в том, что он оперирует не с произвольными формулами, а с дизъюнктами (или элементарными дизъюнкциями).

Относительно переменных в дизъюнктах будем предполагать, что они связаны кванторами общности, но сами кванторы писать не будем. Отсюда следует, что две одинаковые переменные в разных дизъюнктах можно считать различными.

Заметим, прежде всего, что в логике первого порядка правило резолюций в прежнем виде уже не годится. Действительно, множество дизъюнктов S={P(x),P(a)} невыполнимо, (так как предполагается, что переменная х связана квантором общности). В то же время, если использовать правило резолюций для логики высказываний, то из S пустого дизъюнкта не получить. Содержательно понятно, что в этом случае надо сделать. Поскольку дизъюнкт P(x) можно прочитать так: для любого х истинно P(x), то P(x) истинно будет и для x=a. Сделав подстановку х=а, получим множество дизъюнктов S^/={P(a),P(a)}. Множество S и S^/ одновременно выполнимы (или невыполнимы). Но из S^/ с помощью прежнего правила резолюций выводится тривиальным образом. Этот пример подсказывает, что в логике первого порядка правило резолюций надо дополнить возможностью делать подстановку.

Дадим необходимые определения.

Определение. Подстановкой называется множество равенств s={x₁=t₁, x₂=t₂,…, x_n=t_n}, где x₁,x₂,…,x_n – различные переменные, t₁,t₂,…,t_n – термы, причем терм t_i не содержит переменной x_i (1 i  n).

Если s = (x₁=t₁,...,x_n=t_n) – подстановка, а F – дизъюнкт, то через s(F) будем обозначать дизъюнкт, полученный из F одновременной заменой x₁ на t1; и т.д. x_n на t_n. Например, если s={x₁=f(x₂), x₂=c, x₃=g(x₄)), F=R(x₁,x₂,x₃)P(f(x₂)), то s(F)=R(f(x₂), c, g(x₄))P(f(c). Аналогично определяется действие подстановки на терм.

Для удобства введем еще и пустую подстановку – подстановку, не содержащую равенств. Пустую подстановку будем обозначать через e.

Определение. Пусть {E₁,…,E_k} – множество литералов или множество термов. Подстановка s называется унификатором этого множества, если s(E₁)=s(E₂)=…=s(E_k). Множество унифицируемо, если существует унификатор этого множества.

Например, множество атомарных формул {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={x₁=t₁, x₂=t₂,…, x_k=t_k} и h={y₁=s₁, y₂=s₂,…, y_l=s_l} – две подстановки. Тогда произведением подстановок x и h называется подстановка, которая получается из последовательности равенств {x₁=h(t₁), x₂=h(t₂),…,x_k=h(t_k), y₁=s₁, y₂=s₂,…, y_l=s_l}    (4) вычеркиванием равенств вида x_i=x_i для 1 i k, y_j=s_j, если y_jÎ{x₁,…, x_k}, для 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 = {x₁=t₁}○{x₂=t₂}○…○{x_n=t_n} мы будем иногда задавать последовательностью равенств: s = (x₁=t₁, x₂=t₂,…, x_n=t_n). Действие подстановки &s на дизъюнкт (и на терм) в этом случае состоит в последовательной (а не одновременной) замене x₁ на t₁, x₂на t₂, и т.д., x_n на t_n.

Определение. Унификатор 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)}.