From: Dan Connolly <connolly@w3.org>

Date: Thu, 01 Sep 2005 22:23:03 -0500

To: www-archive+breadcrumbs@w3.org

Message-Id: <1125631384.16011.741.camel@dirk>

Date: Thu, 01 Sep 2005 22:23:03 -0500

To: www-archive+breadcrumbs@w3.org

Message-Id: <1125631384.16011.741.camel@dirk>

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.orgReceived on Friday, 2 September 2005 03:23:12 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 7 January 2015 14:42:53 UTC
*