;Carrying a PDA example ;State constraint and non-trivial KT7 axiom ;The example run correctly, with 1 model output ;There are certain things to notice, except the KT7 axiom: ;how to model the functional constraint that each object is in one room, ;how to reduce unnecessary models etc load foundations/Root.e load foundations/EC.e sort object sort agent: object sort room object PDA agent Teo room ISLLab, CARVLab ;----------------------------------------------------------------- fluent InRoom(object,room) fluent Knows_InRoom(object,room) fluent Knows_NotInRoom(object,room) ;Kw Definition fluent Kw_InRoom(object,room) noninertial Kw_InRoom [object,room,time] HoldsAt(Kw_InRoom(object,room),time) <-> HoldsAt(Knows_InRoom(object,room),time) | HoldsAt(Knows_NotInRoom(object,room),time). fluent KP_InRoom(object,room) fluent KP_NotInRoom(object,room) ;Knowledge Axiom T [object,room,time] HoldsAt(Knows_InRoom(object,room),time) -> HoldsAt(InRoom(object,room),time). [object,room,time] HoldsAt(Knows_NotInRoom(object,room),time) -> !HoldsAt(InRoom(object,room),time). ;KT1 noninertial Knows_InRoom noninertial Knows_NotInRoom ;KT2.1 [object,room,time] HoldsAt(KP_InRoom(object,room),time) -> HoldsAt(Knows_InRoom(object,room),time). ;KT2.2 [object,room,time] HoldsAt(KP_NotInRoom(object,room),time) -> HoldsAt(Knows_NotInRoom(object,room),time). ;KT7 ;Pay special attention! [object,room,time] !HoldsAt(KP_InRoom(object,room),time) & !HoldsAt(KP_NotInRoom(object,room),time) & ([agent] ; Due to the state constraint ( HoldsAt(Knows_NotHolding(agent,object),time)| HoldsAt(Knows_NotInRoom(agent,room),time) ) | ( !HoldsAt(Kw_Holding(agent,object),time)| !HoldsAt(Kw_InRoom(agent,room),time) ) )& !({room1} room1!=room & HoldsAt(Knows_InRoom(object,room1),time) )-> ;Due to the only-one-room constraint !HoldsAt(Kw_InRoom(object,room),time). ;----------------------------------------------------------------- ;Only-one-room Constraint ;Any object can only be in one room ; ;This is necessary, regardless of whether we use knowledge or not [object,room1,room2,time] HoldsAt(InRoom(object,room1),time) & HoldsAt(InRoom(object,room2),time) -> room1=room2. ;In order to reflect the knowledge the agent has about the previous ;contraint the following axiom is not adequate (in particular it does ;nothing more than the previous axiom) ;[object,room1,room2,time] ;HoldsAt(Knows_InRoom(object,room1),time) & ;HoldsAt(Knows_InRoom(object,room2),time) -> ;room1=room2. ;Therefore, we must represent this knowledge as shown in the following ;constraint ;NOTE that the KT7 axiom has been extended accordingly [object,room1,room2,time] HoldsAt(Knows_InRoom(object,room1),time) & room1!=room2-> HoldsAt(Knows_NotInRoom(object,room2),time). ;----------------------------------------------------------------- event Walk(agent,room,room) [agent,room1,room2,time] Initiates(Walk(agent,room1,room2),InRoom(agent,room2),time). ;KT3.1 [agent,room1,room2,time] Happens(Walk(agent,room1,room2),time) -> Initiates(Walk(agent,room1,room2),KP_InRoom(agent,room2),time). ;KT3.2 [agent,room1,room2,time] Happens(Walk(agent,room1,room2),time) -> Terminates(Walk(agent,room1,room2),KP_NotInRoom(agent,room2),time). ;------------------------------------------------------------------- [agent,room1,room2,time] room1!=room2 -> Terminates(Walk(agent,room1,room2),InRoom(agent,room1),time). ;KT3.3 [agent,room1,room2,time] room1!=room2 & Happens(Walk(agent,room1,room2),time)-> Initiates(Walk(agent,room1,room2),KP_NotInRoom(agent,room1),time). ;KT3.4 [agent,room1,room2,time] room1!=room2 & Happens(Walk(agent,room1,room2),time)-> Terminates(Walk(agent,room1,room2),KP_InRoom(agent,room1),time). ;----------------------------------------------------------------- fluent Holding(agent,object) fluent Knows_Holding(agent,object) fluent Knows_NotHolding(agent,object) ;Kw Definition fluent Kw_Holding(agent,object) noninertial Kw_Holding [agent,object,time] HoldsAt(Kw_Holding(agent,object),time) <-> HoldsAt(Knows_Holding(agent,object),time) | HoldsAt(Knows_NotHolding(agent,object),time). fluent KP_Holding(agent,object) fluent KP_NotHolding(agent,object) ;Knowledge Axiom K [agent,object,time] HoldsAt(Knows_Holding(agent,object),time) -> HoldsAt(Holding(agent,object),time). [agent,object,time] HoldsAt(Knows_NotHolding(agent,object),time) -> !HoldsAt(Holding(agent,object),time). ;KT1 noninertial Knows_Holding noninertial Knows_NotHolding ;KT2.1 [agent,object,time] HoldsAt(KP_Holding(agent,object),time) -> HoldsAt(Knows_Holding(agent,object),time). ;KT2.2 [agent,object,time] HoldsAt(KP_NotHolding(agent,object),time) -> HoldsAt(Knows_NotHolding(agent,object),time). ;KT7 ;The usual axiom [agent,object,time] !HoldsAt(KP_Holding(agent,object),time) & !HoldsAt(KP_NotHolding(agent,object),time) -> !HoldsAt(Kw_Holding(agent,object),time). ;------------------------------------------------------------------ event PickUp(agent,object) [agent,object,room,time] HoldsAt(InRoom(agent,room),time) & HoldsAt(InRoom(object,room),time) -> Initiates(PickUp(agent,object),Holding(agent,object),time). ;KT3.1 [agent,object,room,time] HoldsAt(Knows_InRoom(agent,room),time) & HoldsAt(Knows_InRoom(object,room),time) & Happens(PickUp(agent,object),time) -> Initiates(PickUp(agent,object),KP_Holding(agent,object),time). ;KT3.2 [agent,object,room,time] HoldsAt(Knows_InRoom(agent,room),time) & HoldsAt(Knows_InRoom(object,room),time) & Happens(PickUp(agent,object),time) -> Terminates(PickUp(agent,object),KP_NotHolding(agent,object),time). ;KT5.1 ;Not needed for the simple executions ;------------------------------------------------------------------ [agent,object,room,time] ;HoldsAt(InRoom(agent,room),time) & ;This does not work, there must be some bug of decreasoner ;HoldsAt(InRoom(object,room),time) -> ;See the comments in the CarryingABook2 example Releases(PickUp(agent,object),InRoom(object,room),time). ;KT5.3 [agent,object,room,time] ;!HoldsAt(Knows_NotInRoom(agent,room),time) & ;!HoldsAt(Knows_NotInRoom(object,room),time) & Happens(PickUp(agent,object),time) -> Terminates(PickUp(agent,object),KP_InRoom(object,room),time). [agent,object,room,time] ;!HoldsAt(Knows_NotInRoom(agent,room),time) & ;!HoldsAt(Knows_NotInRoom(object,room),time) & Happens(PickUp(agent,object),time) -> Terminates(PickUp(agent,object),KP_NotInRoom(object,room),time). ;------------------------------------------------------------------ ;State constraint [agent,object,room,time] HoldsAt(Holding(agent,object),time) & HoldsAt(InRoom(agent,room),time) -> HoldsAt(InRoom(object,room),time). ;This is the result of the distribution axiom (K). ;It is explicitly stated [agent,object,room,time] HoldsAt(Knows_Holding(agent,object),time) & HoldsAt(Knows_InRoom(agent,room),time) -> HoldsAt(Knows_InRoom(object,room),time). ;------------------------------------------------------------------ ; Observations HoldsAt(KP_InRoom(Teo,ISLLab),0). HoldsAt(KP_InRoom(PDA,ISLLab),0). ;Voithitiko gia na meiwnontai ta montela. Oxi aparaithto gia thn ektelesh ;To antistoixo gia to Knows, pou einai k to shmantiko, to exw pio panw [object,room1,room2,time] HoldsAt(KP_InRoom(object,room1),time) & room1!=room2 -> HoldsAt(KP_NotInRoom(object,room2),time). !HoldsAt(Holding(Teo,PDA),0). HoldsAt(KP_NotHolding(Teo,PDA),0). [agent,time] !HoldsAt(Holding(agent,agent),time). [agent,time] HoldsAt(KP_NotHolding(agent,agent),time). [agent,time] HoldsAt(Knows_NotHolding(agent,agent),time). ;------------------------------------------------------------------- ;Narrative Happens(PickUp(Teo,PDA),0). Happens(Walk(Teo,ISLLab,CARVLab),1). completion Happens range time 0 2 range offset 1 1 ; End of file.