Пытаюсь сделать что-то типа локальных баз данных с возможностью доказательства только в рамках утверждённого в них и импортированного в них.
Породил следующее:

member2(X, _, [Y|_]) :- copy_term(Y, Z), Z = X.
member2(_, X, [Y|_]) :- copy_term(Y, Z), Z = X.
member2(X, Y, [_|T]) :-
    member2(X, Y, T).

prove((Goal1, Goal2), Db) :-
    prove(Goal1, Db),
    prove(Goal2, Db).
    
    
prove(Goal, db(Clauses, Imports)) :-
    member2(Goal, (Goal :- Procedure), Clauses),
    (\+ var(Procedure) 
    -> 
        prove(Procedure, db(Clauses, Imports))
    ;
        true 
    ).
    
prove(Goal, db(_, Imports)) :-
    functor(Goal, F, A),
    member(F/A, Imports),
    call(Goal).
    
    
mdb(db([ 
    fact(0, 1),
    (fact(N, R) :- N1 is N - 1, fact(N1, R1), R is N * R1)
], [is/2])).

Проблема заключается в работе с рекурсивными правилами, ибо при унификации головы правила (второе правило предиката prove/2) переменные из базы инстанцируются внекоторые значения и последующие инстантинации проваливаются. Например, если я вызываю fact(2, N), то голова правила fact(N, R) :- ... принимает вид fact(2, R), и при рекурсивном вызове fact(1, R) унификация не срабатывает.

Пока проблему решил, что называется, "в лоб" — при поиске в базе данных создаю копии через copy_term/2 и пытаюсь унифицироваться с ними (см member2). Работает, но меня этот метод коробит, ибо копии создаются для каждой унификации, даже если она окажется неудачной. Понятно, что все лишние термы выбарсываются и будут удалены сборщиком мусора. Однако это лишняя нагрузка на систему.

Есть идеи, как решить проблему с "порчей" переменных в БД без такого брутального копирования?
Заранее спасибо.