Интеллектуальные информационные системы. Макаренко С.И. - 125 стр.

     В заключение раздела дадим формальное определение синтаксиса
Пролога, используя форму записи Бэкуса-Наура, иногда называемую
бэкусовской нормальной формой (БНФ).
     запрос ::- голова утверждения
     правило ::– голова утверждения :- хвост утверждения
     факт ::- голова утверждения
     голова утверждения ::-атом | структура
     хвост утверждения ::- атом структура,
     термы ::-терм [,термы]
     терм ::- число | переменная | атом | структура
     структура ::-атом (термы)
     Данное определение синтаксиса не включает операторную, списковую
и строковую формы записи. Однако, любая программа на Прологе может
быть написана с использованием вышеприведенного синтаксиса.
Специальные формы только упрощают понимание программы. Как мы
видим, синтаксис Пролога не требует пространного объяснения. Но для
написания хороших программ необходимо глубокое понимание языка.

                          14.5 Унификация

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

                                  124