Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Replies: 2   Last Post: Nov 19, 2012 6:34 PM

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
Posted: Nov 19, 2012 6:34 PM

On Nov 19, 9:55 pm, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
> Graham Cooper <grahamcoop...@gmail.com> writes:
> > On Nov 19, 9:30 am, Alan Smaill <sma...@SPAMinf.ed.ac.uk> wrote:
> >> Graham Cooper <grahamcoop...@gmail.com> writes:
> >> > Imagine if you could cut down on all the PROLOG RULES
>
> >> > 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!

>
> >> ever heard of clause/2  from the Prolog standard?
>
> > It looks like it traces the subgoals being invoked.
>
> No, it doesn't;
> it gives what you were talking about,
> a unit clause corresponding to each normal Prolog program clause.
>

but it still uses the UNIFY process to resolve the body/tail.

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

Herc

Date Subject Author
11/19/12 Alan Smaill
11/19/12 Graham Cooper