2.2. Nondeterministic Shooting

In the Yale Shooting Problem (Section 2.1) the person is assumed to become dead any time he is shot with a loaded gun. Let us relax this assumption now and take into account the possibility that the assailant can miss. After shooting, the fluent alive can change its value from t to f, as before, but it can also keep the value t. In terms of the transition system, this modification means that one more edge is added to the graph. The edge starts at the vertex

alive=tloaded=t,

is labeled

load=fshoot=t

and goes to the vertex

alive=tloaded=f.

The modified transition system is nondeterministic, in the sense that it contains a pair of different edges that start at the same vertex and have the same label.

This change can be reflected in the language of CCalc by replacing the proposition

shoot causes -alive
in the original formalization of the shooting domain with
shoot may cause -alive.
may cause propositions, like causes propositions, can be conditional (that is, followed by if...).

Exercise 2.6. In the modified domain, the assumptions of the Yale Shooting Problem (the person is initially alive, then the gun is loaded, then he waits, and then he is shot) entails neither that the fluent alive is true in the final state nor that it is false. Verify this assertion using CCalc.

In the examples discussed so far in this tutorial we have seen CCalc propositions of three kinds: causes propositions, nonexecutable propositions and may cause propositions. The reader familiar with action language C+ knows that all these expressions are actually abbreviations for special kinds of "fluent dynamic laws" (see NMCT, Appendix B). The general form of a fluent dynamic law is

caused F if G after H

where F, G and H are formulas; F and G are not allowed to contain symbols for actions. In particular,

A causes F if G

is shorthand for

caused F if true after A & G

("there is a cause for F to hold after the execution of action A in a state satisfying condition G"). The proposition

nonexecutable A if F

is shorthand for

caused false if true after A & F.

The proposition

A may cause F if G

is expanded into

caused F if F after A & G.

-- if F holds after the execution of action A in a state satisfying condition G then there is a cause for this. In other words, F is a possible outcome of A; F is allowed to become true after executing A, but this outcome is not required.

The reader familiar with C+ knows also that there is no syntactic category of "inertial fluents" in that language. The syntax of C+ distinguishes between two kinds of fluent constants -- simple and statically determined. If C is a simple fluent constant then

inertial C

is shorthand for the set of fluent dynamic laws

caused C=V if C=V after C=V

for all possible values V of C: if C has now the same value V that it had before then there is a cause for this. (Intuitively, inertia is the cause; this is how fluent dynamic laws solve the frame problem.) These fluent dynamic laws are similar to those obtained by expanding may cause propositions: they also have the form caused F if F after ... .

In accordance with this understanding of inertial fluents, an inertialFluent declaration in CCalc code is an abbreviation for a simpleFluent declaration combined with an inertial proposition. For instance, the declaration

:- constants
 c :: inertialFluent(0..n).
has the same meaning as
:- constants
 c :: simpleFluent(0..n).

inertial c.
Forward to Section 2.3: Counting Bullets
Back to Section 2.1: Basic Formulation
Up to the Table of Contents