From: naudts guido <naudts_vannoten@yahoo.com>

Date: Fri, 6 Sep 2002 11:31:06 -0700 (PDT)

Message-ID: <20020906183106.69147.qmail@web40513.mail.yahoo.com>

To: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>, "Sandro Hawke <sandro" <sandro@w3.org>

Cc: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, timbl@w3.org, www-rdf-rules@w3.org, naudts_vannoten@yahoo.com

Received on Friday, 6 September 2002 14:44:08 UTC

Date: Fri, 6 Sep 2002 11:31:06 -0700 (PDT)

Message-ID: <20020906183106.69147.qmail@web40513.mail.yahoo.com>

To: Jos De_Roo <jos.deroo.jd@belgium.agfa.com>, "Sandro Hawke <sandro" <sandro@w3.org>

Cc: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, timbl@w3.org, www-rdf-rules@w3.org, naudts_vannoten@yahoo.com

--- Jos De_Roo <jos.deroo.jd@belgium.agfa.com> wrote: > [...] > > > (This gives me a fun idea for a cwm test: write > resolution in n3, and > > see what things I can get cwm to prove. I bet I > can get cwm to prove > > this isn't the way to implement a fast theorem > prover. :-) > > actually Guido Naudts is making a nice attempt in > http://www.agfa.com/w3c/2002/02/thesis/ > more specifically > http://www.agfa.com/w3c/2002/02/thesis/engine.n3 This was a first trial. Attached is a somewhat more elaborate trial (N3Spec.n3). It might still contain errors. After some reflexions this evening however (on the train) it dawned to me that Haskell functions in a certain format (the way I write all my functions) can be automatically translated into SWeLL rules and facts.See the attachment: haskell_to_n3.doc Guido Naudts > > -- , > Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/ __________________________________________________ Do You Yahoo!? Yahoo! Finance - Get real-time stock quotes http://finance.yahoo.com @prefix log: <http://www.w3.org/2000/10/swap/log#>. # Build a datastructure representing a triple. # The triple is: :s :v :o1, :o2; :v1, :o3. :t a :triple. # a triple is a list of a subject and a propertylist. :triple a :list. :t :add :s, :p. :s a :subject. :p a :propertylist. # a propertylist is a list of properties :propertylist a :list. :p :add :p1, :p2. :p1 a :property. :p2 a :property. # a property is a list of a verb and an objectlist :p1 :add :v, :o. :v a :verb. :o a :objectlist. # an objectlist is a list of objects. :objectlist a :list. :o :add :o1, :o2, :o3. :o1 a :object. :o2 a :object. :o3 a :object. # define p2 :p2 :add :v1, :o3. :v1 a :verb. :o3 a :object. # define properties of list :list :has :head. :list :has :tail. # definition of a simple triple {?:t a :triple.?:s :head ?:t. ?:p :tail ?:t. ?:v :head ?:p. ?:o :tail ?:p. ?:s a :subject. ?:v a :verb. ?:o a :object.} log:implies {?:t a :simpleTriple};log:forAll ?:t, ?:s, :p, ?:v, ?:o. # Unification of a triple # ?:p and ?:p1 are propertylists. # substitutions are accumulated in ?:subst !!! # ?:p2 ?:subst ?:p. means ?:p2 is the result of applying the substitution ?:subst to ?:p. {?:t a :simpleTriple. ?:t1 a :triple. ?:s :head ?:t. ?:s1 :head ?:t1.?:subst a :list. ?:subst = {?:s :unification ?:s1}. ?:subst a :substitution. ?:p :tail ?:t. ?:p1 :tail ?:t1. ?:p2 ?:subst ?:p. ?:p3 ?:subst ?:p1. ?:subst = {:p2 :unification ?:p3} log:implies {?: subst = {?:t :unification ?:t1}; log:forAll ?:t, ?:t1, ?:s, ?:s1, ?:p, ?:p1, ?:subst. # unification of a simple property with a propertylist. {?:p a :property. ?:p1 a :propertylist. ?:p2 :head ?:p1. ?:p :unification ?:p2} log:implies {?:p :unification ?:p1}; log:forAll ?:p, ?:p1, ?:p2. {?:p a :property. ?:p1 a :propertylist. ?:p2 :head ?:p1. ?:p :no_unification ?:p2. ?:p3 :tail ?:p1. ?:p :unification ?:p3} log:implies {?:p :unification ?:p1}; log:forAll ?:p, ?:p1, ?:p2, ?:p3. # unification of two properties {?:p a :property. ?:p1 a :property. ?:v :head ?:p. ?:v1 :head ?:p1. ?:v :unification ?:v1.?:o :tail ?:p. :o1 :tail :p1. :o :unification :o1.} log:implies {:p :unification :p1}; log:forAll ?:p, ?:p1, ?:v, ?:v1, ?:o, ?:o1. # unification of a simple object with a objectlist. {?:o a :object. ?:o1 a :objectlist. ?:o2 :head ?:o1. ?:o :unification ?:o2} log:implies {?:o :unification ?:o1}; log:forAll ?:o, ?:o1, ?:o2. {?:o a :object. ?:o1 a :objectlist. ?:o2 :head ?:o1. ?:o :no_unification ?:o2. ?:o3 :tail ?:o1. ?:o :unification ?:o3} log:implies {?:o :unification ?:o1}; log:forAll ?:o, ?:o1, ?:o2, ?:o3. # unification of two objects = unification of two atoms # subject, verb and object are atoms # an atom is a URI or a variable :subject a :atom. :verb a :atom. :object a :atom. # unification of two atoms {?:a a :atom. ?:a a :URI. ?:b a :atom. ?:b a :URI. ?:a = ?:b. ?:subst :add :nullSubstitution } log:implies {?subst = {?:a :unification ?:b}.}; log:forAll ?:a, ?:b, ?:subst. {?:a a :atom. ?:a a :URI. ?:b a :atom. ?:b a :Var.?:subst :add {?:a :substitutes ?:b} } log:implies {?:subst = {?:a :unification ?:b}.}; log:forAll ?:a, ?:b, ?:subst. {?:a a :atom. ?:a a :Var. ?:b a :atom. ?:b a :URI. } log:implies {?:a :unification ?:b. {?:a :substitutes ?:b} a :substitution}; log:forAll ?:a, ?:b. {?:a a :atom. ?:a a :URI. ?:b a :atom. ?:b a :URI. ?:a :notEqual ?:b.} log:implies {?:a :no_unification ?:b}; log:forAll ?:a, ?:b. {?:a a :atom. ?:a a :Var. ?:b a :atom. ?:b a :Var. } log:implies {?:a :unification ?:b. {?:a :substitutes ?:b.} a :substitution. {?:b :substitutes ?:a.} a :substitution}; log:forAll ?:a, ?:b. # apply a substitution {?:subst1 :head ?:subst. ?:subst1 = {?:a :substitutes ?:b}. ?:subst2 :tail ?:subst. ?:c ?:subst2 ?:b.} log:implies {?:c ?:subst ?:a}; # a nullSubstitution is a substitution # must be the last substitution statement ??? :nullSubstitution a :substitution

- application/msword attachment: haskell_to_N3.doc

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:13 UTC
*