f(a,b,c)  :-  g(a,b) , h(b,c).

and just use SINGLE FACTS!

if(  g(a,b)&h(b,c)  ,  f(a,b,c)).

This would greatly simplify tracing the program run and give you more
control over the facts and implications you manipulate!

-----LOG13.PRO----

less(0,X).
iif( less(X,Y) , less(Y,Z) , less(X,Z)).   %TRANSITIVE RULE
t(less(X,Y)) :- less(X,Y).

t(R) :- if(L,R), t(L).
t(N) :- iif(E,W,N) , t(E), t(W).

less(1,2).
less(2,3).
less(3,4).

---------------------

You might recognize MODUS PONENS

t(R) <- if(L,R) & t(L)

but what is:

t(N) <- iif(E,W,N)  &  t(E)  &  t(W)

This will reduce a fact N(ORTH)
given E(AST) and W(EST) are true!

and (E&W -> N)

------------

This is basically all a prolog rule application does but it might have
several more directions!

================

@ log13.

?- less(1,2).
YES

?- less(1,3).
NO

?- t(less(1,3)).
YES

?- t(less(1,4))
YES

?- t(less(2,4))
YES
-----------------

This is PROLOG using a DOUBLE MODUS PONENS RULE
(instead of it's built in TAIL FOLLOWING SYSTEM directly)

===============

E & W & (E&W)->N
--> N

===============

NEXT WEEK!

MODUS PONENS CONSTRUCTS A PROOF!

proof( R , [R|DED] ) <- if(L,R)  &  proof( L , DED )

less(X,Z) :- less(X,Y), less(Y,Z).

less(1,2).
less(2,3).
less(3,4).

You could just enter TRACE mode.

or 'compile'  the deductions into a list for printing.

t(R)  <-  if(L,R) & t(L).
proof( R , [R|DED] ) <- if(L,R)  &  proof( L , DED )

this would be like putting clause around t(..) or mp(..) to see the
steps taken.

seems there's neater ways to do all these added functions with unify
on atomic predicates.

PROLOG was cut short by only displaying 1 result, then resorting to
LISP coding to show the rest!

mProlog has tabular output of all answers and much of the 3GL add ons
can be done with atomic predicates and recursion.

www.microPROLOG.com

[owns tom X]?

[owns tom       X         ]
[owns tom       house]
[owns tom       car      ]
[owns tom       cat      ]

RULE:     HEAD    ..........   BODY
................less(X,Z)  :-  less(X,Y), less(Y,Z).

clause(  less(X,Z) ,   less(X,Y),less(Y,Z) ).

----------

FORMAL SYSTEM EMULATING RULES (with 1 or 2 tail segments in body)

if(L,R).                     // 1 tail segment  emulated
rule( N , E, W ).      // 2 tail segments emulated

rule( less(X,Z) ,  less(X,Y) ,  less(Y,Z) ).

----------

FORMAL SYSTEM 2 and only 2 RULES

t(R) :- if(L,R), t(L).

t(N) :- if(N,E,W), t(E), t(W)

---------

Now you have full control how the predicates are solved and the trace
is extremely simple.

Herc
--

something like this...

or(1,1).
or(1,0).
or(0,1).
if(1,1).
if(0,1).
if(0,0).
and(1,1).
iff(1,1).
iff(0,0).
xor(1,0).
xor(0,1).

not(or(0,0)).
not(if(1,0)).
not(and(1,0)).
not(and(0,1)).
not(and(0,0)).
not(iff(1,0)).
not(iff(0,1)).
not(xor(1,1)).
not(xor(0,0)).

iif( X      , Y      , or(X,Y)       ).
iif( not(X) , not(Y) , not(or(X,Y))  ).
iif( not(X) , Y      , or(X,Y)       ).
iif( X      , not(Y) , or(X,Y)       ).

iif( X      , Y      , and(X,Y)      ).
iif( not(X) , not(Y) , not(and(X,Y)) ).
iif( not(X) , Y      , not(and(X,Y)) ).
iif( X      , not(Y) , not(and(X,Y)) ).

iif( X      , Y      , if(X,Y)       ).
iif( not(X) , not(Y) , if(X,Y)       ).
iif( not(X) , Y      , if(X,Y)       ).
iif( X      , not(Y) , not(if(X,Y))  ).

iif( X      , Y      , iff(X,Y)      ).
iif( not(X) , not(Y) , iff(X,Y)      ).
iif( not(X) , Y      , not(iff(X,Y)) ).
iif( X      , not(Y) , not(iff(X,Y)) ).

iif( if(A,B) , if(B,C) , if(A,C) ).

if( not(not(X))      , X                  ).
if( not(and(X,Y))    , or(not(X),not(Y))  ).
if( not(or(X,Y))     , and(not(X),not(Y)) ).

t(R) :- if(L,R), t(L).
t(N) :- iif(E,W,N) , t(E), t(W).

proof( R , [R|DED] ) :- if(L,R) , proof( L , DED ).

-------

Then a BINARY TREE MODUS PONENS CONSTRUCTION
with E&W->N
instead of the simple MODUS PONENS  L->R
proof method above...

should solve all mathematics!  If you don't mind exponential time
delays!