Re: Is n3 a rules language or a logic language?

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