/* false_solution(A,Clause) :- If A is a provable false instance, then Clause is a false clause in the program. Top down algorithm. */ :- op( 900, fy, not). false_solution(A,Clause) :- solve(A,Proof), false_goal(Proof,Clause). solve(true,true) :- !. solve((A,B),(ProofA,ProofB)) :- !, solve(A,ProofA), solve(B,ProofB). solve(A,(A:-builtin)) :- builtin(A), !, A. solve(A,(A:-Proof)) :- clause(A,B), solve(B,Proof). false_goal((A :- B),Clause) :- false_conjunction(B,Clause), !. false_goal((A :- B),(A :- B1)) :- extract_body(B,B1). false_conjunction(((A :- B),Bs),Clause) :- query_goal(A,false), !, false_goal((A :- B),Clause). false_conjunction((A :- B),Clause) :- query_goal(A,false), !, false_goal((A :- B),Clause). false_conjunction((A,As),Clause) :- false_conjunction(As,Clause). extract_body(true,true). extract_body((A :- B),A). extract_body(((A :- B),Bs),(A,As)) :- extract_body(Bs,As). query_goal(A,true) :- builtin(A). query_goal(Goal,Answer) :- not builtin(Goal), writeln(['Is the Goal',Goal,'true?']), read(Answer). writeln([T|Ts]) :- write(T), write(' '), writeln(Ts). writeln([]) :- nl. % Program 17.15: Top-down diagnosis of a false solution