% $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.