Я реализую геометрический доказатель теоремы в Sicstus Prolog;и чтобы решить проблему с возвратом через ввод-вывод, я использую мета-интерпретатор.Это последнее, однако, кажется, не обрабатывает сокращения как ожидалось.
Мой мета-интерпретатор выглядит следующим образом.Первый аргумент solve/5 - это цель, которую нужно оценить, второй и третий аргументы позволяют мне контролировать глубину поиска, а четвертый и пятый аргументы предназначены для обработки возврата по выводу.
solve(true,_,_, O, O) :-
!.
solve(_,CurrentDepth,DepthLimit, _, _) :-
CurrentDepth > DepthLimit,
!,
fail.
solve(nl,_,_, O, [nl|O]):- !.
solve(write(X),_,_, O, [X|O]):- !.
solve((A,B),CurrentDepth,DepthLimit, O0, O2) :-
!,
solve(A,CurrentDepth,DepthLimit, O0, O1),
solve(B,CurrentDepth,DepthLimit, O1, O2).
solve((A;B),CurrentDepth,DepthLimit, O0, O2) :-
!,
(
(solve(A,CurrentDepth,DepthLimit, O0, O2);
solve(B,CurrentDepth,DepthLimit, O0, O2))
).
solve(A,_,_, O, O) :-
(
predicate_property(A, built_in);
predicate_property(A, imported_from(lists))
),
!,
call(A).
solve(Goal,CurrentDepth,DepthLimit, O0, O1) :-
!,
predicate_property(Goal, interpreted),!,
NewDepth is CurrentDepth+1,!,
clause(Goal,SubGoals),
solve(SubGoals,NewDepth,DepthLimit, O0, O1).
Iследовали инструкциям в потоке Реализация програмы трассировки мета-интерпретатора пролог и изменили мета-интерпретатор следующим образом.
solve(true,_,_, O, O) :-
!.
solve(_,CurrentDepth,DepthLimit, _, _) :-
CurrentDepth > DepthLimit,
!,
fail.
solve(nl,_,_, O, [nl|O]):- !.
solve(write(X),_,_, O, [X|O]):- !.
solve(!, _,_,_,_):- !, ( true ; throw(cut)).
solve((A,B),CurrentDepth,DepthLimit, O0, O2) :-
!,
solve(A,CurrentDepth,DepthLimit, O0, O1),
solve(B,CurrentDepth,DepthLimit, O1, O2).
solve((A;B),CurrentDepth,DepthLimit, O0, O2) :-
!,
(
(solve(A,CurrentDepth,DepthLimit, O0, O2);
solve(B,CurrentDepth,DepthLimit, O0, O2))
).
solve(A,_,_, O, O) :-
(
predicate_property(A, built_in);
predicate_property(A, imported_from(lists))
),
!,
call(A).
solve(Goal,CurrentDepth,DepthLimit, O0, O1) :-
!,
predicate_property(Goal, interpreted),!,
NewDepth is CurrentDepth+1,!,
clause(Goal,SubGoals),
catch(
(
solve(SubGoals,NewDepth,DepthLimit, O0, O1)
),
cut,
fail
).
Однако теперь solve/5 не удается для некоторых задач, поставленных в доказательстве теоремы.Стоит отметить, что у меня нет ни одного из предикатов call/1, catch/3 или throw/1 в моей проверке теорем.Пример проблемы заключается в следующем.
:- dynamic test_goal/2.
:- dynamic predicate_with_small_depth/2.
:- dynamic predicate_with_large_depth/2.
:- dynamic p_1/2.
:- dynamic p_2/2.
:- dynamic p_3/2.
:- dynamic p_4/2.
:- dynamic p_5/2.
test_goal(X,Y):-
predicate_with_small_depth(X,Y),!,
predicate_with_large_depth(X,Y).
predicate_with_small_depth(X,Y):-
X < Y,
write('Small Depth Outcome 1'), nl.
predicate_with_small_depth(X,Y):-
X > Y,
write('Small Depth Outcome 2'), nl.
predicate_with_large_depth(X,Y):-
p_1(X,Y).
p_1(X,Y):- p_2(X,Y).
p_2(X,Y):- p_3(X,Y).
p_3(X,Y):- p_4(X,Y).
p_4(X,Y):- p_5(X,Y).
p_5(X,Y):-
predicate_with_small_depth(X,Y),!,
write('Large Depth Outcome: '), write(X), write(' '), write(Y), nl.
Если цель solve(test_goal(1,2),0,8,O1,O2) оценена, ответ Пролога с использованием модифицированного мета-интерпретатора будет:
O2 = [nl,2,' ',1,'Large Depth Outcome: '|_A] ?
но ответ должен быть
O2 = [nl,2,' ',1,'Large Depth Outcome: ',nl,'Small Depth Outcome 1',nl,'Small Depth Outcome 1'|O1] ?
, который был задан моим мета-интерпретатором до добавления адаптации сокращения.
Реализует ли новая реализация мета-интерпретаторавыглядите правильно с точки зрения обработки оператора вырезания?
Большое спасибо.
РЕДАКТИРОВАТЬ
В попытке определить набор проблем и способ решения проблем вкомментарии ниже стали очевидными:
TGTP содержит проблемы, с которыми сталкивается моя программа
Доказательство геометрической теоремы Педро Куарежмы, Days in Logic 2012, Университет Эворы, 6-8 февраля 2012
(работа Гелернтера) лучше всего запечатлел мою программу.
Slies: 27/99
и 28/99
также
Сокращение необходимо для меня, поскольку оно позволяет программе прекратить работу над альтернативными решениями данной цели, как только будет найдено одно решение.Например, если у меня
prove(X):-(p1(X),!);(p2(X),!);p3(X), if p1(X) is satisfiable,
, я не хочу, чтобы были найдены другие решения через p2 / 1 и p3 / 1.Это экономит много вычислений.