Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Smart Computer Trace
5 views
Skip to first unread message
Graham Cooper
May 16, 2013, 12:10:32 AM5/16/13
to
TRACE
nat [ s X ]?
TRY 1
nat [ s X ]
TAIL 1
nat X
TRY 1
nat 0
STACK: 1 - X - 22 -
STACK: 2 - - 22 - X1
STACK: 3 - X1 - 2 -
STACK: 4 - - 2 - 0
X:=0
----------
The trace is quite effective in color, but I'm
still working on the Recursion Stack..
Herc
--
www.BLoCKPROLOG.com
AMiews
May 16, 2013, 8:45:41 AM5/16/13
to
"Graham Cooper" <graham...@gmail.com> wrote in message
news:f00bc128-c510-4734...@fq2g2000pbb.googlegroups.com...
Graham Cooper
May 16, 2013, 5:04:03 PM5/16/13
to
On May 16, 10:45 pm, "AMiews" <inva...@invalid.com> wrote:
> "Graham Cooper" <grahamcoop...@gmail.com> wrote in message
In FORTH - Reverse Polish Notation
Peano's number 4 would be
0 s s s s !
MetaMath uses R.P.N to verify all it's proofs, because every predicate
that is relied upon in the theorem has to be stated earlier in the
string.
It's an equivalent system to Horn Clauses / PROLOG.
-------------
HORN CLAUSE
a <- b & c
d <- e & f
(a & d) ?
---------------
RPN
(b , c , & ) , ( e , f , & ) &
---------------
Herc
--
www.BLoCKPROLOG.com
> "Graham Cooper" <grahamcoop...@gmail.com> wrote in message
Peano's number 4 would be
0 s s s s !
MetaMath uses R.P.N to verify all it's proofs, because every predicate
that is relied upon in the theorem has to be stated earlier in the
string.
It's an equivalent system to Horn Clauses / PROLOG.
-------------
HORN CLAUSE
a <- b & c
d <- e & f
(a & d) ?
---------------
RPN
(b , c , & ) , ( e , f , & ) &
---------------
Herc
--
www.BLoCKPROLOG.com
0 new messages