;; File: dungeon.txt
;; Date: 11/2/93
;; Description: Assignment on interval temporal logic

INTRODUCTION

Ralph sat down on the couch and picked up the TV's remote. He pressed
the CHANNEL UP button, but the TV remained in its quiet slumber. He
pressed it again a couple times -- still nothing.  Frustrated, he
stood up, pushed the POWER button a couple times (thus turning the TV
on, then off again), and threw away the remote.  "Hm... Well, I could
always go to the CIT and enjoy a few hours of LISP programming
instead," he thought.

Apparently, Ralph has a bit of a problem with temporal reasoning. He
should have pushed the POWER button first, before trying to change
the channel -- one can change the channel only if the TV is on.
Oh well, luckily for Ralph, he did not make the mistake of wasting
his time watching TV. Instead, he'll be spending numerous hours
enjoying the comfy environments of the Sunlab and LISP.

BACKGROUND INFORMATION

The purpose of this assignment is to acquaint you with interval
temporal logic. In addition to writing axioms in the interval logic,
you will be working with a program that, given initial
conditions, initial events, and causal rules, allows you to predict
the future. 

The initial conditions are specified as a list of propositions that
describe what is true at the initial time. Using our story as an example,
initially, Ralph is not on the couch, Ralph does not have the TV
remote, and the TV is not on. This can be represented as a list of
propositions:

     ( (not (on Ralph couch))
       (not (has Ralph remote))
       (not (turned-on TV)) )

The initial events are specified as a list of things that will happen
at certain points in time. The interval temporal logic program doesn't
associate any particular units with time; instead, it maps our normal
time units (days, hours, minutes, seconds, etc.) onto the set of
integers, with time 0 indicating the starting time, and time > 0
indicating time points after the starting time. For our example, Ralph
sits on the couch at time 1, grabs the remote at time, and pushes the
CHANNEL UP button at time 3. This can be expressed as the following
list of initial events:

     ( ((sit)              1)
       ((grab remote)      2)
       ((push channel-up)  3) )

Finally, the causal rules dictate what happens given that a certain
event occurs with certain conditions true at the time that the event
occurs.  Causal rules have antecedents, a trigger, and consequents.
The antecedents specify the conditions that must hold at the time the
trigger (event) occurs in order for the consequents to become
realized. The consequents be either changes in conditions or more
events. Here are some of the causal rules for our story:

       (pcause (and) (sit)         (on Ralph couch)         0)
       (pcause (and) (stand)       (not (on Ralph couch))   0)
       (pcause (and) (grab remote) (has Ralph remote)       0)
       (pcause (and) (drop remote) (not (has Ralph remote)) 0) 

Although the list is not yet complete, let us take a little time to
explain some things. First of all, this is a list of causal rules.
As stated, causal rules can result in changes in conditions or more
events. The above causal rules are meant to effect changes in
conditions and are preceded by 'pcause to tell our temporal logic
program of this fact. PCAUSE rules have the following format:

     (PCAUSE <antecedents> <trigger> <new fluent> <delay>)

Take, for example, the first PCAUSE rule. The trigger is the event
(sit). Since sitting always results in Ralph sitting on the couch (we
are simplifying quite a bit here), we have no conditions that must
be satisfied. However, since our temporal logic program expects
antecedents, we give an empty list of conjuncts (nil will not work
here). The new fluent (recall a fluent is a description which is
either true or false at any given time) is, as expected,
(on Ralph couch). The delay is 0, indicating that the new fluent takes
effect immediately, not, say, 10 time units later. Note, the next
PCAUSE rule (the one for stand) results in the negation of
(on Ralph couch) becoming true (i.e. (not (on Ralph couch)) becomes
true). We do not have to specify that (on Ralph couch) is no longer
true; the program will figure this out.

We could specify that more than one new fluent should be realized
by including them in a conjunction. Say, for example, when
Ralph sits, he sits on the couch immediately (of course), feels
relaxed one time unit later, and has difficulty thinking immediately.
The causal rule would be:

     (pcause (and) (sit) (and (on Ralph couch) 0
                              (relaxed Ralph) 1
                              (zombie Ralph) 0) )

Okay. Now let's continue with the other causal rules:

     (ecause (turned-on TV) (push channel-up) (change channel))

ECAUSE rules specify that events occur. Their format is:

     (ECAUSE <antecedent> <trigger> <new event> <delay>)

Note that we do not have a conjunction in the above 
ECAUSE rule. This is because we have only one condition which
must be satisfied. If, say, we wanted to add the condition that
the remote was working, the ECAUSE rule would be:

     (ecause (and (turned-on TV) 
                  (working remote))
             (push channel-up) 
             (change channel))

<new event> is very similar to the <new fluent> of a PCAUSE rule
except that it specifies an event that will happen at a certain
point in time (as specified by <delay>). As with the PCAUSE rule,
we could specify multiple new events with a conjunction in
the same way we specified multiple new fluents.

Although our list of causal rules is still incomplete, you should
have an idea of how they are specified and operate.

ASSIGNMENT

For this assignment, you will be playing with the temporal logic
program for a Dungeons-and-Dragons-type scenario. We have
a knight wandering in a castle with the following layout:

               wizard's   castle
               chamber    dungeon
             +---------+----------+
             |         | j        |     k initial location of the knight
             |         +          |     t initial location of the torch
             |               k    |     j initial location of the jewel
             |         +          |     w initial location of the wizard
             |       w |        t |     g initial location of the gold
             +---+ +---+----------+     d initial location of the dragon
             |         |
             |         |
             |         | 
             |         | 
             | g     d | dragon's lair
             +---------+

The fluents you will need to describe a situation are given below.
Note that the temporal logic program knows how to clip the persistence
of all the propositions given below.  In particular, frozen(wizard)
clips ~frozen(wizard) and location(knight,lair) clips
location(knight,dungeon).  Below we have included both the prefix
notation that you would use for specifying axioms in a logical theory
and the Lisp notation that you would use for the temporal logic
program.

    Prefix notation                      Lisp notation

    location(knight,lair)                (location knight lair) 
    location(knight,chamber)             (location knight chamber) 
    location(knight,dungeon)             (location knight dungeon) 
    possess(knight,gold)                 (possess knight gold)         
    possess(knight,torch)                (possess knight torch)         
    possess(knight,jewel)                (possess knight jewel)          
    possess(wizard,jewel)                (possess wizard jewel)          
    enchanted(dragon)                    (enchanted dragon)              
    frozen(wizard)                       (frozen wizard)                
    frozen(knight)                       (frozen knight)                
    alive(knight)                        (alive knight)                 

Events that can trigger change are:

Moving around:

    move(knight,dungeon,chamber)         (move knight dungeon chamber)     
    move(knight,chamber,lair)            (move knight chamber lair)        
    move(knight,lair,chamber)            (move knight lair chamber)        
    move(knight,chamber,dungeon)         (move knight chamber dungeon)     
    enter(knight,dungeon)                (enter knight dungeon)            
    enter(knight,chamber)                (enter knight chamber)            
    enter(knight,lair)                   (enter knight lair)               
                                                                          
Picking things up:                       

    pickup(knight,torch)                 (pickup knight torch)             
    pickup(knight,gold)                  (pickup knight gold)              
    pickup(knight,jewel)                 (pickup knight jewel)             
                                                                          
Miscellaneous actions:                        

    ;; the knight thaws the wizard       
    thaw(knight,wizard)                  (thaw knight wizard)              
    ;; the wizard freezes the knight     
    freeze(wizard,knight)                (freeze wizard knight)            
    ;; dragon toasts the knight          
    toast(dragon,knight)                 (toast dragon knight)             
    ;; knight gives jewel to wizard      
    give(knight,wizard,jewel)            (give knight wizard jewel)        


EXERCISE 1

Write a set of causal rules that capture the following physical laws:

  a. To move from A to B the knight must be alive, not frozen, in A,
     and A must be adjacent to B. If all these conditions are
     satisfied, then the knight will enter B two time units later.
     Entering a place immediately changes the knight's location to
     that place.

  b. If the dragon is not enchanted, whenever the knight enters the
     lair, the dragon will decide to toast the knight one time unit
     later. Should the knight still be in the lair when the dragon
     decides to make toast of him, the knight will die immediately.

  c. The wizard will immediately become unfrozen should the knight
     decide to thaw him. The knight can thaw the wizard only if he
     (the knight) is in the wizard's chamber, possesses the torch,
     and the wizard is frozen. Once thawed, the wizard will decide
     to freeze the knight six time units later, unless the wizard
     possesses the jewel by then. The knight will be immediately
     frozen only if he is in the wizard's chamber when the wizard
     decides to freeze him.

  d. Picking up something immediately results in possessing it. The
     knight can only pick up the torch and/or jewel if he is in the
     dungeon and the gold if he is in the dragon's lair.

  e. The knight can only give away the jewel if he possesses it and
     the receiver is in the same room as he. Giving something away
     immediately results in the receiver becoming the new possessor.
     If the wizard is given the jewel when he is not frozen, the
     wizard will go enchant the dragon (hence the dragon will become
     enchanted) two time units later. (Note: the wizard cannot receive
     things while he is frozen.)


EXERCISE 2

Create a list of ECAUSE and PCAUSE rules that implement the logical rules
you wrote in exercise 1.

EXERCISE 3

You will find a specification of the following initial conditions in
the file scenarios.lisp.

     holds(0,location(knight,dungeon))
     holds(0,location(dragon,lair))
     holds(0,location(wizard,chamber))
     holds(0,location(jewel,dungeon))
     holds(0,location(torch,dungeon))
     holds(0,location(gold,lair))
     holds(0,~(possess(knight,torch)))
     holds(0,~(possess(knight,gold)))
     holds(0,~(possess(knight,jewel)))
     holds(0,~(possess(wizard,jewel)))
     holds(0,~(enchanted(dragon)))
     holds(0,~(frozen(knight)))
     holds(0,frozen(wizard))
     holds(0,alive(knight))

You will also find specifications for the following three 
alternative lists of initial events in scenarios.lisp.

  a. occurs(10,pickup(knight,torch))
     occurs(20,pickup(knight,jewel))
     occurs(30,(move knight,dungeon,chamber))
     occurs(40,thaw(knight,wizard))
     occurs(45,give(knight,wizard,jewel))
     occurs(50,move(knight,chamber,lair))
     occurs(60,pickup(knight,jewel))

  b. occurs(10,pickup(knight,torch))
     occurs(20,move(knight,dungeon,chamber))
     occurs(30,thaw(knight,wizard))
     occurs(40,move(knight,chamber,lair))

  c. occurs(10,move(knight,dungeon,chamber))
     occurs(20,move(knight,chamber,lair))

Run TLS (in tm.lisp) with the above initial conditions, the causal
rules of Exercise 2, and the three different sets of initial events.
Include a copy of the output of each of these three runs.

EXTRA CREDIT
Change the projection code to handle rules with variables.

EXTRA EXTRA CREDIT
Change the projection code to handle rules that constrain propositions
within a single time point.  Your solution will provide a solution to
the ramification problem. Here are some examples of rules that constrain
propositions at a single point. 

     holds(t,alive) -> holds(t,~dead)

     (holds(t,location(x,w)) ^ holds(t,inside(y,x))) -> holds(t,location(y,w))

