# Diagnose false solution top-down

## Description

Top-down diagnosis of a false solution

Source: The Art of Prolog

## Listing

```/*
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).