====== Diagnose false solution top-down ======
{{tag>diagnostic_systems}}
===== Description =====
Top-down diagnosis of a false solution

**Source**:  The Art of Prolog
===== Download =====
Program source code: {{diagnose_false_solution_top-down.pl}}
===== Listing =====
<code prolog>
/* 
   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
</code>
===== Comments =====