この証明を思い出してください。
solve(true, true).
solve([], []).
solve([A|B],[ProofA|ProofB]) :-
solve(A,ProofA),
solve(B, ProofB).
solve(A, node(A,Proof)) :-
rule(A,B),
solve(B,Proof).
次のように、インタープリターの 3 番目の規則が変更され、インタープリターの他の規則は変更されていないとします。
% Signature: solve(Exp, Proof)/2 solve(true, true).
solve([], []).
solve([A|B], [ProofA|ProofB]) :-
solve(B, ProofB), %3
solve(A, ProofA).
solve(A, node(A, Proof)) :-
rule(A, B),
solve(B, Proof).
両方のバージョンのクエリに対して作成されるプルーフ ツリーを考えてみましょう。変数の置換は、1 つのバージョンだけで実現できますか? 説明。一番左の無限枝の向こう側に本葉が移動することはありますか? 説明。両方の質問で、答えが肯定的である場合の例を挙げてください。これは証明にどのように影響しますか？
私を助けてください ！TX