@prefix : . @prefix ben: . @prefix bfi: . @prefix crypto: . @prefix eng: . @prefix http: . @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> . [ a pr:Conjunction, pr:Proof; pr:component [ a pr:Inference; pr:binding [ pr:boundTo { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . <#_g4> http:can-get ; session:id rein:test; session:secret "judy-passwd" . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g17>, <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g17>, <#_g18>, <#_g19> . <#_g20>, <#_g21> . <#_g22>, <#_g23> . <#_g24> . <#_g25> . <#_g26>, <#_g27> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g18>, <#_g21>, <#_g27>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g19>, <#_g23>, <#_g24>, <#_g25>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g17>, <#_g20>, <#_g22>, <#_g26> . } a t2:TroopStuff . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#G" ] ], [ pr:boundTo [ n3:nodeId "file:/devel/WWW/2000/10/swap/test/reason/.run-1131113110.7427831p9788#_g131" ]; pr:variable [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/bfilter.n3#_g_L16C21" ] ], [ pr:boundTo [ n3:nodeId "file:/devel/WWW/2000/10/swap/test/reason/.run-1131113110.7427831p9788#_g27" ]; pr:variable [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/bfilter.n3#_g_L16C99" ] ], [ pr:boundTo [ n3:uri "http://demo.policyawareweb.org/images/award.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:evidence ( [ a pr:Extraction; pr:because [ a pr:Inference; pr:binding [ pr:boundTo [ n3:nodeId "file:/devel/WWW/2000/10/swap/test/reason/.run-1131113110.7427831p9788#_g26" ]; pr:variable [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/bengine.n3#_g_L34C22" ] ], [ 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 [ n3:nodeId "file:/devel/WWW/2000/10/swap/test/reason/.run-1131113110.7427831p9788#_g27" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#WHO" ] ], [ 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 { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#RF" ] ], [ pr:boundTo { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . <#_g4> http:can-get ; session:id rein:test; session:secret "judy-passwd" . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g17>, <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g17>, <#_g18>, <#_g19> . <#_g20>, <#_g21> . <#_g22>, <#_g23> . <#_g24> . <#_g25> . <#_g26>, <#_g27> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g18>, <#_g21>, <#_g27>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g19>, <#_g23>, <#_g24>, <#_g25>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g17>, <#_g20>, <#_g22>, <#_g26> . } a t2:TroopStuff . }; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#G" ] ], [ 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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . }; pr:variable [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/bengine.n3#_g_L45C12" ] ], [ 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://groups.csail.mit.edu/dig/2005/09/rein/bengine.n3#_g_L46C10" ] ], [ pr:boundTo { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . }; pr:variable [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/bengine.n3#_g_L44C58" ] ], [ pr:boundTo { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> 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 :A, :B, :C, :D, :I, :L, :M, :N, :O, :P, :Q, :R, :S, :X, :Y . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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://groups.csail.mit.edu/dig/2005/09/rein/bengine.n3#_g_L47C50" ] ], [ 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://groups.csail.mit.edu/dig/2005/09/rein/bengine.n3#_g_L40C8" ] ], [ pr:boundTo [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/examples/troop42-policy.n3" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#POLICY" ] ], [ pr:boundTo [ n3:uri "http://demo.policyawareweb.org/images/award.jpg" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#RESOURCE" ] ]; pr:evidence ( [ a pr:Extraction; pr:because [ a pr:Inference; pr:binding [ pr:boundTo [ n3:uri "http://demo.policyawareweb.org/images/award.jpg" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#RESOURCE" ] ], [ pr:boundTo [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/examples/troop42-policy.n3" ]; pr:variable [ n3:uri "http://dig.csail.mit.edu/2005/09/rein/engine#POLICY" ] ], [ 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 { @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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . }; pr:variable [ n3:uri "http://groups.csail.mit.edu/dig/2005/09/rein/bengine.n3#_g_L16C9" ] ]; pr:evidence ( [ a pr:Extraction; pr:because <#_g0>; 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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } . } ] <#_g1> <#_g1> ); pr:rule [ a pr:Extraction; pr:because <#_g0>; pr:gives { @forAll eng:LANG, eng:POLICY, eng:RESOURCE . { @forSome ben:_g_L16C9 . eng:POLICY log:semantics ben:_g_L16C9 . eng:RESOURCE rein:policy eng:POLICY . ben:_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 <#_g0>; pr:gives { rein:policy . } ] [ a pr:Extraction; pr:because <#_g0>; pr:gives {{ @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . } ] <#_g2> <#_g2> <#_g2> <#_g2> <#_g2> [ 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: paw-proof.n3,v 1.1 2005/12/21 19:41: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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } . } ] [ a pr:Fact; pr:gives { log:semantics { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . } . } ] [ a pr:Fact; pr:gives { ( {{ @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . } { rein:policy . } { rein:policy-language . } { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . } { @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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> 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: paw-proof.n3,v 1.1 2005/12/21 19:41: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 eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } . } ] [ a pr:Fact; pr:gives {{ @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } log:conclusion { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . <#_g4> http:can-get ; session:id rein:test; session:secret "judy-passwd" . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g17>, <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g17>, <#_g18>, <#_g19> . <#_g20>, <#_g21> . <#_g22>, <#_g23> . <#_g24> . <#_g25> . <#_g26>, <#_g27> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g18>, <#_g21>, <#_g27>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g19>, <#_g23>, <#_g24>, <#_g25>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g17>, <#_g20>, <#_g22>, <#_g26> . } 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 ben:_g_L40C41, ben:_g_L40C61 . ben:_g_L40C41 rein:meta-policy ben:_g_L40C61 . } . } ] ); pr:rule [ a pr:Extraction; pr:because <#_g0>; pr:gives { @forAll eng:ACCESS, eng:F, eng:G, eng:LANG, eng:POLICY, eng:RESOURCE, eng:RF, eng:WHO . { @forSome ben:_g_L40C8, ben:_g_L44C58, ben:_g_L45C12, ben:_g_L46C10, ben:_g_L47C50 . ( {eng:RF a rein:RequestFormula . } {eng:RESOURCE rein:policy eng:POLICY . } {eng:POLICY rein:policy-language eng:LANG . } ben:_g_L44C58 ben:_g_L45C12 ben:_g_L46C10 ben:_g_L47C50 ) log:conjunction eng:F . eng:F log:conclusion eng:G . eng:LANG log:semantics ben:_g_L40C8, ben:_g_L46C10 . eng:POLICY rein:policy-language eng:LANG; log:semantics ben:_g_L45C12 . eng:RESOURCE rein:policy eng:POLICY . eng:RF a rein:RequestFormula; log:includes { @forSome ben:_g_L34C22 . ben:_g_L34C22 a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE . } . ben:_g_L40C8 log:notIncludes { @forSome ben:_g_L40C41, ben:_g_L40C61 . ben:_g_L40C41 rein:meta-policy ben:_g_L40C61 . } . log:semantics ben:_g_L44C58 . log:semantics ben:_g_L47C50 . } log:implies {eng:G eng:has eng:ans . } . } ] ]; pr:gives { @forAll eng:ACCESS, eng:RESOURCE, eng:RF, eng:WHO . { @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . <#_g4> http:can-get ; session:id rein:test; session:secret "judy-passwd" . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g17>, <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g17>, <#_g18>, <#_g19> . <#_g20>, <#_g21> . <#_g22>, <#_g23> . <#_g24> . <#_g25> . <#_g26>, <#_g27> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g18>, <#_g21>, <#_g27>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g19>, <#_g23>, <#_g24>, <#_g25>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g17>, <#_g20>, <#_g22>, <#_g26> . } a t2:TroopStuff . } eng:has eng:ans . } ] <#_g3> <#_g3> <#_g3> <#_g3> <#_g3> <#_g3> ); pr:rule [ a pr:Extraction; pr:because [ a pr:Parsing; pr:because [ a pr:CommandLine; pr:args "REIN bfilter.n3@@" ]; pr:source ]; pr:gives { @forAll eng:ACCESS, eng:G, eng:RESOURCE . { eng:G eng:has eng:ans; log:includes { @forSome bfi:_g_L16C21, bfi:_g_L16C99 . bfi:_g_L16C21 a rein:Request; rein:access eng:ACCESS; rein:requester bfi:_g_L16C99; rein:resource eng:RESOURCE . bfi:_g_L16C99 eng:ACCESS eng:RESOURCE . } . } log:implies { @forSome bfi:_g_L17C107, bfi:_g_L17C8 . bfi:_g_L17C107 eng:ACCESS eng:RESOURCE . bfi:_g_L17C8 a rein:Request; rein:access eng:ACCESS; rein:ans rein:Valid; rein:requester bfi:_g_L17C107; rein:resource eng:RESOURCE . } . } ] ]; pr:gives { [ a rein:Request; rein:access http:can-get; rein:ans rein:Valid; rein:requester [ http:can-get ]; rein:resource ]. } ]. <#_g0> a pr:Premise; pr:gives { @forAll eng:ACCESS, eng:F, eng:G, eng:LANG, eng:META, eng:POLICY, eng:RESOURCE, eng:RF, eng:WHO . rein:policy . { @forSome ben:_g_L16C9 . eng:POLICY log:semantics ben:_g_L16C9 . eng:RESOURCE rein:policy eng:POLICY . ben:_g_L16C9 log:includes {eng:POLICY rein:policy-language eng:LANG . } . } log:implies {eng:POLICY rein:policy-language eng:LANG . } . { @forSome ben:_g_L21C7 . eng:LANG log:semantics ben:_g_L21C7 . eng:POLICY rein:policy-language eng:LANG . ben:_g_L21C7 log:includes {eng:LANG rein:meta-policy eng:META . } . } log:implies {eng:LANG rein:meta-policy eng:META . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome ben:_g_L40C8, ben:_g_L44C58, ben:_g_L45C12, ben:_g_L46C10, ben:_g_L47C50 . ( {eng:RF a rein:RequestFormula . } {eng:RESOURCE rein:policy eng:POLICY . } {eng:POLICY rein:policy-language eng:LANG . } ben:_g_L44C58 ben:_g_L45C12 ben:_g_L46C10 ben:_g_L47C50 ) log:conjunction eng:F . eng:F log:conclusion eng:G . eng:LANG log:semantics ben:_g_L40C8, ben:_g_L46C10 . eng:POLICY rein:policy-language eng:LANG; log:semantics ben:_g_L45C12 . eng:RESOURCE rein:policy eng:POLICY . eng:RF a rein:RequestFormula; log:includes { @forSome ben:_g_L34C22 . ben:_g_L34C22 a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE . } . ben:_g_L40C8 log:notIncludes { @forSome ben:_g_L40C41, ben:_g_L40C61 . ben:_g_L40C41 rein:meta-policy ben:_g_L40C61 . } . log:semantics ben:_g_L44C58 . log:semantics ben:_g_L47C50 . } log:implies {eng:G eng:has eng:ans . } . }; pr:text "got it from an HTTP request@@" . <#_g1> 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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . } log:includes { rein:policy-language eng:LANG . } . } . <#_g2> a pr:Fact; pr:gives {{ @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } log:includes { @forSome ben:_g_L34C22 . ben:_g_L34C22 a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource . } . } . <#_g3> a pr:Fact; pr:gives {{ @forAll eng:ACCESS, eng:PROP, eng:RESOURCE, eng:RF, eng:VALUE, eng:WHO, 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 . 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 . rein:policy-language . :rcsid "$Id: paw-proof.n3,v 1.1 2005/12/21 19:41: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 . <#_g4> http:can-get ; session:id rein:test; session:secret "judy-passwd" . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. { log:semantics t3:F . } log:implies {t3:F a t2:TroopStuff . } . { :L a rdf:List . } log:implies {:L :L . } . { eng:RF a rein:RequestFormula; log:includes { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . } log:implies { [ a rein:Request; rein:access eng:ACCESS; rein:requester eng:WHO; rein:resource eng:RESOURCE ]. } . { :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 <#_g5> . t2:WHO t:member t:w3c . t3:PHOTO a http:photo; log:uri <#_g5> . <#_g5> str:startsWith "http://demo.policyawareweb.org/images/group.jpg" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { eng:RF a rein:RequestFormula; log:includes {eng:WHO eng:PROP eng:VALUE . } . [ a rein:Request; rein:requester eng:WHO ]. } log:implies {eng:WHO eng:PROP eng:VALUE . } . { :A owl:distinctMembers :D . :L :D; rdf:first :X; rdf:rest :R . :Y list:in :R . } log:implies {:X owl:differentFrom :Y . } . { @forSome <#_g6> . t2:WHO session:login t2:amy . t3:PHOTO log:uri <#_g6> . [ rein:requester t2:WHO ]. [ rein:resource t3:PHOTO ]. <#_g6> str:startsWith "http://demo.policyawareweb.org/images/" . } log:implies {t2:WHO http:can-get t3:PHOTO . } . { @forSome <#_g4> . [ a rein:Request; rein:access http:can-get; rein:requester <#_g4>; rein:resource ]. <#_g4> session:id rein:test; session:secret "judy-passwd" . } a rein:RequestFormula . { @forSome <#_g7> . t2:PG log:semantics <#_g7> . 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 <#_g8>, <#_g9> . t2:LOC t:attendee <#_g9> . t2:PG <#_g8>, <#_g9> . [ t:member <#_g8> ]. } . t3:S crypto:md5 t2:TXT . <#_g7> log:includes { @forSome <#_g10> . t2:PG <#_g10> . <#_g10> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g11> . t2:PG log:semantics <#_g11> . 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 <#_g12> . t2:PG <#_g12> . [ t:member <#_g12> ]. }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g11> log:includes { @forSome <#_g13> . t2:PG <#_g13> . <#_g13> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g14> . t2:PG log:semantics <#_g14> . 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 <#_g15> . t2:LOC t:attendee <#_g15> . t2:PG <#_g15> . }, {t2:LOC a t:Jamboree . t2:PHOTO a t:Photo; t:location t2:LOC . } . t3:S crypto:md5 t2:TXT . <#_g14> log:includes { @forSome <#_g16> . t2:PG <#_g16> . <#_g16> session:hexdigest t2:TXT . } . } log:implies {t2:WHO http:can-get t2:PHOTO . } . { @forSome <#_g17>, <#_g18>, <#_g19>, <#_g20>, <#_g21>, <#_g22>, <#_g23>, <#_g24>, <#_g25>, <#_g26>, <#_g27> . a t:Photo; t:location t2:SepJamboree . a t:Photo; t:location t2:AnnualMeeting . a t:Photo; t:location t2:AnnualMeeting . <#_g17>, <#_g18>, <#_g19> . <#_g20>, <#_g21> . <#_g22>, <#_g23> . <#_g24> . <#_g25> . <#_g26>, <#_g27> . t2:AnnualMeeting a t:Meeting; t:attendee <#_g18>, <#_g21>, <#_g27>; t:troop t2:troop42 . t2:SepJamboree a t:Jamboree; t:attendee <#_g19>, <#_g23>, <#_g24>, <#_g25>; t:troop t2:troop42 . t2:troop42 a t:Troop; t:member <#_g17>, <#_g20>, <#_g22>, <#_g26> . } a t2:TroopStuff . } log:includes { @forSome bfi:_g_L16C21, bfi:_g_L16C99 . bfi:_g_L16C21 a rein:Request; rein:access eng:ACCESS; rein:requester bfi:_g_L16C99; rein:resource eng:RESOURCE . bfi:_g_L16C99 eng:ACCESS eng:RESOURCE . } . } .