/* 
    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) :-
		query_goal(A,Answer),
		check_answer(Answer,A,B,Clause).
	check_clause((A1 :- B1),A,B,(A1 :- B1)).

	check_answer(true,A,B,ok).
	check_answer(false,A,B,(A :- 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).
	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.14   Bottom-up diagnosis of a false solution