define_operators:-
op( 920, xfy, and),
op( 930, xfy, or),
op( 940, xfx, cf),
op( 950, xfx, then),
op( 960, fx, if),
op( 970, xfx, ':').
?- define_operators.
solve( P1 and P2, Trace, Proof1 and Proof2) :-
solve( P1, Trace, Proof1),
solve( P2, Trace, Proof2).
solve( P1 or P2, Trace, Proof) :-
solve( P1, Trace, Proof).
solve( P1 or P2, Trace, Proof) :-
solve( P2, Trace, Proof).
solve( not P, Trace, failed( P)) :-
not solve( P, Trace, _).
solve( P, Trace, Fact: P ) :- Fact : P.
solve( P, Trace, R: if Proof then P) :-
R: if P0 then P,
solve( P0, [R | Trace], Proof).
solve( P, Trace, told( P) ) :-
told( P, yes).
solve( P, Trace, told( P) ) :-
askable( P), not told( P, _),
ask( P, Trace).
ask( P, Trace) :-
nl, write( P), write( ' ? '),
read( A), respond( P, A, Trace).
respond( P, yes, Trace) :-
assert( told( P, yes)), !.
respond( P, no, Trace) :-
assert( told( P, no)), !, fail.
respond( P, why, []):-
!, nl, write( ' you ask too many questions'),
ask( P, []).
respond( P, why, [H]) :- !,
nl, write( H), write(' is my hypothesis'),
ask( P, []).
respond( P, why, [R | Trace]) :- !,
R : if G1 then G,
nl, write(' trying to apply the rule'),
show_rule( R: if G1 then G),
nl, write( 'to prove the conclusion '),
write( G),
ask( P, Trace).
respond( P, _, Trace) :-
write(' valid answers are: yes, no, why'),
ask( P, Trace).
show_rule( R: if P0 then P) :-
nl, write( R ), write( ' :'),
nl, write( ' if '), write( P0 ),
nl, write( ' then '), write( P ).
how1( G, Fact: G) :- !,
nl, write( G),
write( ' is a fact '),
write( Fact).
how1( G, told( G) ) :- !,
nl, write( G),
write( ' was told me').
how1( not G, failed( G) ) :- !,
nl, write( not G),
write( ' proved by failure of '),
write( G).
how1( G, R: if _ then G) :- !,
nl, write( G),
write( ' was proved by using the rule: '),
R: if P then G,
show_rule( R: if P then G).
how1( G, R: if Proof then _) :-
how( G, Proof).
how1( G, Proof1 and Proof2) :-
how( G, Proof1) ; how( G, Proof2).
how( G, Proof) :- how1( G, Proof), !.
how( G, _) :- nl, write( G), write( ' was not proved').
explain( Proof) :-
nl, nl, write( 'explanation ? [goal/no]: '), read( G),
( G \= no -> how( G, Proof), explain( Proof) ),
!.
backtrack :-
nl, nl,
write( 'further solutions ? : '),
read( no).
init :-
retractall( told( _, _)).
shell :-
init,
goal( G),
solve( G, [G], Proof),
nl, nl,
write( 'solution: '),
write( G),
explain( Proof),
backtrack.
Back to example 11.1
r1 :
if material_verbrennt
then temperatur( zu_hoch).
r2 :
if temperatur( zu_hoch)
or temperatur( zu_niedrig)
then temperatur( falsch).
r3 :
if temperatur( falsch)
and thermostat( richtig_eingestellt)
then thermostat( defekt).
r4 :
if temperatur( falsch)
and not thermostat( richtig_eingestellt)
then thermostat( richtig_einstellen).
r5_1 :
if kein_dampf
then temperatur( zu_niedrig).
r5_2 :
if kein_dampf
then dampfsystem_problem.
r6_1 :
if dampfsystem_problem
then kein_wasser.
r6_2 : if dampfsystem_problem
then duese_verstopft.
r7 :
if buegelwirkung_schlecht
then temperatur( zu_niedrig).
r8 :
if buegeleisen_kalt
and lampe_leuchtet
then warten.
r9 :
if buegeleisen_kalt
and not lampe_leuchtet
then kein_strom.
s1 :
symptom( material_verbrennt).
s2 :
symptom( kein_dampf).
s3 :
symptom( buegelwirkung_schlecht).
s4 :
symptom( buegeleisen_kalt).
s5 :
symptom( lampe_leuchtet).
s6 :
symptom( thermostat( richtig_eingestellt)).
d1 :
diagnosis( thermostat( defekt)).
d2 :
diagnosis( thermostat( richtig_einstellen)).
d3 :
diagnosis( kein_wasser).
d4 :
diagnosis( duese_verstopft).
d5 :
diagnosis( kein_strom).
d6 :
diagnosis( warten).
diagnose :- shell.
askable( P) :- symptom( P).
goal( G) :- diagnosis( G).
Back to example 11.2