Основы программирования на языке Пролог



         

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


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

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




Содержание  Назад  Вперед