#Processed by Id: cwm.py,v 1.179 2005/10/28 01:38:42 timbl Exp # using base file:/devel/WWW/2000/10/swap/test/reason/ # Notation3 generation by # notation3.py,v 1.184 2005/10/24 16:58:38 timbl Exp # Base was: file:/devel/WWW/2000/10/swap/test/reason/ @prefix : . @prefix crypto: . @prefix en: . @prefix eng: . @prefix http: . @prefix jud: . @prefix judy: . @prefix list: . @prefix log: . @prefix math: . @prefix n3: . @prefix owl: . @prefix pr: . @prefix rdf: . @prefix rdfs: . @prefix rein: . @prefix session: . @prefix str: . @prefix t: . @prefix t2: . @prefix t3: . @forSome <#_g0>, <#_g1>, <#_g2>, <#_g3>, <#_g4> . [ a pr:Conjunction, pr:Proof; pr:component [ a pr:Inference; pr:binding [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/judy-req#req" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#REQ" ] ], [ pr:boundTo [ n3:uri "http://demo.policyawareweb.org/images/group.jpg" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#RESOURCE" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/http-access#can-get" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#ACCESS" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/judy-req.n3#_g_L8C18" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#WHO" ] ], [ pr:boundTo { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . a http:Photo; rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> http:can-get ; session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27>, <#_g28> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g18>, <#_g19>, <#_g20> . <#_g21>, <#_g22> . <#_g23>, <#_g24> . <#_g25> . <#_g26> . <#_g27>, <#_g28> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g19>, <#_g22>, <#_g28>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g20>, <#_g24>, <#_g25>, <#_g26>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g18>, <#_g21>, <#_g23>, <#_g27> . } a t2:TroopStuff . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#G" ] ], [ pr:boundTo [ n3:nodeId "http://dig.csail.mit.edu/2005/09/rein/examples/judy-req#_L14C8" ]; pr:variable [ n3:nodeId "http://dig.csail.mit.edu/2005/09/rein/filter.n3#_g_L22C40" ] ]; pr:evidence ( [ a pr:Extraction; pr:because <#_g1>; pr:gives {judy:req rein:resource . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives { @forSome jud:_g_L8C18 . judy:req rein:requester jud:_g_L8C18 . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives {judy:req rein:access http:can-get . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives {judy:req a rein:Request . } ] [ a pr:Extraction; pr:because [ a pr:Inference; pr:binding [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/troop42-policy.n3" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#POLICY" ] ], [ pr:boundTo { @forAll :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine.n3#_g_L42C50" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/http-access#can-get" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#ACCESS" ] ], [ pr:boundTo { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#F" ] ], [ pr:boundTo { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . a http:Photo; rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> http:can-get ; session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27>, <#_g28> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g18>, <#_g19>, <#_g20> . <#_g21>, <#_g22> . <#_g23>, <#_g24> . <#_g25> . <#_g26> . <#_g27>, <#_g28> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g19>, <#_g22>, <#_g28>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g20>, <#_g24>, <#_g25>, <#_g26>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g18>, <#_g21>, <#_g23>, <#_g27> . } a t2:TroopStuff . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#G" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/judy-req#req" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#REQ" ] ], [ pr:boundTo [ n3:uri "http://demo.policyawareweb.org/images/group.jpg" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#RESOURCE" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/http-access.rdf" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#LANG" ] ], [ pr:boundTo {http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine.n3#_g_L36C8" ] ], [ pr:boundTo { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S . rein:policy-language . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine.n3#_g_L40C12" ] ], [ pr:boundTo {http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine.n3#_g_L41C10" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/judy-req.n3#_g_L8C18" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#WHO" ] ], [ pr:boundTo { @forSome <#_g5> . rein:policy . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . <#_g5> session:secret "judy-passwd" . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine.n3#_g_L37C9" ] ]; pr:evidence ( [ a pr:Extraction; pr:because [ a pr:Inference; pr:binding [ pr:boundTo [ n3:uri "http://demo.policyawareweb.org/images/group.jpg" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#RESOURCE" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/troop42-policy.n3" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#POLICY" ] ], [ pr:boundTo { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S . rein:policy-language . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine.n3#_g_L16C9" ] ], [ pr:boundTo [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/examples/http-access.rdf" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#LANG" ] ]; pr:evidence ( [ a pr:Extraction; pr:because <#_g1>; pr:gives { rein:policy . } ] [ a pr:Fact; pr:gives { log:semantics { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S . rein:policy-language . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } . } ] <#_g3> <#_g3> ); pr:rule [ a pr:Extraction; pr:because <#_g2>; pr:gives { @forAll eng:LANG, eng:POLICY, eng:RESOURCE . { @forSome en:_g_L16C9 . eng:POLICY log:semantics en:_g_L16C9 . eng:RESOURCE rein:policy eng:POLICY . en:_g_L16C9 log:includes {eng:POLICY rein:policy-language eng:LANG . } . } log:implies {eng:POLICY rein:policy-language eng:LANG . } . } ] ]; pr:gives { rein:policy-language . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives { rein:policy . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives {judy:req rein:access http:can-get . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives {judy:req rein:resource . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives { @forSome jud:_g_L8C18 . judy:req rein:requester jud:_g_L8C18 . } ] [ a pr:Extraction; pr:because <#_g1>; pr:gives {judy:req a rein:Request . } ] [ a pr:Fact; pr:gives { log:semantics { @forAll :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . } . } ] [ a pr:Fact; pr:gives { log:semantics {http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . } . } ] [ a pr:Fact; pr:gives { log:semantics { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S . rein:policy-language . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } . } ] [ a pr:Fact; pr:gives {judy:req log:semantics { @forSome <#_g5> . rein:policy . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . <#_g5> session:secret "judy-passwd" . } . } ] [ a pr:Fact; pr:gives { ( { @forSome <#_g5> . rein:policy . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . <#_g5> session:secret "judy-passwd" . } { rein:policy . } { rein:policy-language . } { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S . rein:policy-language . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } {http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . } { @forAll :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . } ) log:conjunction { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } . } ] [ a pr:Fact; pr:gives {{ @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } log:conclusion { @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . a http:Photo; rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> http:can-get ; session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27>, <#_g28> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g18>, <#_g19>, <#_g20> . <#_g21>, <#_g22> . <#_g23>, <#_g24> . <#_g25> . <#_g26> . <#_g27>, <#_g28> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g19>, <#_g22>, <#_g28>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g20>, <#_g24>, <#_g25>, <#_g26>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g18>, <#_g21>, <#_g23>, <#_g27> . } a t2:TroopStuff . } . } ] [ a pr:Fact; pr:gives { log:semantics {http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . } . } ] [ a pr:Fact; pr:gives {{ http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . } log:notIncludes { @forSome en:_g_L36C41, en:_g_L36C61 . en:_g_L36C41 rein:meta-policy en:_g_L36C61 . } . } ] ); pr:rule [ a pr:Extraction; pr:because <#_g2>; pr:gives { @forAll eng:ACCESS, eng:F, eng:G, eng:LANG, eng:POLICY, eng:REQ, eng:RESOURCE, eng:WHO . { @forSome en:_g_L36C8, en:_g_L37C9, en:_g_L40C12, en:_g_L41C10, en:_g_L42C50 . ( en:_g_L37C9 {eng:RESOURCE rein:policy eng:POLICY . } {eng:POLICY rein:policy-language eng:LANG . } en:_g_L40C12 en:_g_L41C10 en:_g_L42C50 ) log:conjunction eng:F . eng:F log:conclusion eng:G . eng:LANG log:semantics en:_g_L36C8, en:_g_L41C10 . eng:POLICY rein:policy-language eng:LANG; log:semantics en:_g_L40C12 . eng:REQ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE; log:semantics en:_g_L37C9 . eng:RESOURCE rein:policy eng:POLICY . en:_g_L36C8 log:notIncludes { @forSome en:_g_L36C41, en:_g_L36C61 . en:_g_L36C41 rein:meta-policy en:_g_L36C61 . } . log:semantics en:_g_L42C50 . } log:implies {eng:G eng:has eng:ans . } . } ] ]; pr:gives {{ @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . a http:Photo; rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> http:can-get ; session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27>, <#_g28> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g18>, <#_g19>, <#_g20> . <#_g21>, <#_g22> . <#_g23>, <#_g24> . <#_g25> . <#_g26> . <#_g27>, <#_g28> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g19>, <#_g22>, <#_g28>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g20>, <#_g24>, <#_g25>, <#_g26>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g18>, <#_g21>, <#_g23>, <#_g27> . } a t2:TroopStuff . } eng:has eng:ans . } ] <#_g4> <#_g4> <#_g4> ); pr:rule [ a pr:Extraction; pr:because [ a pr:Parsing; pr:because <#_g0>; pr:source ]; pr:gives { @forAll eng:ACCESS, eng:G, eng:REQ, eng:RESOURCE, eng:WHO . { eng:G eng:has eng:ans; log:includes { @forSome <#_g29> . eng:REQ rein:requester <#_g29> . <#_g29> eng:ACCESS eng:RESOURCE . } . eng:REQ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE . } log:implies {eng:REQ rein:ans rein:Valid; rein:requester [ eng:ACCESS eng:RESOURCE ] . } . } ] ]; pr:gives {judy:req rein:ans rein:Valid; rein:requester [ http:can-get ] . } ]. <#_g0> a pr:CommandLine; pr:args "['/devel/WWW/2000/10/swap/cwm.py', '--chatty=9', '--n3=B', 'http://dig.csail.mit.edu/2005/09/rein/examples/judy-req.n3', 'http://dig.csail.mit.edu/2005/09/rein/engine.n3', '--mode=h', '--think', '--chatty=90', '--filter=http://dig.csail.mit.edu/2005/09/rein/filter.n3', '--chatty=30', '--why']" . <#_g1> a pr:Parsing; pr:because <#_g0>; pr:source . <#_g2> a pr:Parsing; pr:because <#_g0>; pr:source . <#_g3> a pr:Fact; pr:gives {{ @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S . rein:policy-language . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } log:includes { rein:policy-language eng:LANG . } . } . <#_g4> a pr:Fact; pr:gives {{ @forAll t2:LOC, t2:PG, t2:PHOTO, t2:REQ, t2:TXT, t2:WHO, t2:X, t3:F, t3:PHOTO, t3:S, :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y. @forSome <#_g5> . a http:Photo; rein:policy . http:Photo a rdfs:Class . http:can-get a rein:PositiveAccess, rdf:Property; rdfs:range http:Photo . http:cannot-get a rein:NegativeAccess, rdf:Property; rdfs:range http:Photo . judy:req a rein:Request; rein:access http:can-get; rein:requester <#_g5>; rein:resource ; rdfs:comment "Judy makes a request for http://demo.policyawareweb.org/images/group.jpg which was taken during AnnualMeeting which Judy attended. This is a valid request." . rein:policy-language . :rcsid "$Id: judy-proof.n3,v 1.2 2005/11/02 00:06:26 timbl Exp $" . rdf:first a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdfs:Resource . rdf:rest a owl:FunctionalProperty; rdfs:domain rdf:List; rdfs:range rdf:List . rdfs:subClassOf a owl:TransitiveProperty; rdfs:domain rdfs:Class; rdfs:range rdfs:Class . rdfs:subPropertyOf a owl:TransitiveProperty; rdfs:domain rdf:Property; rdfs:range rdf:Property . owl:differentFrom a owl:SymmetricProperty; rdfs:domain owl:Thing; rdfs:range owl:Thing . owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List . owl:inverseOf a owl:SymmetricProperty; rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty . <#_g5> http:can-get ; session:secret "judy-passwd" . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { :A rdfs:subClassOf :B . :S a :A . } log:implies {:S a :B . } . { :A owl:distinctMembers :D . :D rdf:rest :R . } log:implies {:A owl:distinctMembers :R . } . { :C owl:oneOf :L . :X list:in :L . } log:implies {:X a :C . } . { :L a rdf:List; rdf:first :I . } log:implies {:I list:in :L . } . { :P a owl:SymmetricProperty . :S :P :O . } log:implies {:O :P :S . } . { :P rdfs:domain :C . :S :P :O . } log:implies {:S a :C . } . { :P rdfs:range :C . :S :P :O . } log:implies {:O a :C . } . { :P rdfs:subPropertyOf :R . :S :P :O . } log:implies {:S :R :O . } . { :P owl:inverseOf :Q . :S :P :O . } log:implies {:O :Q :S . } . { ( 1.0 :M ) math:difference :N . ( :X :A ) :M . :C owl:complementOf :A . } log:implies { ( :X :C ) :N . } . { :I list:in :R . :L a rdf:List; rdf:rest :R . } log:implies {:I list:in :L . } . { :L a rdf:List; rdf:rest :R . :X :R . } log:implies {:X :L . } . { :P a owl:FunctionalProperty . :S :P :X, :Y . } log:implies {:X = :Y . } . { :P a owl:InverseFunctionalProperty . :X :P :O . :Y :P :O . } log:implies {:X = :Y . } . { :P a owl:TransitiveProperty . :S :P :X . :X :P :O . } log:implies {:S :P :O . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :M . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:intersectionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:lessThan :N . } log:implies { ( :X :C ) :N . } . { ( :X :A ) :M . ( :X :B ) :N . :C owl:unionOf ( :A :B ) . :M math:notLessThan :N . } log:implies { ( :X :C ) :M . } . { @forSome <#_g6> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g6> . <#_g6> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g7> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g7> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g7> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g8> . t2:PG log:semantics <#_g8> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes {t2:LOC a t:Meeting . t2:PHOTO a t:Photo; t:location t2:LOC . }, { @forSome <#_g9>, <#_g10> . t2:LOC t:attendee <#_g10> . t2:PG <#_g9>, <#_g10> . [ t:member <#_g9> ]. } . t3:S crypto:md5 t2:TXT . <#_g8> log:includes { @forSome <#_g11> . t2:PG <#_g11> . <#_g11> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g12> . t2:PG log:semantics <#_g12> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g13> . t2:PG <#_g13> . [ t:member <#_g13> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g12> log:includes { @forSome <#_g14> . t2:PG <#_g14> . <#_g14> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g15> . t2:PG log:semantics <#_g15> . t2:REQ a rein:Request; rein:requester t2:WHO; rein:resource t2:PHOTO . t2:WHO session:secret t3:S . t3:F a t2:TroopStuff; log:includes { @forSome <#_g16> . t2:LOC t:attendee <#_g16> . t2:PG <#_g16> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g15> log:includes { @forSome <#_g17> . t2:PG <#_g17> . <#_g17> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27>, <#_g28> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g18>, <#_g19>, <#_g20> . <#_g21>, <#_g22> . <#_g23>, <#_g24> . <#_g25> . <#_g26> . <#_g27>, <#_g28> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g19>, <#_g22>, <#_g28>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g20>, <#_g24>, <#_g25>, <#_g26>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g18>, <#_g21>, <#_g23>, <#_g27> . } a t2:TroopStuff . } log:includes { @forSome <#_g29> . judy:req rein:requester <#_g29> . <#_g29> http:can-get . } . } . #ENDS