/*              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

think :-
       write_database,
       nl,
       write('Reasoning..........................'), nl,
       apply_rule,
       think1.
think1:-
      apply_rule,nl,
      think1.
think1:-
       nl,
       write('DATABASE:'),nl,
       write_database.

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.

clear:-
       retract(db(_)),
       fail.
clear.

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(6, [and(X,_)],               [X],      [],       ['Simplification-1', 'Simp1']).
rule(7, [and(_,Y)],               [Y],      [],       ['Simplification-2', 'Simp2']).

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']).

rule(100,[a(X,Y), a(Y,Z)],         [a(X,Z)],              [],  ['Barbara', 'Bar']).
rule(101,[a(X,Y), i(Y,Z)],         [i(X,Z)],              [],  ['Darii', 'Dar']).
rule(102,[a(X,Y), e(Y,Z)],         [e(X,Z)],              [],  ['Celarent','Cel']).
rule(103,[e(X,Y), i(Y,Z)],         [o(X,Z)],              [],  ['Ferio', 'Fer']).

rule(110,[i(X,Y)],                 [i(Y,X)],              [],  ['Conversion-I', 'Con']).
rule(111,[e(X,Y)],                 [e(Y,X)],              [],  ['Conversion-E', 'Con']).

rule(120,[a(X,Y)],                 [i(X,Y)],              [],  ['Existential-implication/A', 'Exist-imp-A']).


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:'),nl,
             write(Z2),nl,
             write('BY THE RULE:'),
             write(N),
             write('. '),
             write(Name1),
             nl,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,and(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.