Слайд 2
Исходный текст программы
domains
list=symbol*
predicates
nondeterm transition(symbol, symbol, symbol)
nondeterm accessible(symbol, list, symbol)
clauses
transition(b1, x1, b2).
transition(b2, x1,
b3).
transition(b3, x1, b4).
transition(b4, x1, b1).
transition(b1, x2, b4).
transition(b2, x2, b3).
transition(b3, x2, b2).
transition(b4, x2, b1).
accessible(B1, [X], B2) :- transition(B1, X, B2).
accessible(B1, [X|Rest], B2) :- transition(B1, X, B3), accessible(B3, [Rest], B2).
goal
accessible(b1, [X1, X1, X1], b4).
Слайд 3
Обозначение списка
[x1, x2, x3] – список из трех
элементов
[x1] – список из одного элемента
[] – пустой список
При
подстановке [x1, x2, x3] -> [H | Tail] будет H = x1, Tail = [x2, x3].
При подстановке [x1] -> [H | Tail] будет H = x1, Tail = [].
Слайд 4
Разделы программы
domains
list=symbol*
predicates
nondeterm transition(symbol, symbol, symbol)
nondeterm
accessible(symbol, list, symbol)
clauses
transition(b1, x1, b2).
transition(b2, x1, b3).
transition(b3, x1, b4).
transition(b4, x1, b1).
transition(b1, x2, b4).
transition(b2, x2, b3).
transition(b3, x2, b2).
transition(b4, x2, b1).
accessible(B1, [X], B2) :- transition(B1, X, B2).
accessible(B1, [X|Rest], B2) :- transition(B1, X, B3), accessible(B3, [Rest], B2).
goal
accessible(b1, [X1, X1, X1], b4).
Слайд 5
Виды аксиом
Факт:
transition(b1, x1, b2).
|||
transition(b1, x1, b2) = ИСТИНА
Правило:
accessible(B1,
[X|Rest], B2) :- transition(B1, X, B3), accessible(B3, [Rest], B2).
|||
accessible(B1,
[X|Rest], B2) ← transition(B1, X, B3) & accessible(B3, [Rest], B2)
Слайд 6
Целевая формула
domains
list=symbol*
predicates
nondeterm transition(symbol, symbol, symbol)
nondeterm
accessible(symbol, list, symbol)
clauses
transition(b1, x1, b2).
transition(b2, x1, b3).
transition(b3, x1, b4).
transition(b4, x1, b1).
transition(b1, x2, b4).
transition(b2, x2, b3).
transition(b3, x2, b2).
transition(b4, x2, b1).
accessible(B1, [X], B2) :- transition(B1, X, B2).
accessible(B1, [X|Rest], B2) :- transition(B1, X, B3), accessible(B3, [Rest], B2).
goal
accessible(b1, [X1, X1, X1], b4).
Слайд 8
Поиск подходящего правила
domains
list=symbol*
predicates
nondeterm transition(symbol, symbol, symbol)
nondeterm accessible(symbol, list, symbol)
clauses
transition(b1, x1, b2).
transition(b2, x1,
b3).
transition(b3, x1, b4).
transition(b4, x1, b1).
transition(b1, x2, b4).
transition(b2, x2, b3).
transition(b3, x2, b2).
transition(b4, x2, b1).
accessible(B1, [X], B2) :- transition(B1, X, B2).
accessible(B1, [X|Rest], B2) :- transition(B1, X, B3), accessible(B3, [Rest], B2).
goal
accessible(b1, [X1, X1, X1], b4).
Слайд 11
Поиск подходящего правила
domains
list=symbol*
predicates
nondeterm transition(symbol, symbol, symbol)
nondeterm accessible(symbol, list, symbol)
clauses
transition(b1, x1, b2).
transition(b2, x1,
b3).
transition(b3, x1, b4).
transition(b4, x1, b1).
transition(b1, x2, b4).
transition(b2, x2, b3).
transition(b3, x2, b2).
transition(b4, x2, b1).
accessible(B1, [X], B2) :- transition(B1, X, B2).
accessible(B1, [X|Rest], B2) :- transition(B1, X, B3), accessible(B3, [Rest], B2).
goal
accessible(b1, [X1, X1, X1], b4).
Слайд 15
Решение
Целевая формула
accessible(b1, [X1, X1, X1],
b4)
доказана в виде
accessible(b1, [x1, x1, x1], b4),
значит,
решение:
X1 = x1.
Слайд 16
Составная цель
goal
transition(B1, X, B2), B1 =
B2.
transition(B1, X, B2), B1 = B2.
transition(B1, X, B2)
B1 =
B2
![Обозначение списка[x1, x2, x3] – список из трех элементов[x1] – список из](/img/tmb/15/1464935/e4494dc36e40e1c9de3d5a59cb2afb9f-720x.jpg "Построение дерева вывода")
![Виды аксиомФакт:transition(b1, x1, b2).|||transition(b1, x1, b2) = ИСТИНАПравило:accessible(B1, [X|Rest], B2) :- transition(B1,](/img/tmb/15/1464935/16abebd00d37a109a2ebc14d81e96e8a-720x.jpg "Построение дерева вывода")
![РешениеЦелевая формула accessible(b1, [X1, X1, X1], b4)доказана в виде](/img/tmb/15/1464935/e670de57b77abbf44e208d3a4729870e-720x.jpg "Построение дерева вывода")
