(=>
(and
(issuedBy ?TICKET ?AGENT)
(instance ?TICKET Ticket)
(possesses ?CUST ?TICKET))
(confersNorm ?AGENT Permission
(exists (?T)
(holdsDuring ?T
(exists (?P)
(and
(instance ?P Process)
(agent ?P ?AGENT)
(experiencer ?P ?CUST))))))) |
Mid-level-ontology.kif 18156-18168 |
If X is an issued by of Y, Y is an instance of ticket, and Z possesses Y, then X confers norm permission for there exists W such that there exists V such that V is an instance of process, X is an agent of V, and Z experiences V holds during W |
(=>
(and
(instance ?P Passport)
(possesses ?A ?P))
(confersNorm
(exists (?T ?N1 ?N2)
(and
(instance ?T Translocation)
(agent ?T ?A)
(origin ?T ?N1)
(destination ?T ?N2)
(instance ?N1 Nation)
(instance ?N2 Nation)
(not
(equal ?N1 ?N2)))) Permission ?P)) |
Mid-level-ontology.kif 18175-18189 |
If X is an instance of passport and Y possesses X, then All of the following hold: (1) there exist Z, W (2) V such that Z is an instance of translocation (3) Y is an agent of Z (4) Z originates at W (5) Z ends up at V (6) W is an instance of nation (7) V is an instance of nation (8) equal W (9) V confers norm permission for X |
(=>
(and
(instance ?P PassCertificate)
(possesses ?A ?P))
(exists (?L)
(confersNorm
(located ?A ?L) Permission ?P))) |
Mid-level-ontology.kif 18196-18203 |
If X is an instance of pass certificate and Y possesses X, then there exists Z such that Y is located at Z confers norm permission for X |
(=>
(and
(instance ?L DriversLicense)
(possesses ?A ?L))
(confersNorm ?L Permission
(exists (?D ?V)
(and
(instance ?D Driving)
(agent ?D ?A)
(patient ?D ?V)
(instance ?V RoadVehicle))))) |
Mid-level-ontology.kif 18500-18511 |
If X is an instance of drivers license and Y possesses X, then X confers norm permission for there exist Z, W such that Z is an instance of driving, Y is an agent of Z, W is a patient of Z, and W is an instance of road vehicle |
(=>
(and
(instance ?B Bequeathing)
(agent ?B ?P)
(destination ?B ?H)
(objectTransferred ?B ?PROP))
(exists (?D)
(and
(instance ?D Death)
(experiencer ?D ?P)
(earlier
(WhenFn ?D)
(WhenFn ?B))
(holdsDuring
(ImmediatePastFn
(WhenFn ?D))
(possesses ?P ?PROP))
(confersNorm
(possesses ?H ?PROP) Permission ?P)))) |
Mid-level-ontology.kif 20601-20617 |
If X is an instance of bequeathing, Y is an agent of X, X ends up at Z, and the object transferred in X is W, then there exists V such that V is an instance of death, Y experiences V, the time of existence of V happens earlier than the time of existence of X, Y possesses W holds during immediately before the time of existence of V, and Z possesses W confers norm permission for Y |
(=>
(and
(instance ?S SeizingProperty)
(destination ?S ?A)
(origin ?S ?V)
(instance ?V CognitiveAgent))
(and
(instance ?A Government)
(not
(confersNorm ?V Permission
(destination ?S ?A))))) |
Mid-level-ontology.kif 20623-20634 |
If X is an instance of seizing property, X ends up at Y, X originates at Z, and Z is an instance of cognitive agent, then Y is an instance of government and Z doesn't confers norm permission for X doesn't end up at Y |
(=>
(and
(instance ?POLICY PetsAllowedPolicy)
(policyLocationCoverage ?POLICY ?LOC)
(policyOwner ?AGENT ?POLICY))
(confersNorm ?AGENT Permission
(exists (?PET)
(and
(instance ?PET DomesticAnimal)
(located ?PET ?LOC))))) |
Hotel.kif 2579-2588 |
If X is an instance of pets allowed, X covers Y, and Z enacts policy X, then Z confers norm permission for there exists W such that W is an instance of domestic animal and W is located at Y |
(=>
(and
(instance ?POLICY SmokingAllowedPolicy)
(policyLocationCoverage ?POLICY ?LOC)
(policyOwner ?AGENT ?POLICY))
(confersNorm ?AGENT Permission
(exists (?SMOKE)
(and
(instance ?SMOKE Smoking)
(located ?SMOKE ?LOC))))) |
Hotel.kif 2628-2637 |
If X is an instance of smoking allowed policy, X covers Y, and Z enacts policy X, then Z confers norm permission for there exists W such that W is an instance of smoking and W is located at Y |
(=>
(confersNorm ?E Permission ?F)
(not
(confersNorm ?E Prohibition ?F))) |
Law.kif 311-314 |
If X confers norm permission for Y, then X doesn't confers norm prohibition for Y |
(=>
(confersNorm ?E Prohibition ?F)
(confersNorm ?E Permission
(not ?F))) |
Law.kif 316-318 |
If X confers norm prohibition for Y, then X confers norm permission for Y |
(=>
(confersNorm ?E Obligation ?F)
(confersNorm ?E Permission ?F)) |
Law.kif 320-322 |
If X confers norm obligation for Y, then X confers norm permission for Y |
(=>
(deprivesNorm ?E Prohibition ?F)
(confersNorm ?E Permission ?F)) |
Law.kif 332-334 |
If X deprives norm prohibition for Y, then X confers norm permission for Y |
(=>
(and
(instance ?W Transitway)
(attribute ?W BiDirectionalTraffic))
(exists (?P)
(and
(instance ?P Policy)
(confersNorm
(exists (?T1 ?A ?B)
(and
(instance ?T1 Transportation)
(path ?T1 ?W)
(instance ?A GeographicArea)
(origin ?T1 ?A)
(instance ?B GeographicArea)
(destination ?T1 ?B)
(holdsDuring
(WhenFn ?T1)
(exists (?T2)
(and
(instance ?T2 Transportation)
(path ?T2 ?W)
(origin ?T1 ?B)
(destination ?T1 ?A)
(not
(equal ?T1 ?T2))))))) Permission ?P)))) |
Transportation.kif 3785-3809 |
If X is an instance of transitway and bidirectional traffic is an attribute of X, then All of the following hold: (1) there exists Y such that Y is an instance of policy (2) there exist Z, W (3) V such that Z is an instance of transportation (4) X is path along which Z occurs (5) W is an instance of geographic area (6) Z originates at W (7) V is an instance of geographic area (8) Z ends up at V (9) there exists U such that U is an instance of transportation (10) X is path along which U occurs (11) Z originates at V (12) Z ends up at W (13) equal Z (14) U holds during the time of existence of Z confers norm permission for Y |
(=>
(and
(instance ?W Transitway)
(attribute ?W UniDirectionalTraffic))
(exists (?P)
(and
(instance ?P Policy)
(confersNorm
(exists (?T1 ?A ?B)
(and
(instance ?T1 Transportation)
(path ?T1 ?W)
(instance ?A GeographicArea)
(origin ?T1 ?A)
(instance ?B GeographicArea)
(destination ?T1 ?B)
(holdsDuring
(WhenFn ?T1)
(exists (?T2)
(and
(instance ?T2 Transportation)
(path ?T2 ?W)
(origin ?T1 ?B)
(destination ?T1 ?A)
(not
(equal ?T1 ?T2))))))) Prohibition ?P)))) |
Transportation.kif 3818-3842 |
If X is an instance of transitway and unidirectional traffic is an attribute of X, then All of the following hold: (1) there exists Y such that Y is an instance of policy (2) there exist Z, W (3) V such that Z is an instance of transportation (4) X is path along which Z occurs (5) W is an instance of geographic area (6) Z originates at W (7) V is an instance of geographic area (8) Z ends up at V (9) there exists U such that U is an instance of transportation (10) X is path along which U occurs (11) Z originates at V (12) Z ends up at W (13) equal Z (14) U holds during the time of existence of Z confers norm prohibition for Y |
(=>
(and
(instance ?TA TravelApproval)
(possesses ?EMPLOYEE ?TA))
(confersNorm ?TA Permission
(exists (?BT)
(and
(instance ?BT BusinessTrip)
(patient ?TA ?BT)
(agent ?BT ?EMPLOYEE))))) |
TravelPolicies.kif 565-574 |
If X is an instance of TravelApproval and Y possesses X, then X confers norm permission for there exists Z such that Z is an instance of BusinessTrip, Z is a patient of X, and Y is an agent of Z |
(=>
(and
(instance ?T Ticket)
(possesses ?T ?CUST)
(issuedBy ?T ?ORG)
(attribute ?ORG AmusementGamblingAndRecreationIndustries)
(located ?ORG ?LOC))
(confersNorm ?ORG Permission
(exists (?REC)
(and
(instance ?REC RecreationOrExercise)
(experiencer ?REC ?CUST)
(eventLocated ?REC ?LOC))))) |
naics.kif 11453-11465 |
If X is an instance of ticket, X possesses Y, Z is an issued by of X, amusement gambling and recreation industries is an attribute of Z, and Z is located at W, then Z confers norm permission for there exists V such that V is an instance of recreation or exercise, Y experiences V, and V is located at W |