F1_F3.clj

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


{:name        "DDE base"
 :description "DDE"
 :assumptions {
               I2
               (Ought! I now situation (and (not (exists [?t] (HoldsAt (dead P1) ?t)))
                                            (not (exists [?t] (HoldsAt (dead P1) ?t)))) )

               I3
               (Knows! I now situation)

               I4
               (Believes! I now (Ought! I now situation (and (not (exists [?t] (HoldsAt (dead P1) ?t)))
                                            (not (exists [?t] (HoldsAt (dead P1) ?t)))) ))}

 :goal        (Intends! I now (and (not (exists [?t] (HoldsAt (dead P1) ?t)))
                                            (not (exists [?t] (HoldsAt (dead P1) ?t)))))}

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



{:name        "DDE 3a 1"
 :description "DDE"
 :assumptions {
               I2
               (Ought! I now situation (and (not (exists [?t] (HoldsAt (dead P1) ?t)))
                                            (not (exists [?t] (HoldsAt (dead P2) ?t)))) )

               I3
               (Knows! I now situation)

               I4
               (Believes! I now (Ought! I now situation (and (not (exists [?t] (HoldsAt (dead P1) ?t)))
                                                             (not (exists [?t] (HoldsAt (dead P2) ?t)))) ))}

 :goal        (Intends! I now (not (HoldsAt (dead P1) 5)))}

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

{:name        "DDE 3a 2"
 :description "DDE"
 :assumptions {
               I2
               (Ought! I now situation (and (not (exists [?t] (HoldsAt (dead P1) ?t)))
                                            (not (exists [?t] (HoldsAt (dead P2) ?t)))) )

               I3
               (Knows! I now situation)

               I4
               (Believes! I now (Ought! I now situation (and (not (exists [?t] (HoldsAt (dead P1) ?t)))
                                                             (not (exists [?t] (HoldsAt (dead P2) ?t)))) ))}

 :goal        (Intends! I now (not (HoldsAt (dead P2) 6)))}

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

{:name "De Se condition"
 :description ""
 :assumptions {1 (Knows! I now (forall [?x] (if (Agent ?x) (or (= ?x I) (= ?x P1) (= ?x P2) (= ?x P3)))))
               2 (Knows! I now (= 1 (nu alpha I P1 now)))
               3 (Knows! I now (= 1 (nu alpha I P2 now)))
               4 (Knows! I now (= 1 (nu alpha I P3 now)))
               5 (Knows! I now (= (- 1) (nu alpha I I now)))
               6 (Knows! I now (= alpha (Drop (self I) track1 3)))
               7 (Knows! I now (forall [a b] (if (= (self a) (self b)) (= a b))))
               8 (Knows! I now (forall [a] (= a (self a))))
               9 (Knows! I now (and (not (= P1 P2)) (not (= P1 P3)) (not (= P1 I)) (not (= P2 P3)) (not (= P2 I)) (not (= P3 I))))
               10 (Knows! I now (and (>> 1 0) (<< (- 1)  0)))
               }
 :goal (Knows! I now (and (<< (nu (Drop (self I) track1 3) I I now) 0)
                          (forall [?agent] (if (Agent ?agent) (if (not (= ?agent (self I))) (>> (nu (Drop (self I) track1 3) I ?agent now) 0)))))  )}