An example plan proof

In ANDI-Land version 1.2 the game character Djak is on a personal mission to obtain some lumber for himself. The plan that he carries out was generated using the automated theorem prover ANDI and is shown below.

Action specifications

The input to the theorem prover is the agent's background knowledge about actions and their effects, expressed in Temporal Action Logic:

(= (value t-now (tmoney-wealth agent-self)) 5)
(= (value t-now (tmoney-price object-axe)) 3)
(= (value t-now (location agent-self)) (loc 1 -1))
;; Walking somewhere
(-> (and 
     ;; We must know where the destination is
     (knows ?agent (start ?i) (= ?loc-to ?loc-to-ident))
     (knows ?agent (start ?i) (standard-id ?loc-to-ident))
     ;; Then we can walk there
     (occurs ?agent ?i (walk ?loc-to-ident)))
    (and (= (value (finish ?i) (location ?agent)) ?loc-to)
         (-> (not (occlude ?i2 (location ?agent))) (not-overlap ?i2 ?i))))
;; Chopping down trees
(-> (and 
     ;; We need to own an axe
     (= (value (start ?i) (agent-owner object-axe)) agent-self)
     ;; We must be at the place of the (only) tree
     (= (value (start ?i) (location ?agent)) (loc 1 -1))
     ;; Then we can chop it down.
     (occurs ?agent ?i chop))
    (= (value (finish ?i) (agent-owner object-lumber)) ?agent))
;; Buying objects
(-> (and 
     ;; We must know who the seller is.
     (knows ?agent-buyer (start ?i) (= (value (start ?i) (agent-owner ?object)) ?agent-seller-ident))
     (knows ?agent-buyer (start ?i) (standard-id ?agent-seller-ident))
     ;; We must be at the same place as the seller.
     (= (value (start ?i) (location ?agent-buyer)) (value (start ?i) (location ?agent-seller-ident)))
     ;(not (occlude ?i (location ?agent-buyer))) ; Not needed under the seriality assumption
     ;; We must know the price of the object.
     (= (value (start ?i) (tmoney-price ?object)) ?tmoney-price-id)
     ;; We must know our own wealth.
     (= (value (start ?i) (tmoney-wealth ?agent-buyer)) ?tmoney-wealth-id)
     ;; We must check that we can afford the object.
     (>= ?tmoney-wealth-id ?tmoney-price-id)
     ;; Then we can buy it.
     (occurs ?agent-buyer ?i (buy ?object ?agent-seller-ident)))
    (and (= (value (finish ?i) (agent-owner ?object)) ?agent-buyer)
         (= (value (finish ?i) (tmoney-wealth ?agent-buyer))
            (- (value (start ?i) (tmoney-wealth ?agent-buyer))
               (value (start ?i) (tmoney-price ?object))))
         (= (value (finish ?i) (tmoney-wealth ?agent-seller-ident)) 
            (+ (value (start ?i) (tmoney-wealth ?agent-seller-ident)) 
               (value (start ?i) (tmoney-price ?object))))
         (-> (not (occlude ?i2 (agent-owner ?object))) (not-overlap ?i2 ?i))
         (-> (not (occlude ?i3 (tmoney-wealth ?agent-buyer))) (not-overlap ?i3 ?i))
         (-> (not (occlude ?i4 (tmoney-wealth ?agent-seller-ident))) (not-overlap ?i4 ?i))))
;; Asking questions
(-> (and
     ;; We must know what the question is
     (knows ?agent (start ?i) (= ?p-fluent ?p-fluent-ident))
     (knows ?agent (start ?i) (standard-id ?p-fluent-ident))                         
     ;; Then we can ask it
     (occurs ?agent ?i (ask-value ?agent-knower ?p-fluent-ident)))
    (and (knows ?agent (finish ?i) (= (value (finish ?i) ?p-fluent) $p-value))
         (knows ?agent (finish ?i) (standard-id $p-value))))

Plan proof

The goal is to have lumber, as expressed by the formula:

(= (value ?t (agent-owner object-lumber)) agent-self)

The output of the theorem prover is a natural deduction style proof. It is quite large, at about 150 steps, and is best shown by this text file viewed in an editor with line breaks turned off. Notice the extensive use of the natural deduction assumption mechanism indicated by vertical lines in the left margin.

Resulting plan

Finally, the resulting plan is extracted from the proof by looking at what actions were assumed to occur. It is displayed below with vertical lines indicating time intervals and explanations for the intervals in the right margin:

o o o           ((start $i-1851) (start $i-2039) t-now)
| |<-------------(not (occlude $i-2039 (tmoney-wealth agent-self)))
|<|---------------(not (occlude $i-1851 (tmoney-price object-axe)))
| |   o            ((start $i-386))
| |   |<------------(occurs agent-self $i-386 (ask-value ?agent-knower-389 (agent-owner object-axe)))
| |   o o            ((finish $i-386) (start $i-391))
| |     |<------------(knows agent-self (start $i-202) (not (occlude $i-391 (agent-owner object-axe))))
| |     | o            ((start $i-974))
| |     | |<------------(occurs agent-self $i-974 (ask-value ?agent-knower-977 (location $p-value-390)))
| |     | o o            ((finish $i-974) (start $i-979))
| |     |   |<------------(knows agent-self (start $i-774) (not (occlude $i-979 (location $p-value-390))))
| |     |   | o            ((start $i-774))
| |     |   | |<------------(occurs agent-self $i-774 (walk $p-value-978))
| |     |   | o o            ((finish $i-774) (start $i-778))
| |     |   |   |<------------(not (occlude $i-778 (location agent-self)))
o o     o   o   o o           ((finish $i-1851) (finish $i-2039) (start $i-202)
                  |            (finish $i-391) (finish $i-778) (finish $i-979))
                  |<-----------(occurs agent-self $i-202 (buy object-axe $p-value-390))
                  o o           ((finish $i-202) (start $i-210))
                    |<----------(not (occlude $i-210 (agent-owner object-axe)))
                    | o         ((start $i-2281))
                    | |<--------(occurs agent-self $i-2281 (walk (loc 1 -1)))
                    | o o       ((finish $i-2281) (start $i-2285))
                    |   |<------(not (occlude $i-2285 (location agent-self)))
                    o   o o     ((finish $i-210) (finish $i-2285) (start $i-29))
                          |<----(occurs agent-self $i-29 chop)
                          o o   ((finish $i-29) (start $i-31))
                            |<--(not (occlude $i-31 (agent-owner object-lumber)))
                            o o ((finish $i-31) $t)