==LHS=============RHS
if( and(lt(X,Y),lt(Y,Z)) , lt(X,Z) ).

LOG4.PRO uses MODUS PONENS on the above inference rule!

MP
t(RHS) <- if(LHS,RHS) ^ t(LHS).

--------------------------------
TEST RUN!

   lt(2,5).
   lt(5,10).        (ADD SOME FACTS ABOUT 2<5, 5<10)

   ?- lt(2,X).
   X = 5            (PROLOG MISSED THE INFERENCE RULE)

   ?- t(lt(2,X)).   (TRY AGAIN!)
   X = 5
   X = 10

This is the format to Query and include further inferences.

.
.

- - - - - - - - - - - -MODUS PONENS
(2<5) ^ (5<10) ---------------------------> (2<10)
- - - - - - - - - - - -INFERENCE RULE

.
.
.
.
.
Herc

----LOG4.PRO-----
f(0).
t(1).
t(X) :- f(f(X)).
wff(X) :- t(X).
wff(X) :- f(X).
what(X,true) :- t(X).
what(X,false) :- f(X).

t(if(X,Y)) :- t(X), t(Y).
t(if(X,Y)) :- f(X), f(Y).
t(if(X,Y)) :- f(X), t(Y).
t(or(X,Y)) :- t(X).
t(or(X,Y)) :- t(Y).
t(and(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- t(X),t(Y).
t(iff(X,Y)) :- f(X),f(Y).
t(xor(X,Y)) :- t(X),f(Y).
t(xor(X,Y)) :- f(X),t(Y).

f(if(X,Y)) :- t(X),f(Y).
f(or(X,Y)) :- f(X),f(Y).
f(and(X,Y)) :- f(X).
f(and(X,Y)) :- f(Y).
f(iff(X,Y)) :- t(X),f(Y).
f(iff(X,Y)) :- f(X),t(Y).
f(xor(X,Y)) :- t(X),t(Y).
f(xor(X,Y)) :- f(X),f(Y).

t(lt(A,B)) :- lt(A,B).

if( and(lt(X,Y),lt(Y,Z)) , lt(X,Z) ).  .... INFERENCE RULE