Невероятно, есть частичное решение этой проблемы here. Чтобы воспроизвести соответствующую часть здесь, это существенный код, поэтому позвольте мне пояснить, что это не моя собственная работа, я просто включаю здесь работу здесь, если в будущем веб-сайт пропадет без вести.
Во-первых, вам нужно мета-круговой переводчик:
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])]
Увы, это не работает вне я думаю, что с некоторым изучением вы могли бы найти способ применить эту технику к ней и придумать что-нибудь. Например, вы можете создать мета-интерпретатор, который принимает список фактов, чтобы проверять и выполнять один и тот же тип цикла delete-one-then-proof, чтобы найти их.
Надеюсь, что это поможет и, по крайней мере, интересно.
Без дополнительной информации трудно дать какой-либо намек. Какой Пролог? Metainterpreter структура? – CapelliC
Я проделал пролог долгое время, но я не уверен, что здесь будет полезно использовать покрытие кода, поскольку факт может быть оценен в сочетании со многими другими, чтобы попытаться достичь цели, прежде чем она будет позже «отброшена». Возможно, вам нужно что-то, что бы устранить факт, а затем посмотреть, может ли цель все еще быть удовлетворена; Кажется, немного интенсивнее. –
Я уверен, что я помню функцию «trace», которая рассказывает вам, как факты использовались в цели. Возможно, если ваша версия пролога поддерживает эту функцию, вы можете проанализировать этот вывод (простить каламбур), чтобы достичь своей цели. –