% $Id: Swell.html,v 1.1 2003/10/01 07:22:16 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 ⊥, top for ⊤)
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]
HTML generated using lsl2html.