Assume that the person is initially alive. The gun is loaded, then he waits for a while, and then he is shot with the gun. What can we say, given these assumptions, about the values of the fluents involved -- alive and loaded -- at various points in time?
The description of the domain above does not say whether the load action is considered executable when the gun is already loaded. Let's decide that the answer is yes: when the gun is loaded, that action can be executed but will have no effect.
Note that the assumptions of the Yale Shooting Problem do not determine the initial state completely: the fluent loaded can be either true or false in the initial state. But once the initial value of this fluent is selected, all future changes in the values of fluents are uniquely defined.
The shooting domain can be described in the language of CCalc by the following declarations and propositions:
:- constants loaded, alive :: inertialFluent; load, shoot :: exogenousAction. load causes loaded. shoot causes -alive. shoot causes -loaded. nonexecutable shoot if -loaded. nonexecutable load & shoot.The declarations of the two fluent constants are combined here into one, and so are the declarations of the two action constants. The last line expresses the assumption (implicit in the informal description of the domain) that the two actions cannot be executed concurrently.
The corresponding transition system has 4 vertices:
Its edges are labeled by 3 events:
Exercise 2.1. How many edges do you think this transition system has? Verify your answer using CCalc.
Expressing the assumptions about the sequence of events in the Yale Shooting Problem (load, then wait, then shoot) by a CCalc query can be made easier by introducing the macro
:- macros wait -> -load & -shoot.(to wait means not to load and not to shoot). Then we can write:
:- query maxstep:: 3; 0: alive; 0: load; 1: wait; 2: shoot.Exercise 2.2. Run CCalc to verify that this query has exactly two answers, as expected.
The examination of the answers to the query above shows that, in each of them, the fluent alive is false at step 3. In this sense, the assumptions of the Yale Shooting Problem entail the conclusion that this fluent eventually becomes false. An alternative way to verify this conclusion is to instruct CCalc to answer the query in which this conclusion is required not to hold:
:- query maxstep:: 3; 0: alive; 0: load; 1: wait; 2: shoot; 3: alive.CCalc will determine that these assumptions are inconsistent.
Exercise 2.3. Use CCalc to check that the assumption 0:-alive entails 10:-alive.
Exercise 2.4. Modify the original formalization of the Yale Shooting Problem to reflect the assumption that the shoot action is executable even when the gun is not loaded, but it does not affect the fluent alive in this case. How does this modification affect the number of edges of the transition system, in your opinion? Verify your answer using CCalc.
Exercise 2.5. In the modification of the Yale Shooting Problem introduced by Andrew Baker in 1991 (Artificial Intelligence, Vol. 49) and known as the Stanford Murder Mystery, the person is alive initially, but is found to be dead after a wait followed by shooting. Using CCalc, check under these assumptions that the gun was initially loaded.
Instead of defining wait as an abbreviation, we can treat this symbol as a third action constant. The assumption that no two actions out of 3 can be executed concurrently requires 3 propositions:
nonexecutable load & shoot. nonexecutable load & wait. nonexecutable shoot & wait.The language of CCalc allows us to express the no concurrency assumption more concisely, simply by writing
noconcurrency.
Forward to Section 2.2: Nondeterministic Shooting Back to Section 1.5: Setting Paramemeters Up to the Table of Contents