Проектирование систем искусственного интеллекта




Унификация


Одним из наиболее важных аспектов программирования на Прологе являются понятия унификации (отождествления) и конкретизации переменных.

Пролог пытается отождествить термы при доказательстве, или согласовании, целевого утверждения. Например, в программе из лек. 1 для согласования запроса ?- собака(Х) целевое утверждение собака (X) было отождествлено с фактом собака (реке), в результате чего переменная Х стала конкретизированной: Х= рекc.

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

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

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

Таблица 7.1. Иллюстрация унификацииТерм1Терм2Отождествимы ?
джек(Х)джек (человек)да: Х=человек
джек (личность)джек (человек)нет
джек(Х,Х)джек(23,23)да: Х=23
джек(Х.Х)джек (12,23)нет
джек( . )джек(12,23)да
f(Y,Z)Хда: X=f(Y,Z)
ХZда: X=Z
<


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