Основы современных компьютерных технологий


Пролог и логическое программирование - часть 4


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

Пусть имеются два терма t1=ОТЕЦ(Х,У) и t2=ОТЕЦ("ПЕТР", "ПАВЕЛ"). Унификатором этих двух термов будет подстановка ?=(Х="ПЕТР", Y="ПАВЕЛ"), т.е. если в терм t1 вместо переменных X и Y подставить значения из соответствующих мест терма t2, термы станут одинаковыми, а значением их будет пример ОТЕЦ("ПЕТР", "ПАВЕЛ").

Пусть теперь t1=ОТЕЦ(Х,"ИВАН") и t2=ОТЕЦ("ПЕТР", "ПАВЕЛ"). В этом случае унификация невозможна, так как с помощью подстановки термы нельзя сделать одинаковыми - на втором месте в обоих термах стоят разные константные выражения. Если бы термы были, например, вида t1=ОТЕЦ(Х,"ИВАН") и t2=ОТЕЦ("ПЕТР",Z), тогда ?=(Х="ПЕТР", Z="ИBAH"), и пример для этих термов ОТЕЦ("ПЕТР", "ИВАН").

Правило резолюции позволяет из дизъюнктов

D1 = ¬ A1(t) ? A2 ? ... ?An

D2 = ¬ A1(s) ? B1 ? ... ? Bm

получить новый дизъюнкт D = Q(A2 ?... ? An ? B1 ?... ? Bm).

Здесь ? - наиболее общий унификатор термов t и s, обеспечивает их равенство и означает, что все подстановки унификатора выполнены для всех атомов, входящих в дизъюнкты D1 D2. Дизъюнкты D1 D2 называют родителями дизъюнкта D. В дизъюнкте D отсутствует пара: A (? t)? A1 (?s), при этом (?t) = (?s) и пара является тавтологией (тождественно-истинной) и может быть удалена из дальнейших вычислений, что и выполняет правило резолюции.

Правило склейки позволяет из дизъюнкта A(t) ?A(s) ? B1 ?...? Bn получить дизъюнкт ?(A(t) ? B1.? ... ? Bn), т.е. осуществляется "склеивание" одинаковых атомов, полученных после унифицирующей подстановки ?t = ?s.

306

Работу метода резолюции опишем на примере, приведенном ранее. Запишем множество утверждений и фактов в виде логической программы, используя прологообразный синтаксис:




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