Actions can be combined into strategies. The simplest combination is a finite sequence of actions. We shall combine actions as though they were ALGOL statements, that is, procedure calls. Thus, the sequence of actions, (`move the box under the bananas', `climb onto the box', and `reach for the bananas') may be written:
A strategy in general will be an ALGOL-like compound statement containing actions written in the form of procedure calling assignment statements, and conditional go to's. We shall not include any declarations in the program since they can be included in the much larger collection of declarative sentences that determine the effect of the strategy.
Consider for example the strategy that consists of walking 17 blocks south, turning right and then walking till you come to Chestnut Street. This strategy may be written as follows:
In the above program the external actions are represented by procedure calls. Variables to which values are assigned have a purely internal significance (we may even call it mental significance) and so do the statement labels and the go to statements.
For the purpose of applying the mathematical theory of computation we shall write the program differently: namely, each occurrence of an action is to be replaced by an assignment statement Thus the above program becomes
Suppose we wish to show that by carrying out this strategy John can go home provided he is initially at his office. Then according to the methods of Zohar Manna (1968a, 1968b), we may derive from this program together with the initial condition and the final condition at(John,home(John),s), a sentence W of first-order logic. Proving W will show that the procedure terminates in a finite number of steps and that when it terminates s will satisfy at(John, home(John),s).
According to Manna's theory we must prove the following collection of sentences inconsistent for arbitrary interpretations of the predicates q1 and q2 and the particular interpretations of the other functions and predicates in the program:
Therefore the formula that has to be proved may be written
In order to prove this sentence we would have to use the following kinds of facts expressed as sentences or sentence schemas of first-order logic:
1. Facts of geography. The initial street stretches at least 17 blocks to the south, and intersects a street which in turn intersects Chestnut Street a number of blocks to the right; the location of John's home and office.
2. The fact that the fluent will have the value `Chestnut Street' at that point.
3. Facts giving the effects of action expressed as predicates about deducible from sentences about s.
4. An axiom schema of induction that allows us to deduce that the loop of walking 17 blocks will terminate.
5. A fact that says that Chestnut Street is a finite number of blocks to the right after going 17 blocks south. This fact has nothing to do with the possibility of walking. It may also have to be expressed as a sentence schema or even as a sentence of second-order logic.
When we consider making a computer carry out the strategy, we must distinguish the variable s from the other variables in the second form of the program. The other variables are stored in the memory of the computer and the assignments may be executed in the normal way. The variable s represents the state of the world and the computer makes an assignment to it by performing an action. Likewise the fluent requires an action, of observation.