Introduction to Logic

Blocks World Programs

The Blocks World is a popular application area for illustrating ideas in elementary robot programming. In this article, we use Herbrand Logic to formalize the Blocks World and we use our reasoning methods to verify that simple robot programs when run in given states achieve specific goals.

Note that Chapter 6 of the notes discusses a simple version this world. The Blocks World described there is static - there is a just one configuration of blocks, and it cannot change. In this article, we discuss a dynamic version of this world - one in which there is a robot capable of observing and acting upon the world to change its state.

Each state of our dynamic Blocks World consists of an arrangement of toy blocks on a table, as in the scene shown below. Here, there are five distinct blocks. In this state, block C is on block A, block A is on block B and block E is on block D. C and E are clear, while B and D are on the table.

C A B E D

Our robot has sensors that allow it to observe information about the state of the world. In what follows, we assume there is a camera that allows the robot to determine whether a block is clear, whether a block is on the table, and whether one block is on top of another.

Our robot also has an arm with a grasper on the end. This allows the robot to pick up blocks and place them in other locations. In what follows, we assume that the robot has just two types of actions - it can unstack a block from another block and put it on the table or it can take a block from the table and stack it on another block. In order to unstack a block, that block must be clear of other blocks; and, in order to stack one block on another, both blocks must be clear.

A Blocks World program is a schedule of observations and actions. Some programs are linear. For example, in the situation pictured above, the robot might unstack C from A and then unstack A from B and then stack B onto C and the stack A onto B. Programs can also be conditional. For example, the program might dictate that the robot unstack C from A; then, if D is on E, it stacks C onto D; otherwise, it stacks C onto E. Programs can also have loops. For example, a program might dictate that the robot keep unstacking blocks until block B is clear.

Typically, a program is designed to be executed in either a single state or a set of possible states, and it is intended to produce any one of several goal states (which may be dependent on the initial state). For example, we might write a program to convert the initial state shown above into one in which A is on B and B is on C. Or we might imagine a program that inverts the order of blocks in the stack on the left.

In order to describe the Blocks World, we start with a vocabulary with five object constants (a, b, c, d, e), with one object constant corresponding to each of the five blocks in the scene. The intent here is for each of these object constants to represent the block marked with the corresponding capital letter in the scene.

Each state of the world is described in terms of conditions that are true or false in that state. In order to name these conditions, we add three function constants to our vocabulary - on, clear, and table. The condition on(a,b) is true in a state if and only if Block A is on Block B. The condition clear(a) is true in the state if and only if there are no blocks on top of Block A. The condition table(a) is true in the state if and only if Block A is not on top of some other block.

In order to describe the robot's actions, we add two more function constants - t and s. The term t(a,b) refers to the action of removing a from b and placing it on the table. The term s(a,b) refers to the action of taking a from the table and placing it on b.

In order to describe the dynamics of the world, we add an object constant s1 to refer to the initial state, and we add a binary function constant do to designate the state resulting from the execution of a given action (its first argument) in a given state (its second argument). For example, we use the term do(t(a,b),s1) to refer to the state that results from performing action t(a,b) in state s1.

Finally, we add a binary relation constant true to say which conditions are true in which states. For example, the sentence true(on(c,a),s1) says that the condition on(c,a) is true in state s1.

Given this vocabulary, we can begin to describe the dynamics of the Blocks World. We will look first at how to describe states directly. Then we will look at the effects of actions. Finally, we will use these description to simulate programs and verify that they achieve desired goals.

The easiest way to describe a state is to say which conditions are true in that state. For now, we just ignore conditions that are false. For example, we can describe the state shown above with the following sentences.

true(clear(c),s1)
true(on(c,a),s1)
true(on(a,b),s1)
true(table(b),s1)
true(clear(e),s1)
true(on(e,d),s1)
true(table(d),s1)

We can characterize our actions by talking about their effects. We do this by writing conditionals like the ones shown below. The first says that, in any state, in which block x is clear and and on the table and if block y is clear, then block x will still be clear after stacking x onto y and block x will be on block y.

true(clear(x),w) ∧ true(table(x),w) ∧ true(clear(y),w) ⇒
    true(clear(x), do(s(x,y),w)) ∧ true(on(x,y), do(s(x,y),w))
 
true(clear(x),w) ∧ true(on(x,y),w) ⇒
    true(clear(x), do(t(x,y),w)) ∧ true(table(x), do(t(x,y),w)) ∧ true(clear(y), do(t(x,y),w))

Unfortunately, we are not quite done. While these sentences describe what changes as a result of the execution of our robot's actions, they do not say what stays the same. In addition, we must write frame axioms to express that fact that everything else stays the same. The following sentences are sufficient for our encoding of the Block World.

true(clear(x),w) ⇒ true(clear(x), do(t(u,v),w))
true(table(x),w) ⇒ true(table(x), do(t(u,v),w))
true(on(x,y),w) ∧ ¬same(x,u) ⇒ true(on(x,y), do(t(u,v),w))
 
true(clear(y),w) ∧ ¬same(y,v) ⇒ true(clear(y), do(s(u,v),w))
true(table(x),w) ∧ ¬same(x,u) ⇒ true(table(x), do(s(u,v),w))
true(on(x,y),w) ⇒ true(on(x,y), do(s(u,v),w))

Before we talk about programs, let's see how we can use these sentences to reason about the dynamics of the Blocks World. Consider the state shown above. Now imagine that the robot unstacks C from A, then stacks C onto E. In other words, consider the state do(s(c,e),do(t(c,a),s1)). What conditions are true in this state?

To answer this question, we start with the facts describing the conditions that are true in state s1. The facts are listed above and reproduced below.

true(clear(c), s1)
true(on(c,a), s1)
true(on(a,b), s1)
true(table(b), s1)
true(clear(e), s1)
true(on(e,d), s1)
true(table(d), s1)

Next, we use our rules about dynamics to deduce the conditions that are true in state do(t(c,a),s1). See below.

true(clear(a), do(t(c,a),s1))
true(on(a,b), do(t(c,a),s1))
true(table(b), do(t(c,a),s1))
true(clear(c), do(t(c,a),s1))
true(table(c), do(t(c,a),s1))
true(clear(e), do(t(c,a),s1))
true(on(e,d), do(t(c,a),s1))
true(table(d), do(t(c,a),s1))

Finally, we use our rules about dynamics once again to deduce the conditions that are true in state do(s(c,e),do(t(c,a),s1)). See below.

true(clear(a), do(s(c,d),do(t(c,a),s1)))
true(on(a,b), do(s(c,d),do(t(c,a),s1)))
true(table(b), do(s(c,d),do(t(c,a),s1)))
true(clear(c), do(s(c,d),do(t(c,a),s1)))
true(on(c,e), do(s(c,d),do(t(c,a),s1)))
true(on(e,d), do(s(c,d),do(t(c,a),s1)))
true(table(d), do(s(c,d),do(t(c,a),s1)))

Reading off the conditions, just deduced, we can see that the end result is the state shown below. The upshot of performing these two actions is that block C moves from A to E.

A B C E D

This example shows how we can model and simulate simple linear programs. We can do the same for more complex programs.

The disadvantage of this approach to formalizing programs is that structure of the programs is lost in this approach; it is implicit in those terms involving do. We can fix this problem by introducing some new vocabulary that allows us to describe such programs as terms in our language. This representation makes the structure clearer.

Let's start with linear programs. As a linear program is just a sequence of actions, we can use list notation to represent such programs. To this end, we borrow the cons function from our formalization of lists. For example, to represent the sequence of actions consisting of t(c,a) followed by s(c,e), we would write cons(t(c,a),cons(s(c,e),nil)). To make things more legible, we can write our nested cons terms using more conventional list notation, keeping in mind that this is just shorthand for the nested cons term. For example, we can write cons(t(c,a),cons(s(c,e),nil)) as shown below.

[t(c,a), s(c,e)]

To describe conditional programs, we introduce the ternary function constant if. For example, we can represent a conditional program as shown below. The intent here is that on(d,e) is the condition, s(c,d) is to be performed if the condition is true, and s(c,e) to be performed if the condition is false.

if(on(d,e), s(c,d), s(c,e))

Finally, we introduce a binary relation define and use it to relate subroutines to their definitions. For example, we might introduce the constant move to refer to a program to move a block from one block to another by tabling the first block from the second and stacking it on the third.

define(move(x,y,z), [t(x,y), s(y,z)])

The semantics of sequential programs can be expressed as shown below. A condition is true in the state resulting from the execution of a list of actions if it is true in the state that results from executing the "tail" of the sequence in the state resulting form the head of the sequence.

true(z,w) ⇔ true(z,do(nil,w))
true(z,do(v,do(u,w))) ⇔ true(z,do(cons(u,v),w))

To see how this works, consider the problem of simulating the execution of the sequence shown above in the initial state shown at the start of this chapter. We could proceed as before and simulate the program step by step. However, we can get the same result with a different approach. Let's assume that an arbitrary condition z is true in the state do(s(c,e),do(t(c,a),s1)). Using the first rule above, we know that z is true in state do(nil,do(s(c,e),do(t(c,a),s1))). Using our second rule above, we can prove the result in the third line below. Then, using our second rule once again, we get the fourth line. At this point, from our initial assumption we have shown that everything we deduced earlier about state do(s(c,e),do(t(c,a),s1)) is also true of state do(cons(t(c,a),cons(s(c,e),nil)),s1). Consequently, we can just copy over our results from before.

true(z,do(s(c,e),do(t(c,a),s1)))
true(z,do(nil,do(s(c,e),do(t(c,a),s1))))
true(z,do(cons(s(c,e),nil), do(t(c,a),s1)))
true(z,do(cons(t(c,a),cons(s(c,e),nil)),s1))

We can express the semantics of conditional programs in similar fashion. If the condition in a conditional program is true, then any condition true in the state resulting from executing the second argument is true in the state resulting from the execution of the conditional. If the condition is false, then any condition true in the state resulting from executing the third argument is true in the state resulting from the execution of the conditional.

true(u,w) ∧ true(v,do(v1,w)) ⇒ true(v,do(if(u,v1,v2),w))
~true(u,w) ∧ true(v,do(v2,w)) ⇒ true(v,do(if(u,v1,v2),w))

Any condition true in the state resulting from executing the definition of a subroutine is true in the state resulting from the execution of the subroutine.

define(u,v) ∧ true(z,do(v,w)) ⇒ true(z,do(u,w))

With these definitions for the semantics of our programming language, we can simulate programs to verify their results, as we did above with the linear program.

Although this article focusses on the Blocks World, the approach used here can be applied to programs in other physical environments, and it can be used in analyzing programs in traditional programming languages as well. The details are more complicated, but the basic approach is the same.

Suggested Exercises. Verify that executing the program [t(c,a),t(a,b),s(b,c),s(a,b)] results in a state in which A is on B and B is on C. Verify that executing move(c,a,e) in the state illustrated at the start of this article results in a state in which Block C is on block E. Define a subroutine invert that takes two arguments such that the first is clear and positioned on the second and that produces a state where the second is on the first.