/*              Patched up to work decently for PHI 519   Sept 17 2003,
                Modified for UB  Feb 2001.
                Minor changes to f-infer1.pro.
                3/20  This version of f-infer.pro
                includes a provision for halting reasoning
                after each screen.                          */
dynamic:-  db/1.                %Required for SWI Prolog
clear:-
       retractall(db(X)).

think :-
       write_database,
       nl,
       write('Reasoning..........................'), nl,
       apply_rule.
write_database :-
       db(X),
       write(X),nl,
       fail.
write_database :-
       db(neg(X)),
       db(X),
       write('Contradictions in database:  '),
       writet(neg(X)),
       write('      '), writet(X), nl, fail.
write_database.

rule(1, [if(X,Y),X],               [Y],      [],       ['Modus ponens', 'MP']).
rule(2, [or(X,Y), neg(X)],         [Y],      [],       ['Disjunctive syllogism','DS']).
rule(3, [or(X,Y), neg(Y)],         [X],      [],       ['Disjunctive syllogism','DS']).
rule(4, [if(X,Y), neg(Y)],         [neg(X)], [],       ['Modus tollens', 'MT']).
rule(5, [if(X,Y), if(Y,Z)],        [if(X,Z)],[],       ['Hypothetical syllogism', 'HS']).

rule(50, [neg(and(X,Y))],          [or(neg(X), neg(Y))], [],   ['DeMorgan Laws', 'DM']).
rule(51, [neg(or(X,Y))],           [and(neg(X), neg(Y))], [],  ['DeMorgan Laws', 'DM']).
rule(52, [and(neg(X),neg(Y))],     [neg(or(X,Y))],        [],  ['DeMorgan Laws', 'DM']).
rule(53, [or(neg(X),neg(Y))],      [neg(and(X,Y))],       [],  ['DeMorgan Laws', 'DM']).


apply_rule:-
      rule(N,[Z1,Z2], [Z3],[],[Name1,Name2]),
      db(Z1),
      db(Z2),
      db_absent(Z3),
      assertz(db(Z3)),
             write('INFERRING:'),nl,
             write(Z3),nl,
             write('FROM'),nl,
             write(Z1),nl,
             write('AND FROM:'),nl,
             write(Z2),nl,
             write('BY THE RULE:  '),
             write(N),
             write('. '),
             write(Name1),
             nl.
apply_rule:-
      rule(N,[Z1], [Z3],[],[Name1,Name2]),
      db(Z1),
      db_absent(Z3),
      assertz(db(Z3)),
             write('INFERRING:'),nl,
             write(Z3),nl,
             write('FROM:'),nl,
             write(Z1),nl,
             write('BY THE RULE:  '),
             write(N),
             write('. '),
             write(Name1),
             nl.

       
db_absent(X):-
      db(X),
      !,fail.
db_absent(_):- true.
                  

/* Samples beginning database                */
db1 :-
   assertz(db(and(a,b))),

   assertz(db(if(a,c))),
   assertz(db(if(c,d))),
   assertz(db(if(or(g,h),d))),
   assertz(db(or(neg(j),neg(l)))),
   assertz(db(if(u,or(j,l)))),
   write('Test database #1 installed.'),nl.

db2 :-
   assertz(db(tall(tom))),
   assertz(db(if(tall(X),big(X)))),
   assertz(db(or(small(X),big(X)))),
   assertz(db(neg(big(susan)))),
   assertz(db(if(big(X), has_expensive_clothes(X)))),
   write('Test database #2 installed.'), nl.

db3:-
   assertz(db(if('Sam the butler is guilty',
              'Sam the butler had a motive'))),
   assertz(db(if('Sam and Marilyn were the only 2 in the house',
              or('Sam the butler is guilty',
                 'Marilyn the maid is guilty')))),
   assertz(db(or('Sam was in Mr. Smithers will',
              neg('Sam the butler had a motive')))),
   assertz(db(neg('Sam was in Mr. Smithers will'))),
   assertz(db('Sam and Marilyn were the only 2 in the house')),

    write('Database #3 installed.'),nl.