我正在 Sicstus Prolog 中实现几何定理证明器；为了克服 I/O 回溯的问题，我使用了元解释器。然而，最后一个似乎并没有像预期的那样处理削减。
我的元解释器如下所示。第一个参数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).
我已按照线程在跟踪元解释器序言中实现剪切中的说明，并将元解释器 更改为以下内容。
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)被评估，Prolog 使用修改后的元解释器的答案是：
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包含我的程序解决的那种问题
Pedro Quaresma 的几何定理证明，Days in Logic 2012，埃武拉大学，2012 年 2 月 6 日至 8 日
（Gelernter 的作品）最好地捕捉我的程序。
谎言：27/99
和 28/99
还
削减对我来说是必要的，因为它允许程序在找到一个解决方案后停止处理给定目标的替代解决方案。例如，如果我有
prove(X):-(p1(X),!);(p2(X),!);p3(X), if p1(X) is satisfiable,
我不希望通过 p2/1 和 p3/1 找到其他解决方案。这节省了大量的计算量。