Пролог «под капотом». Лекция 2

1.

Лекция 2
ПРОЛОГ «ПОД КАПОТОМ»

2.

ЛОГИЧЕСКОЕ СЛЕДСТВИЕ
Правило подстановки. Подстановкой
называется конечное (возможно, пустое)
множество Ω пар вида Xi= ti, где Xi–
переменная и ti– терм; Xi≠ Xj при i≠ j и Xi не
входит в tj при любых i и j.
Ω1={X=вася},
man(X). Ω1 man(вася).
Ω2={X=вася, Y=маша}
нравится(X,Y). Ω2 нравится(вася, маша).

3.

ЛОГИЧЕСКОЕ СЛЕДСТВИЕ
Правило обобщения. Целевое утверждение A
истинно, если существует хотя бы одна такая
подстановка Ω в A, что получившийся в
результате терм является логическим
следствием программы.

4.

ЛОГИЧЕСКОЕ СЛЕДСТВИЕ
Правило конкретизации. При выполнении
подстановки Ω в целевое утверждение A
переменные, входящие в A принимают
конкретные значения или, как говорят,
конкретизируются. Из утверждения A,
содержащего переменные, всегда выводится
утверждение, полученное в результате
выполнения любой подстановки Ω в A.

5.

МЕХАНИЗМ УНИФИКАЦИИ
Унификатором двух термов называется такая
подстановка, которая делает эти два терма
одинаковыми
pair (‘Петр I’, ‘Екатерина I’) .
Для термов
pair(‘Петр I’, X) и pair(Y, ‘Екатерина I’)
унификатор: {X= ‘Екатерина I’, Y= ‘Петр I’}
pair(‘Петр I’, ‘Екатерина I’)

6.

ПРАВИЛА УНИФИКАЦИИ ДВУХ ТЕРМОВ
1. Если оба терма – константы, они должны
совпадать:
собака(рекс) и собака(феликс)
2. Если один из термов - не
конкретизированная переменная, то второй
терм может быть любым:
man(X) и man(вася) Х=вася
man(X) и man(Y) Х=Y - сцеплены

7.

ПРАВИЛА УНИФИКАЦИИ ДВУХ ТЕРМОВ
3. Если оба терма – структуры, то должны
совпадать имена и количество их аргументов,
а также сопоставляться между собой все
компоненты этих структур:
book(Author,Title) и book(james,’The tree’)
Author = james, Title=’The tree’
book(Author,Title) и book(james) false

8.

УНИФИКАЦИЯ
Терм 1
Терм 2
джек (Х)
джек (человек)
джек (личность)
джек (человек)
джек (Х,Х)
джек (23,23)
джек (Х,Х)
джек (12,23)
f(Y,Z)
Х
Х
Z

9.

УНИФИКАЦИЯ
?- нравится(X,X).
false
?- нравится(_,_).
true

10.

ДОКАЗАТЕЛЬСТВО ЦЕЛИ
1) совпадение: из Р выводимо Р. Если
тождественный цели факт найден, ответом
будет true. Иначе ответом будет false.
?-собака(рекс).
true

11.

ДОКАЗАТЕЛЬСТВО ЦЕЛИ
2) обобщение - это поиск с помощью
подстановки (от частного к общему)
?-собака(Х).
Х=рекс
Х=лиза
Х=джек

12.

ДОКАЗАТЕЛЬСТВО ЦЕЛИ
3) конкретизация – от общего к частному, а
не наоборот
плюс(0,Х,Х).
?-плюс(0,2,2).
true

13.

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

14.

МЕТОД РЕЗОЛЮЦИЙ (РЕДУКЦИЯ ЦЕЛИ)
Начинается с исходного вопроса G1 и
завершается успехом или отказом
Тело цели заменяется телом того правила из
программы, чей заголовок совпадает с целью
На каждом этапе редукции имеется некоторая
резольвента (конъюнкция подцелей) Gi, которые
следует доказать.
Выбираются такая цель в резольвенте и такое
предложение в логической программе, что
заголовок предложения унифицируем с целью

15.

ПРИМЕР
● mother(‘Даша’,’Маша’).
● mother(‘Наташа’,’Даша’).
● mother(‘Наташа’,’Глаша’).
grandmother(X,Y):– mother(X,Z), mother(Z,Y).
?-grandmother(B,V).
B=X, V=Y mother(X,Z), mother(Z,Y)
●{ X=‘Даша’, Z=‘Маша’} mother(‘Маша’,Y) fail
●{ X= ‘Наташа’, Z=‘Даша’} mother(‘Даша’,Y)
{Y=‘Маша’} true, B= ‘Наташа’, V=‘Маша’
●{ X= ‘Наташа’, Z=‘Глаша’} mother(‘Глаша’,Y) fail

16.

Знак = это механизм унификации
Унифицируйте:
N=N+1
Унифицируйте:
N1=N+1