%--------------------------------------------------------------%
%   Forward and backward chaining                              %
%   (C) 1998 Zdravko Markov                                    %
%--------------------------------------------------------------%
:- op(900,fx,if).
:- op(890,xfy,then).
:- op(880,xfy,or).
:- op(870,xfy,and).
:- op(860,fx,not).

% Rules

if gives_milk(X) then mammal(X).
if has_feathers(X) and lays_eggs(X) then bird(X).
if has_gills(X) and lays_eggs(X) then fish(X).
if bird(X) and not penguin(X) then flies(X).
if fish(X) then lives(X,sea).
if mammal(X) or fish(X) or bird(X) then homeothermic(X).
if mammal(X) and can_speak(X) then human(X).
if bird(X) and can_speak(X) then parrot(X).

% Facts 

:- dynamic fact/1.

fact(has_feathers(tweety)).
fact(lays_eggs(tweety)).
fact(gives_milk(john)).
fact(can_speak(john)).


% Backward chaining

is_true(P,[fact(P)]) :-
    fact(P), !.
is_true(P,[rule(if Condition then P)|L]) :-
    if Condition then P,
    is_true(Condition,L).
is_true(P and Q,L) :-
    is_true(P,L1),
    is_true(Q,L2),
    append(L1,L2,L).
is_true(P or Q,L) :-
    is_true(P,L);
    is_true(Q,L).
is_true(not P,[not(P)]) :-
    \+ is_true(P,_).
is_true(P,[asked(P)]) :-
    \+ (if _ then P), 
    \+ (P = (_ and _)),
    \+ (P = (_ or _)),
    \+ (P = (not _)),
    write('Is '), write(P), write(' true (y/n): '),
    read(y),
    assertz(fact(P)).


% Forward chaining

derive :-
    derive_fact(P),
    write('Derived: '),
    write(P), nl,
    derive.
derive.

derive_fact(P) :-
    if Condition then P,
    ok(Condition),
    \+ fact(P),
    assertz(fact(P)).

ok(P) :-
    fact(P).
ok(P and Q) :-
    ok(P),
    ok(Q).
ok(P or Q) :-
    ok(P);
    ok(Q).

% ----------------
append([],L,L) :- !.
append([H|T],L,[H|V]) :-
    append(T,L,V).
