% Известен ли ответ для всех конкретизации утверждения Цель?
ответпольз( Цель, Копия, _, Ответ, _ ) :-
сказано( Копия, Ответ, _ ),
конкретизация( Копия, Цель), !. % Ответ известен
% Найти все известные решения для Цель с индексами, начиная с N
ответпольз( Цель, _, _, правда, N) :-
сказано( Цель, правда, М),
М >= N.
% Все уже сказано об утверждении Цель?
ответпольз( Цель, Копия, _, Ответ, _) :-
конец_ответов( Копия),
конкретизация( Копия, Цель), !, % Уже все сказано
fail.
% Попросить пользователя дать (еще) решения
ответпольз( Цель, _, Трасса, Ответ, N) :-
спросить_польз( Цель, Трасса, Ответ, N).
спросить_польз( Цель, Трасса, Ответ, N) :-
можно спросить( Цель, ВнешФормат),
формат( Цель, ВнешФормат, Вопрос, [], Перем),
% Получить формат вопроса
спросить( Цель, Вопрос, Перем, Трасса, Ответ, N).
спросить( Цель, Вопрос, Перем, Трасса, Ответ, N) :-
nl,
( Перем = [], !, % Сформулировать вопрос
write( 'Это правда: ');
write( 'Есть (еще) решения для :' )),
write( Вопрос), write( '?'),
принять( Ответ1), !, % Ответ1 - да/нет/почему
обработать( Ответ1, Цель, Вопрос, Перем,
Трасса, Ответ, N).
обработать( почему, Цель, Вопрос, Перем,
Трасса, Ответ, N):-
выд_трассу( Трасса),
спросить( Цель, Вопрос, Перем, Трасса, Ответ, N).
обработать( да, Цель,_, Перем, Трасса, правда, N) :-
след_индекс( Инд),
% Получить новый индекс для 'сказано'
Инд1 is Инд + 1,
( запрос_перем( Перем),
assertz( сказано( Цель, правда, Инд) );
% Запись решения
копия( Цель, Копия), % Копирование цели
ответпольз( Цель, Копия, Трасса, Ответ, Инд1) ).
% Есть еще решения?
обработать( нет, Цель, _, _, _, ложь, N) :-
копия( Цель, Копия),
сказано( Копия, правда, _), !,
% 'нет' означает, больше нет решений
assertz( конец_ответов( Цель) ),
% Отметить конец ответов
fail;
след_индекс( Инд),
% Следующий свободный индекс для 'сказано'
assertz( сказано( Цель, ложь, Инд) ).
% 'нет' означает нет ни одного решения
формат( Пер, Имя, Имя, Перем, [Пер/Имя | Перем]) :-
var( Пер), !.
формат( Атом, Имя, Атом, Перем, Перем) :-
atomic( Атом), !,
atomic( Имя).
формат( Цель, Форм, Вопрос, Перем0, Перем) :-
Цель =.. [Функтор | Apг1],
Форм =.. [Функтор | Форм1],
формвсе( Apг1, Форм1, Арг2, Перем0, Перем),
Вопрос =.. [Функтор | Арг2].
формвсе( [], [], [], Перем, Перем).
формвсе( [X | СпХ], [Ф | СпФ], [В | СпВ], Перем0, Перем) :-
формвсе( СпХ, СпФ, СпВ, Перем0, Перем1),
формат( X, Ф, В, Перем1, Перем).
запрос_перем( []).
запрос_перем( [Переменная/Имя | Переменные]) :-
nl, write( Имя), write( '='),
read( Переменная),
запрос_перем( Переменные).
выд_трассу( []) :-
nl, write( 'Это был ваш вопрос'), nl.
выд_трассу( [Цель по Прав | Трасса] ) :-
nl, write( 'Чтобы проверить по' ),
write( Прав), write( ', что'),
write( Цель),
выд_трассу( Трасса).
конкретный( Терм) :-
нумпер( Терм, 0, 0). % Нет переменных в Терм'е
% конкретизация( Т1, Т2) означает, что Т2 - конкретизация Т1,
% т.е. терм Т1 - более общий, чем Т2, или той же степени
% общности, что и Т2
