# Diagnose false solution

## Description

Bottom-up diagnosis of a false solution

Source: The Art of Prolog

Program source code: diagnose_false_solution.pl

## Listing

```/*
false_solution(A,Clause) :-
If A is a provable false instance, then Clause is
a false clause in the program. Bottom up algorithm.
*/

:-  op( 900, fy, not).

false_solution(A,Clause) :-
solve(A,Proof),
false_clause(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_clause(true,ok).
false_clause(builtin,ok).
false_clause((A,B),Clause) :-
false_clause(A,ClauseA),
check_conjunction(ClauseA,B,Clause).
false_clause((A :- B),Clause) :-
false_clause(B,ClauseB),
check_clause(ClauseB,A,B,Clause).

check_conjunction(ok,B,Clause) :-
false_clause(B,Clause).
check_conjunction((A :- B1),B,(A :- B1)).

check_clause(ok,A,B,Clause) :-
check_clause((A1 :- B1),A,B,(A1 :- B1)).

extract_body(B,B1).

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).
not builtin(Goal),
writeln(['Is the Goal',Goal,'true?']),

writeln([T|Ts]) :- write(T), write(' '), writeln(Ts).
writeln([]) :- nl.

%  Program 17.14   Bottom-up diagnosis of a false solution```