Re: N3 semantics w.r.t. Acl2?

On Sun, 2005-08-28 at 20:20 -0500, Dan Connolly wrote:

> What of wtr and intuitionistic? S4, provability, ...





Partial functions

What about functions that aren't total? The ACL2 convention seems to be
to make them total somehow...

        when non-numeric arguments are provided, the functions act as
        though 0 had been provided.

Existential Variables

What to do with formulas like the following?

        car normalLocation [ a Garage ].

I recall some discussion of skolemization and choice. Hmm.


Substitution

I think there's a (subst) library function, no?

Generalized Modus Ponens

Hmm... ACL2 has no quantification. How to represent it...

        (defun (log:implies F G) (or (not F) G))

No, that assumes F and G are t/f constants, not formulas.

Hmm...

        Actually, ACL2 does provide full first-order quantification via
        defun-sk.

Atomic Formulas


So... how to represent the basic sentence of RDF? i.e.

        @keywords is, of, a.
        car color blue.

Ah...

        In ACL2, "relations" and "predicates" are defined as Boolean
        valued functions...
        -- Finite Set Theory in ACL2, by J Strother Moore

so...

        (holds car color blue)

but... oops... how to define holds? It's not computable, in general, is
it? Suppose the extent of each predicate is computable... and finite...

        (defun (lookup p) ...)
        (defun (extent p) ...)
        (defun (holds p s o) (mem (pair s o) (extent p)) )

Maybe the thing to do is, rather than translating N3 to ACL2, define the
proof theory (or provability logic) of N3 in ACL2. That doesn't give a
semantics for N3, but it might still be useful. e.g. to get a proof of
B' from a proof of A => B and a proof of A', where B' is (subst (match
A' A) B):

        (defun (generalized-modus-ponens pfA pfAimpB)
         (let (bindings (match (conclusion pfA) (antecedent (conclusion
        pfAimpB))))
          (subst bindings (consequent (conclusion pfAimpB))) ) )

umm... that returns B'. Maybe the thing to define in ACL2 is the proof
checker:

        (defun (check-gmp pf)
          (and (listp pf)
               (rule pf :GMP)
               (equal 2 (premise-qty pf))
               (let* ( (pfA2 (premise 1 pf))
                       (pfAimpB (premise 2 pf))
                       (A2 (conclusion pfA2))
                       (B (consequent (conclusion pfAimpB)))
                       (bindings (match A A2))
                     )
                (equal (subst bindings B) (conclusion pf))
              )

But now we're back to using ACL2 as an ordinary programming language,
and we might as well use python or Java.

-- 
Dan Connolly, research scientist, MIT CSAIL
Decentralized Information Group http://groups.csail.mit.edu/dig/
office: tel:+1-617-395-0241
mobile: mailto:connolly+pager@w3.org