令人难以置信的是，这里有这个问题的部分解决方案。在这里复制相关部分是大量代码，所以让我澄清一下，这不是我自己的工作，我只是把工作包括在这里，以防上面的网站将来丢失。
首先，您需要一个元循环解释器：
mi_circ(true).
mi_circ((A,B)) :-
mi_circ(A),
mi_circ(B).
mi_circ(clause(A,B)) :-
clause(A,B).
mi_circ(A \= B) :-
A \= B.
mi_circ(G) :-
G \= true,
G \= (_,_),
G \= (_\=_),
G \= clause(_,_),
clause(G, Body),
mi_circ(Body).
这适用于\=/2和clause/2。要将这种模式推广到所有内置谓词，我们可以使用 predicate_property/2 来识别它们，以便直接调用它们：
provable(true, _) :- !.
provable((G1,G2), Defs) :- !,
provable(G1, Defs),
provable(G2, Defs).
provable(BI, _) :-
predicate_property(BI, built_in),
!,
call(BI).
provable(Goal, Defs) :-
member(Def, Defs),
copy_term(Def, Goal-Body),
provable(Body, Defs).
这为您提供了一个具体的元解释器，这意味着您可以传递provable/2一个目标和一组定义，它会告诉您提供的定义是否足以证明目标。我敢打赌，你现在可以尝到我们离最终解决方案有多近了！
通过以下附加定义，我们可以使用此 MI 来识别某些谓词定义中的冗余事实：
redundant(Functor/Arity, Reds) :-
functor(Term, Functor, Arity),
findall(Term-Body, clause(Term, Body), Defs),
setof(Red, Defs^redundant_(Defs, Red), Reds).
redundant_(Defs, Fact) :-
select(Fact-true, Defs, Rest),
once(provable(Fact, Rest)).
这select/3用于一次分割一个定义，并查看谓词是否仍然可证明。通过在所有定义中执行此操作，您可以获得所有不必要的规则集。
给定定义：
as([]).
as([a]). % redundant
as([a,a]). % redundant
as([A|As]) :-
A = a, % test built-in =/2
5 is 2 + 3, % test built-in is/2
1 > 0, % test built-in >/2
as(As).
我们可以要求可以从所有（相应的）剩余条款中推导出来的事实，因此是多余的：
?- redundant(as/1, Reds).
Reds = [as([a]), as([a, a])]
唉，这在您的问题上不是开箱即用的，但我确实认为通过一些研究，您可以找到一种方法将这种技术应用于它并想出一些东西。例如，您可以创建一个元解释器，它接受一个事实列表来检查并执行相同类型的 remove-one-then-prove 循环来找到它们。
希望这会有所帮助，并且至少很有趣。