Как я могу запомнить термины на дереве в Прологе?
Я думал, что мои рассуждения в порядке, но такие узлы, как коммутация, продолжают добавлять новые узлы с тем же предыдущим значением, программа работает, но я бы хотел остановить создание этих узлов.
name(Term,X) :- Term=..[X|_].
prop(eq,commutative).
prop(and,commutative).
prop(and,associative).
prop(Op,P):-compound(Op),name(Op,Opname),prop(Opname,P).
identity(A,A). %checks if both are the same, or returns the same in any parameter
commute(A,B):- A=..[N,X,Y], B=..[N,Y,X]. %true if B is commutation of A, or B outputs commutation of A
associate(X,Y):- X=..[N,A,B],B=..[N,BA,BB], Y=..[N,C,BB],C=..[N,A,BA].
:- dynamic proofcache/1.
proof(_,Steps) :- Steps<1, !, false.
proof(eq(A,B),Steps) :- identity(A,B),writeln(["id",A,"=",B,Steps]),!,true.
proof(eq(A,B),Steps) :- prop(A,commutative), (proofcache(eq(A,B));asserta(proofcache(eq(A,B))), commute(A,R),writeln(["comm",A,"=",R,Steps]), proof(eq(R,B),Steps-1)).
proof(eq(A,B),Steps) :- prop(A,associative), (proofcache(eq(A,B));asserta(proofcache(eq(A,B))), associate(A,R),writeln(["assoc",A,"=",R,Steps]), proof(eq(R,B),Steps-1)).
пример запроса:
proof( eq( and(t,and(t,f)), and(and(t,t),f) ) ,6).