WHY PROLOG WILL DICTATE THE FUTURE OF LOGIC THEORY

[Graham Cooper]

It's an ALGORITHMIC APPROACH not a mathematical one

UNIFY( f(X,g) f(a,B) )
= f(a,g)

This is the CORE of the PROLOG ENGINE and not only does it

[o] MATCH arguments of inference rules in theories
[o] it's fully computational in itself
[o] works as a 3GL fetch cycle
[o] does recursion
[o] SEARCHES for functions that best solve the problem
[o] then applies them trial and error style.

By REVERSE ENGINEERING theorem provers from UNIFY(f1,f2)
we now know that

CONJUNCTIVE CLAUSES
DISJUNCITVE CLAUSES

are _not_ the base representation of logic theorems.

{ p1(..) p2(..) p3(..) ... pn(...) } -> head(...)

This is the BASE STRUCTURE for UNIFY ALGORITHM
that performs BACKWARD CHAINING TO AXIOMS
from the HEAD to the TAIL that implies the HEAD
and recursively to each segment of the TAIL.

Herc
--
A LOGIC INFERENCE RULE IN PROLOG
if( if(S,not(R)) , if(R,not(S)) ).
if it's sunny then it's not raining