# resolution theorem prover

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

    i've written a little k resolution theorem prover (for the

    propositional calculus only):

    http://www.nsl.com/k/resolve.k

    i've designed the functions with an eye towards translation

    into ck, which i'll probably complete sometime this weekend.

    no assignments, no explicit loops.  strategies (currently,

    just set of support and unit preference) are passed in as

    functional arguments, which suggests that 'resolve' be

    implemented in ck as a combinator.

    first column of output is step number, second and third are

    resolved steps, fourth onward is the resolved clause.

    e.g.

      `0:p                      / goal is always first clause

    -r

    pq

    pr

    -pr

    rs

    r-q

    -s-q

      resolve[sos;p]            / use set of support strategy

        0             -r

        1              p    q

        2              p    r

        3             -p    r

        4              r    s

        5              r   -q

        6             -s   -q

        7    2    0    p

        8    3    0   -p        / why don't we see this sooner?

        9    4    0    s

       10    5    0   -q

       11    7    3    r

       12    8    1    q

       13    8    2    r

       14    8    7

      resolve[upr;p]            / use unit preference strategy

        0             -r

        1              p    q

        2              p    r

        3             -p    r

        4              r    s

        5              r   -q

        6             -s   -q

        7    2    0    p

        8    7    3    r        / quick!

        9    8    0

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

    > i've written a little k resolution theorem prover (for the

    > propositional calculus only):

    >

    > http://www.nsl.com/k/resolve.k

     Maybe someone has asked this question before, but is there a *GOOD* quality

    introduction to K?  I can't read it in full right now because of other

    obligations, but someone has passed me a link to an intro once, but I wasn't

    too impressed with it.  I've since lost the link though.  I would like another

    link so I can save it in my bookmarks for future viewing.

    As this is off-topic, I'd appreciate a private e-mail response, so as to not

    pollute this list with too much irrelavent traffic.

    Thanks.

    --

    Samuel A. Falvo II

    __________________________________

    Do you Yahoo!?

    Yahoo! Calendar - Free online calendar with sync to Outlook(TM).

    http://calendar.yahoo.com

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

    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.

    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.

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

    I'll use this opportunity to ask some questions about K and cK.

    About K:

       Is it compiled or interpreted?

       What source language is the processor written in?

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

      - Manfred

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

    ----- 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/

    >

    >

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

    stevan apter scripsit:

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

     My Scheme implementation is not functional in the stack -- it side-effects

    a global stack location -- though I have been thinking of rewriting it

    so that it is functional.

    --

    What is the sound of Perl?  Is it not the       John Cowan

    sound of a [Ww]all that people have stopped     jcowan@...

    banging their head against?  --Larry            http://www.ccil.org/~cowan