Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов

Первый шаг. Приводим исходную формулу к предваренной нормальной форме. Для этого:

пользуясь эквивалентностью A
B
¬A
B исключим импликацию;
перенесем все отрицания внутрь формулы, чтобы они стояли только перед атомными формулами, используя следующие эквивалентности:

¬(A
B)
¬A
¬B ¬(A
B)
¬A
¬B ¬(
xA)

x¬A ¬(
xA)

x¬A ¬¬A
A
переименовываем связанные переменные так, чтобы ни одна переменная не входила в нашу формулу одновременно связанно и свободно.
выносим кванторы в начало формулы, используя эквивалентности:

QxA(x)
B
Qx(A(x)
B), если B не содержит переменной x, а Q
{
,
}

QxA(x)
B
Qx(A(x)
B), если B не содержит переменной x, а Q
{
,
}
xA(x)

xB(x)

x(A(x)
B(x))
xA(x)

xB(x)

x(A(x)
B(x))

Q1xA(x)
Q2xB
Q1xQ2y(A(x)
B(y)), где Q
{
,
}

Q1xA(x)
Q2xB
Q1xQ2y(A(x)
B(y)), где Q
{
,
}

Второй шаг. Проведем сколемизацию, т.е. элиминируем в формуле кванторы существования. Для этого для каждого квантора существования выполним следующий алгоритм.

Если устраняемый квантор существования — самый левый квантор в префиксе формулы, заменим все вхождения в формулу переменной, связанной этим квантором, на новую константу и вычеркнем квантор из префикса формулы.

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

Проведя этот процесс для всех кванторов существования, получим формулу, находящуюся в сколемовской нормальной форме. Алгоритм устранения кванторов существования придумал Сколем в 1927 году.

Имеет место теорема о том, что формула и ее сколемизация эквивалентны в смысле выполнимости.

Третий шаг. Элиминируем кванторы всеобщности. Полученная формула будет бескванторной и эквивалентной исходной в смысле выполнимости.

Четвертый шаг. Приведем формулу к конъюнктивной нормальной форме, для чего воспользуемся эквивалентностями, выражающими дистрибутивность:

C) A

Пятый шаг. Элиминируем конъюнкции, представляя формулу в виде множества дизъюнктов.

Получаем множество дизъюнктов, эквивалентное исходной формуле в том смысле, который дает нам следующая теорема.

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

Напомним, что множество формул называется невыполнимым, если не существует такого означивания переменных, чтобы все формулы из этого множества были бы истинными.

Пример. Превратим формулу

x(P(x)

y(P(y)

¬Q(x,y))) в эквивалентное ей множество дизъюнктов.

Первый шаг. Приведем исходную формулу к предваренной нормальной форме. Элиминировав импликацию, получим формулу

x(¬P(x)

y(P(y)

¬Q(x,y))). Вынесем переменную y за скобки:

y(¬P(x)

(P(y)

¬Q(x,y))). Это можно сделать, потому что формула ¬P(x) не зависит от переменной y. Если бы она зависела, то можно было бы переименовать связанную переменную y.

Второй шаг. Проведем сколемизацию полученной формулы. Левее квантора существования стоит квантор всеобщности, значит, нужно заменить все вхождения переменной y новым унарным функциональным символом, зависящим от x. Получим формулу, находящуюся в сколемовской нормальной форме:

x(¬P(x)

(P(f(x)

¬Q(x,f(x)))).

Третий шаг. Элиминируем квантор всеобщности: ¬P(x)

(P(f(x))

¬Q(x,f(x))).

В четвертом и пятом шагах необходимости нет, поскольку формула уже представляет собой дизъюнкт: ¬P(x)

P(f(x))

¬Q(x,f(x)).

Следующая техника, лежащая в основе Пролога, с которой мы попробуем разобраться, — это унификация. Унификация позволяет отождествлять формулы логики первого порядка путем замены свободных переменных на термы.

Подстановка — это множество вида {x1/t1,..., xn/tn}, где для всех i, xi — переменная, а ti — терм, причем xi

ti (отображение переменных в термы). При этом все переменные, входящие в подстановку, различны (для любого i

j xi

xj).

Символом ? будем обозначать пустую подстановку.

Подстановка, в которой все термы основные, называется основной подстановкой.

Простое выражение — это терм или атомная формула.

Если A — простое выражение, а ? — подстановка, то A? получается путем одновременной замены всех вхождений каждой переменной из A соответствующим термом. A? называется частным случаем (примером) выражения A. Содержательно подстановка заменяет каждое вхождение переменной xi на терм ti.

Пусть ? и ? — подстановки, ?={x1/t1,..., xn/tn}, ?={y1/s1,...,yn/sn}. Композиция ?? получается из множества {x1/t1?,...,xn/tn?,y1/s1,..., yn/sn} удалением пар xi/ti?, где xi

ti? и пар yi/si, где yi совпадает с одним из xj.

Пример. Пусть ?={x/f(y),y/z}, ?={x/a,y/b,z/y}. Построим ??. Для этого возьмем множество {x/f(b),y/y,x/a,y/b,z/y} и выбросим из него пары y/y (потому что заменяемая переменная совпадает с термом), ,x/a,y/b (потому что заменяемая переменная из подстановки ? совпадает с заменяемой переменной из подстановки ?). Получим ответ: ??={x/f(b),z/y}.

Подстановка ? называется более общей, чем подстановка ?, если существует такая подстановка ?, что ?=??.

Подстановка ? называется унификатором простых выражений A и B, если A?=B?. Про A и B в такой ситуации говорят, что они унифицируемы. Унификация используется в Прологе для композиции и декомпозиции структур данных.

Пример. A=p(f(x),z) и B=p(y,a) унифицируемы. Можно взять в качестве их унификатора подстановку {y/f(x),z/a} или подстановку {y/f(a),x/a,z/a}.

Вообще говоря, две формулы могут иметь бесконечно много унификаторов. Унификатор ? называют наиболее общим (или простейшим) унификатором простых выражений A и B, если он является более общей подстановкой, чем все другие унификаторы простых выражений A и B.

Пример. В рассмотренном выше примере наиболее общим унификатором является подстановка {y/f(a),z/a}.

Пусть S — конечное множество простых выражений. Определим множество d(S) разногласий (рассогласований). Зафиксируем самую левую позицию, на которой не во всех выражениях из S стоит один и тот же символ. Занесем в d(S) подвыражения выражений из S, начинающиеся с этой позиции.

Пример. Пусть S={p(f(x),h(y),a),p(f(x),z,a),p(f(x),h(y),b)}.Множество рассогласований для S d(S)={h(y),z}.

Содержание раздела