Средства разработки приложений


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


Подстановка — это множество вида {x1/t1,..., xn/tn}, где для всех i, xi — переменная, а ti — терм, причем xi≠ti (отображение переменных в термы). При этом все переменные, входящие в подстановку, различны (для любого i≠j xi≠xj).

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

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

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

Если 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}.




Начало  Назад  Вперед



Книжный магазин