% $Id: RDFSemantics.lsl,v 1.2 2001/03/30 18:42:44 connolly Exp $
%
%

Algebraic Specification for RDF Models, Sergey Melnik, meknik@db.stanford.edu July 1999. from GINF


RDFSemantics: trait
  includes
    FormalSystem,
    RDFAbSyn,
    Relation(Resource, Rel[Resource]),
    RelSet(Object, Set[Object])

  introduces
    universe, resources, literals, properties: Interpretation ® Set[Object]
    statement: Interpretation, Object, Object, Object ® Bool
    reify: Interpretation, Object, Object, Object ® Object

% melnik 2: basic resources
% leaving containers out for now: Seq, Bag, Alt, N'
    Statement, type, predicate, subject, object, value: Interpretation ® Object

    RDF1: ® System
    andI: ® Rule
    andE: ® Rule
    exI:  ® Rule

    ind: URI, Interpretation ® Resource
    pred: URI, Interpretation ® Rel[Resource]

  asserts
    forall x: Object, m: Interpretation, fls: Set[Formula],
        p, s, o, r, p2, s2, o2: Object

% melnik 1: "Resources and literals are disjunct"
    model(RDF1, m, fls) Þ
      (x Î universe(m) Þ ((x Î resources(m)) Û (x \notin literals(m))));

% skipping melnik 2; I don't see where Kappa is used

% melnik 3: properties are resources [leaving out ordinals for now]
    model(RDF1, m, fls) Þ
      ((x Î properties(m)) Þ (x Î resources(m)));

% melnik 4: set of statements
    model(RDF1, m, fls) Þ
      (statement(m, p, s, o) Þ (p Î properties(m)
                                  Ù s Î resources(m)
                                  Ù o Î universe(m)) );

% melnik 5: [skipping containers for now]

% melnik 6: a resource cannot be typed using a literal
    model(RDF1, m, fls) Þ
      (statement(m, type(m), s, o) Þ o Î resources(m));

% melnik 7: constants for basic resources
% [leaving out Seq, Bag, Alt for now]
    model(RDF1, m, fls) Þ
      (Statement(m) Î (resources(m) - properties(m)));

% melnik 8: constants for basic properties
    model(RDF1, m, fls) Þ
      (type(m) Î properties(m)
      Ù predicate(m) Î properties(m)
      Ù subject(m) Î properties(m)
      Ù object(m) Î properties(m)
      Ù value(m) Î properties(m));

% melnik 9: Rf is a partial one-to-one function
    model(RDF1, m, fls) Þ
    ( reify(m, p, s, o) = r Û (  statement(m, type(m), r, Statement(m))
                                Ù statement(m, predicate(m), r, p)
                                Ù statement(m, subject(m), r, s)
                                Ù statement(m, object(m), r, o) ) );

% melnik 10: uniqueness of reificiation
    model(RDF1, m, fls) Þ
    ( reify(m, p, s, o) = reify(m, p2, s2, o2)
      Þ (p=p2 Ù s=s2 Ù o=o2));


    forall
        f, g: Formula,
        a, b: Atomic,
        i: Interpretation,
        p, s, o: URI

    wff(RDF1, f); %hmm... separate sorts for RDF formula and formula in general?
% i.e. wff(RDF1, asFormula(m))?

    direct_consequence(RDF1, andI, insert(f, {g}), f \U g);
    direct_consequence(RDF1, andE, {insert(a, f)}, {a});

    interpret(RDF1, i, insert(a, f)) = interpret(RDF1, i, {a})
                                         Ù interpret(RDF1, i, f);
    interpret(RDF1, i, {[const(p), const(s), const(o)]}) = ind(s, i) á pred(p, i) ñ ind(o, i);

%@@more: interpretation of formulas with existentials

% Acks/Fodder:
% rm508 meeting: soundness under deletion of arcs; aka erasure

% Semantics of Predicate Calculus
% http://www.cee.hw.ac.uk/courses/3pe1/20/9.htm
% Thu, 16 Nov 2000 17:19:02 GMT

% http://www.google.com/search?q=first+order+predicate+calculus
% http://directory.google.com/Top/Science/Math/Logic_and_Foundations/Computational_Logic/Combinatory_Logic_and_Lambda_Calculus/Formulae-as-Types_Correspondence/

[Index]

[source]

HTML generated using lsl2html.