TODO: write this up as prose:
@keywords is, of, a. @prefix : <speech#>. @prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>. @prefix dc: <http://purl.org/dc/elements/1.1/>. @prefix s: <http://www.w3.org/2000/01/rdf-schema#> . @prefix owl: <http://www.w3.org/2002/07/owl#>. <> dc:source _:ablp. _:ablp dc:title "A Calculus for Access Control in Distributed Systems"; dc:creator "Martin Abadi, Michael Burrows, Butler Lampson, and Gordon Plotkin"; dc:publisher "ACM"; s:comment "Trans. Programming Languages and Systems, 15, 4, pp 706-734."; dc:date "1993-10"; s:seeAlso <http://research.microsoft.com/en-us/um/people/blampson/44-CalculusAccessControl/44-CalculusAccessControlAbstract.html>, <http://research.microsoft.com/en-us/um/people/blampson/44-CalculusAccessControl/44-CalculusAccessControlAsPub.pdf> . # ugh. there seem to be several related papers. # these course notes look right # http://www.ecs.syr.edu/faculty/chin/ACECS/Examples/example6a.pdf # modal stuff @prefix log: <http://www.w3.org/2000/10/swap/log#>. @forAll s, s2, subj, pred, obj, subj2, pred2, obj2, A, B. says s:label "says"; s:domain :Principal. # idemopotency? { A says { A says s } } => { A says s }. speaks_for s:label "speaks for"; s:isDefinedBy _:ablp; s:domain :Principal; s:range :Principal. { ?A speaks_for ?B . ?A says ?s } => { ?B says ?s }. { ?A says s. ?A says { s => s2 }} => { ?A says s2 }. { A says { s => s2 } } => { { A says s } => { A says s2 } }. { ?A a Principal. s a log:Truth } => { ?A says s }. quoting a owl:FunctionalProperty; s:domain rdf:List; # of 2 principals s:range :Principal. #@@ <=> { [is quoting of (?B A)] says s } <=> { ?B says { A says s }}. { [ is quoting of (A B)] says s } => { A says { B says s } }. # need this? { A says { B says s } } => { [ is quoting of (A B) ] says s }. # blows up in fwd chainer: # { ?A says ?p. ?A says ?q. } => { ?A says [ is log:conjunction of (?p ?q)]}. { ?A says { subj pred obj }. ?A says { subj2 pred2 obj2 }. } => { ?A says { subj pred obj. subj2 pred2 obj2 }}. ###### controls s:label "controls"; s:domain :Principal. { ?A controls ?s . ?A says ?s } => { ?s a log:Truth } . #level-breaker. # constrained version of the rule: { ?A controls_spo ( subj pred obj ) ; says [ log:includes { subj pred obj }] } => { subj pred obj }. # constrained version of the rule: { ?A controls_subject ( pred obj ) ; says [ log:includes { subj pred obj }] } => { subj pred obj }. # special case controls_property s:label "controls property"; s:domain Principal; s:range rdf:Property. { ?A controls_property pred. ?A says [log:includes { subj pred obj }] } => { subj pred obj }. ##### # Theorems to help cwm { A says { [ is quoting of (A B)] says s } } => { B says s }. # justification: # { A | B says S } => { A says s } . # defn quoting # A says { { A | B says S } => { A says s } } # principals say all true things # A says { A says s } # implication works inside says # A says s # idemopotency of says # partial treatment of log:Truth { { subj pred obj } a log:Truth } => { subj pred obj }.
ah...
A says s represents the informal statement that principal A says s. Here s may function as an imperative ("the file should be deleted") or not ("C's public key is K"); imperative modalities are not explicit in the fomalism.
Move this to the origin section, when it's written, maybe.
while we're doing deep logic stuff, work this in:
[pD] | H.J. ter Horst, Completeness, Decidability and Complexity of Entailment for RDF Schema and a Semantic Extension Involving the OWL Vocabulary, Journal of Web Semantics 3 (2005) 79-115. |