State Transition ProblemSample answers

Here is a suggested encoding of the Before and After problem from the Expert list. This has features typical of a large and important class of problems in which we need to reason about a system which changes its state from one time step to the next. They vary quite a lot in detail, but some of the techniques for encoding them are sufficiently general to be worth noting.

There are states, which here are simply allocations of numbers of beans to the four children, and there are transitions between these states. In this case, each transition consists of a transfer of beans from one child to another. To encode the problem, we need vocabulary to describe a state (here the function “beans” recording who has what) and vocabulary to describe a transition (specifying the donor, the recipient and the amount transferred).

Since the system (the bit of the world we are describing) changes from time to time, the description of things in it is generally a function of the time step or state, so we need to declare “state” (or “time” or something equivalent) as a sort and add it as an argument to most of the predicates and function symbols. Note that the “donor” and “recipient” functions are partial, as no such things exist in the final state.

Our constraints describing transitions amount to a theory of the system dynamics, and need to cover three things. Each transition has preconditions, saying what has to hold in a state in order for that transition to happen, postconoditions, saying what changes as we move to the successor state, and frame axioms which say what does not change. Typically, states inherit most of their properties from their predecessors, but if we are to reason about them we need to specify this, since otherwise it would be consistent with the theory that there could be undocumented changes (e.g. someone might eat a jellybean, or lose one, or buy some more).

The precondition of a bean tranfer is simply that the donor has enough beans. In the case of this simple problem, this is actually enforced by the fact that the numbers of beans are all non-negative and that the transfers are successful, but in general preconditions have to be made explicit, so we give the (redundant) constraint here.

The postconditions are obviously that the donor’s bean count decreases by the transfer amount while the recipient’s increases by the same amount.

The only frame axioms required are that everybody other than the donor and recipient has the same number of beans after the transition as they had before.