On May 5, 10:57 am, fom <fomJ...@nyms.net> wrote: > On 5/4/2013 7:30 PM, Graham Cooper wrote: > > > > > That Paradigm is not even used with a valid set theory > > I am rather unconcerned with the > pretend mathematics that occurs in > computation where thousands of real > mathematical results are involved > prior to the compilation of a "hello > world" program. > > I wish I knew more about prolog in order > to counter your statements appropriately. > > But, I do not. > > I am curious, however, about the notion > of "valid set theory". >
Starting with MODUS PONENS you come across the need to MATCH 1 predicate from the LHS (or RHS) of an inference rule to existing theorems.
This is the algorithm UNIFY( f1(a,b,c) , f2(c,d,e) ) => TRUE/FALSE
From here you gain HORN CLAUSES
p(a,b,c,d) p(a,b,c,d) <- CLAUSE & CLAUSE & CLAUSE
where the TAIL predicates are recursively matched also down to a raw base fact (theorem) with no CLAUSES.
It is widely believed that HORN CLAUSES can only perform a subset of LOGIC due to finite negation by exhaustion, (no NOT).
a raw PROLOG INTERPRETER contains nothing more than the UNIFY algorithm.
WHY PROLOG WILL DICTATE THE FUTURE OF LOGIC THEORY JAN 1 Graham Cooper