Swell

% $Id: Swell.lsl,v 1.3 2000/07/27 22:18:04 connolly Exp $

% foundations of Swell, the Semantic Web Logic Language
% cf http://www.w3.org/DesignIssues/
% cf http://www.w3.org/2000/07/hs78/FOPC

Swell: trait
    includes
% each property URI (with optional fragment identifer) is
% a relation from subject URIs to object URIs
% for s \< p \> o you can read: p(s, o) is true,
% or p(s, o) is a theorem.
% @@hm... do a sort of modal extension, where
% p(s, o) is asserted by a message?
        Relation(URIwf, URIwf,
         __ \< __ \> __ for __ á __ ñ __,
        bot for \bot, top for \top)

    introduces
% primitives
        false_ : ® URIwf
        implies_: ® URIwf
        forall_ : ® URIwf

        subject : ® URIwf
        predicate : ® URIwf
        object : ® URIwf

        first: ® URIwf
        rest: ® URIwf
        empty: ® URIwf

% it's axiomatic that for any URIwf's p,s,o, they
% form a statement.. oops! maybe not! maybe subj/obj/pred are
% acyclic!
% hmm... can I reify this operator somehow?
% using some sort of lambda thingy?
% ( (lambda x . body) y ) == http://www.w3.org/2000/07/lambda?body=urlescape(body);arg=urlescape(y)

% short-hands
        quote: URIwf, URIwf, URIwf, URIwf ® Bool % quote(p, s, o, x)
        insert: URIwf, URIwf, URIwf ® Bool % insert(first, rest, l)

% derived stuff

        true : ® URIwf
        negation, conjunction, implication : ® URIwf

        second, restrest : ® URIwf

    asserts
        " p, s, o, x, y, a_l, a, l: URIwf

% shorthand (hmm... could build this on n-ary predicate mechanism)
        quote(p, s, o, x) = (x \< subject \> s
                            Ù x \< predicate \> p
                            Ù x \< object \> o);

        insert(a, l, a_l) = (a_l \< first \> a
                            Ù a_l \< rest \> l);

% define negation
        quote(implies_, x, false_, y)
        Þ x \< negation \> y;

%negation \< type \> symmetric;
        x \< negation \> y
        Þ y \< negation \> x;

% and here we define true:
        false_ \< negation \> true;

% and here we give an axiom for implies_ ...
% this is known as the "level breaking" axiom
        true \< implies_ \> x
        Ù quote(p, s, o, x)
        Þ s \< p \> o;

% the implication of a list of statements...
        empty \< implication \> true;

        a_l \< first \>  a
        Ù a_l \< rest \> l
        Ù l \< implication \> s
        Ù quote(implies_, a, s, x)
        Þ a_l \< implication \> x;

% define second
        s \< first \> x
        Ù o \< rest \> x
        Þ s \< second \> o;

% build a conjuction from implies_, false_
        empty \< conjunction \> true;

        " a, l, a_l,  s, notS,
                a_notS, impliesANotS, notImpliesANotS: URIwf

        l \< conjunction \> s
        Ù insert(a, l, a_l)
        Ù s \< negation \> notS
        Ù a_notS \< first \> a
        Ù a_notS \< second \> notS
        Ù a_notS \< restrest \> empty
        Ù a_notS \< implication \> impliesANotS
        Ù impliesANotS \< negation \> notImpliesANotS
        Þ a_l \< conjunction \> notImpliesANotS;

[Index]

[source]

HTML generated using lsl2html.