Построение дерева вывода

Исходный текст программы
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).

Обозначение списка
[x1, x2, x3] – список из трех элементов
[x1] – список из одного элемента
[] – пустой список
При подстановке [x1, x2, x3] -> [H | Tail] будет H = x1, Tail = [x2, x3].
При подстановке [x1] -> [H | Tail] будет H = x1, Tail = [].

Разделы программы
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).

Виды аксиом
Факт:
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)

Целевая формула
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).

Шаг 0

Поиск подходящего правила
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).

Шаг 1: Конкретизация

Шаг 1

Поиск подходящего правила
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).

Шаг 2: Конкретизация

Шаг 2

Шаг последний

Решение
Целевая формула
accessible(b1, [X1, X1, X1], b4)
доказана в виде
accessible(b1, [x1, x1, x1], b4),
значит, решение:
X1 = x1.

Составная цель
goal
transition(B1, X, B2), B1 = B2.
transition(B1, X, B2), B1 = B2.
transition(B1, X, B2)
B1 = B2