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

But it can be used to build a meta interpreter:

   solve(true) :- !.
   solve((A,B)) :- !, solve(A), solve(B).
   solve(H) :- clause(H,B), solve(B).

And from this also debuggers etc.. can be built. Including
solvers that return a kind of proof tree as your proof/2
suggests. And much more.

But it wont be very efficient since a call to clause/2 is
usually slower than a native clause invokation, although
clause/2 might also offer multi-argument indexing. Here is
a little test whether it has multi-argument indexing:

    :- dynamic r/2.

    r(a, b).
    r(a, c).
    r(d, c).
    r(d, e).

In SWI-Prolog (6.3.4) and Jekejeke Prolog (0.9.6) we have:

    ?- clause(r(X, c),true).
    X = a ;
    X = d
    ?-

So it detects determinism, since after showing the solution
X = d it directly returns to the top level as it didn't find
more choice points. In GNU Prolog (1.4.1) on the other hand
we have:

    ?- clause(r(X,c),true).
    X = a ? ;
    X = d ? ;
    no
    ?- (X=a;X=d).
    X = a ? ;
    X = d
    yes

With multi-argument indexing in clause/2 determinism can also
transpire through the last rule of solve/1 and make solve/1
behave as the original program concerning determinism.

The clause/2 system predicate is for example documented here:

    http://www.swi-prolog.org/pldoc/man?predicate=clause%2F2

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!