----- Original Message -----
From: <phimvt@...>
To: <concatenative@yahoogroups.com>
Sent: Tuesday, June 17, 2003 4:28 AM
Subject: Re: [stack] resolution theorem prover

>
> On Fri, 6 Jun 2003, stevan apter wrote:
>
> > i've written a little k resolution theorem prover (for the
> > propositional calculus only):
> >
> > http://www.nsl.com/k/resolve.k
>
> That is most impressive. And all in just a few lines of K !
> Well done, and thanks for sharing.

thanks manfred.

http://www.nsl.com/k/resolve2.k is a resolution theorem prover
for the the predicate calculus. my first implementation of
unification used the standard (?) algorithm found in nilsson,
but i prefer my second pass, based on martelli and montanari.
oddly enough, the code for 'prove' is shorter than that for
the propositional calculus version.

i made a start at a connection-graph-based prover (kowalski)
(http://www.nsl.com/k/connect.k), but there's some work to do
on that. unfortunately, kowalski's book (logic for problem-
solving, which is also online at his site) gives an abbreviated
version of his proof-procedure, and the ACM insists on charging
for the paper where he gives the full version with factoring,
which is what i'd like to implement. i think this could be
done in a very few lines of code.

i didn't have time to implement the machinery to translate
from standard to clause form, but i like kowalski's notation:
(p v ... v p) <- (q & ... & q). intuitive and elegant.

i hope to have cK versions available at some point.

>
> I have only written the obvious truth table programs and then
> many versions of semantic tableaux (= truth trees). The other
> two possibilities, connection graphs and resolution I have
> never done. That was because they require a front end to
> translate the usual infix/prefix/postfix form into the normal
> form required: negation normal form for connection graphs,
> and conjunctive normal form for resolution. But the translation
> is just about as runtime extensive as determining whether
> the formula is a tautology. So for the propositional case,
> where the translated normal form is then only used once, it
> does not seem worth it. The matter is entirely different
> for predicate logic.

i've been meaning to study this code. i don't think i've
used backtracking in anything i've written.

>
> You might want to look at my other web page, Symbolic Processing
> in Pascal, where I have a monadic logic semantic tableaux prover
> and a polyadic logic database system (not a theorem prover).

logic databases are interesting. given a formula with free variables,
you instantiate all/some of the sentences implied by the database?
i'll take a look. have you thought about implementing this in joy?

>
> I'll use this opportunity to ask some questions about K and cK.
>
> About K:
> Is it compiled or interpreted?

interpreted. scalar operations are 10-20 times slower than c.
vector operations are faster (i know, i know - it's a paradox.)
no garbage collection - k uses reference counting.

when k encounters a function, e.g. {x+y-z}, it compiles it into
word-code. so during run-time, there's no tokenizing/parsing
overhead. i guess this is pretty standard for modern interpreters.

> What source language is the processor written in?

most of it is written in c, although some parts are written in k.

> (if they only distribute the executable, then you might not know)
>
> About cK, your concatenative version of K:
> How have you implemented it?
> As a collection of library routines written in K ?
> As a compiler, translating from cK to K
> As an interpreter which runs K and interprets cK ?

i don't think my approach differs much from john's in scheme, except
that i parse input strings in joy notation. for each joy primitive,
there is a corresponding k function. for example, 'pop' is a k
function which takes a stack and returns a stack without its first
element. so the thing which gets evaluated is a list, some of whose
elements (i.e. those corresponding to operations/combinators) are
functions, and the rest are data (strings, symbols, ints, floats,
lists). the evaluation function is pretty simple: take the stack
so far and the next element in the list to be evaluated; if it's
data, append it to the stack, else (it's a function, so) apply it
to the stack; in both cases, return the new stack. the evaluation
function is wrapped in code to do tracing, timing, stopping, continuation
collection, &c., which is where the cruft appears. otherwise it
would just be:

e:{x a/y} / apply a progressively to stack x, list y
a:{:[7=4:y;y x;x,,y]} / if y is a function, apply it to x, else append it to x

if you look at the ck script (http://www.nsl.com/k/ck.k) you'll see
major sections:

// Wrappers this the code which takes the stack and maps all
or part of it to the ck operators, takes the result
of applying the operator and puts it together with
the stack. e.g. + takes 2 elements and returns 1.

// K optimization
this code figures out when we can dodge special
ck processing and proceed directly to k. strictly
for performance, to match k on simple operations.

// Errors functions to signal different kinds of errors.

// Stack split/fuse

could have been integrated into binrec, the only
place where it's used.

// Assignment handles set, def, and script execution. ck doesn't
support "name == prog". instead, definitions are
created e.g. [2 +] `add2 def (take an element from
stack, side-effect is assign a name to it, leave the
name on the stack. ck doesn't have joy-style modules/
libraries. instead you say "script.ck" run, or
invoke the script(s) on the command line.

// lambda, shuffle

code for lambda sugar and billy's shuffle operator.

// K list of K operations, wrapped in stack handlers.

// Joy for each non-symbolic joy primitive, a k function.
for example, 'i' is s1[{[s;p]E[s;p]}], where s1
is the stack wrapper which takes the stack and
breaks it into two pieces, s, the stack minus the last
element, and p, the last element, then passes those
two pieces to some function which returns a new stack.
in this case, the function evaluates p on s, i.e.
E[s;p]. compare with john's scheme implementation -
i think they're more similar than different.

// Tokenize the tokenizer. more code than i would like, but
joy notation is so elegant it's worth preserving.
the only noteworthy thing to say about this code is
that it's free of explicit loops or recursion. it
makes extensive use of k's pattern-matching string
search and replace primitive _ssr. i wasn't sure
this could be done without a lexer of some kind, but
it seems to work ok. e.g. "[10 [2] [i]]" -> ("10";
,,"2";,,"i").

// Type given a list of tokens (i.e. strings) replace each
string with the appropriate value, e.g. ("10";,,"2";
,,"i") -> (10;,2;,s1[{[s;p]E[s;p]}]).

// Display take a k list (i.e. the stack) and display it in
joy notation. e.g. (10;,2;,s1[{[s;p]E[s;p]}]) ->
"[10 [2] [i]]"

// Evaluation evaluate, trace, time, stop, continuations

>
> I have another question about adverbs in K and cK, but that will
> have to wait for another time.
>
> Good luck with cK and the theorem prover, keep us informed.

thanks again for your interest.

>
> - Manfred
>
>
>
>
> To unsubscribe from this group, send an email to:
> concatenative-unsubscribe@egroups.com
>
>
>
> Your use of Yahoo! Groups is subject to http://docs.yahoo.com/info/terms/
>
>

resolution theorem prover

stevan apter — 2003-06-07 03:01:44

Samuel Falvo — 2003-06-07 05:22:04

phimvt@lurac.latrobe.edu.au — 2003-06-17 08:28:14

stevan apter — 2003-06-17 12:32:57

John Cowan — 2003-06-17 12:54:10