1 Blocksworld

The blocks-world is a classic AI domain. It has been widely used as a test-bed for planning systems, and is a favorite of logical AI.

When logicians formalize a mathematical domain, it is usual to provide some kind of completeness proof, as a check that the domain is correctly characterized. A good example of this is Euclidean geometry. This can be seen to be complete, by reducing it to the theory of addition and multiplication of real numbers. The theory of + and ∗ over reals can be shown to be complete by quantifier elimination.

Another way in which we can gain confidence that a theory is appropriate is when various different axiomatizations are shown to be equivalent. The classic example of this is set theory, where many different formalizations are known to be equivalent to ZFC.

When we move to more common-sense domains it becomes harder to know when our axiomatizations are correct. However, the same tools that are used in more mathematical domains, completeness results and the equivalence of multiple axiomatizations can still be used.

While many mathematical theories are characterized by first order sentences, even simple domains like blocks world need second order logic. We prove this fact. However, this is not a cause for despair. Although second order logic is highly undecidable in general, the parts of it that we need to use to characterize blocks-world are decidable.

2 Basic Axioms

Our blocks world has 4 sorts, situations s, blocks b, locations l and actions a. These are all disjoint.

We have the usual situation constant S0, and we have a location constant T able. We have a countable number of blocks. That is we have a function S on blocks, and a block constant A_{0}. We write A_{i+1} for S(A_{i}), and we have,

l \begin{matrix}∀a, a_{1}.S(a) = S(a_{1}) → a = a_{1} \\ ∀a.¬(S(a) = A_{0}) \\ ∀ϕ.ϕ(A_{0}) ∧ ∀a.ϕ(a) → ϕ(S(a))) → ∀a.ϕ(a) \end{matrix}  (1)

Thus in particular we have, A_{i} ≠ A_{j}|i ≠ j. We have locations, which are the top of a block, or are the T able.

∀l.∃b.top(b) = l ∨ l = T able  (2)

All distinct location terms denote distinct locations.

∀b, b′.top(b) = top(b′) → b = b′, ∀b.top(b) ≠ T able  (3)

We have a function from actions and situations to situations, r(a, s), and a function from blocks and locations to actions, move(b, l), which gives the action where block b is moved to location l.

All distinct action terms are distinct, and all actions are moving blocks.

\begin{matrix}∀b, b′, l, l′.move(b, l) = move(b′, l′) → b = b′ ∧ l = l′ \\ ∀a.∃b, l.a = move(b, l) \end{matrix}

We have our foundational axioms for situations. We have fluents, On(b, l, s) which states that b is on location l in situation s, and Clear(l, s). Clear(l, s) is fully defined in terms of On.

∀l, s.Clear(l, s) ≡ (∃b.∀b′.l = top(b′) ∧ ¬On(b′, top(b), s)) ∨ l = T able  (4)

We have an explanation closure axiom that determines On(b′, r(a, s)) in terms of On at the previous situation. If we attempt to move a block which has a block on top of it, or if we attempt to move a block to a location that contains a block, or it we try to move a block to it own top, then there is no change in the locations of all the blocks.

∀b, b′, l, l′, s.On(b′, l′, r(move(b, l), s)) ≡ ; \begin{matrix}b ≠ b′ ∧ On(b′, l′, s) ∨ b′ = b ∧ l′ = l ∧ top(b) ≠ l∧ \\ (∀b_{2}.¬On(b_{2}, top(b), s)) ∧ ((∀b_{2}.¬On(b_{2}, l, s)) ∨ l = T able)∨ \\ ( \begin{matrix}¬(∀b_{2}.¬On(b_{2}, top(b), s))∨ \\ ¬(∀b_{2}.¬On(b_{2}, l, s) ∧ l ≠ T able)∨ \\ (l ≠ l′ ∧ b ≠ b′) ∨ top(b) = l \end{matrix} ) ∧ On(b′, l′, s) \end{matrix}  (5)

From this explanation closure axioms, and the previous axioms, we can derive the following explanation closure axiom for Clear(l, s)

A location l is clear after moving b to l′, if , l is the table, which is always clear, or l′ ≠ l and l was clear before, or if b was on l, and top(b) and l′ are clear, and top(b) ≠ l′, or finally, if l = l′ and the action fails, that is either top(b) is not clear, or l′ = top(b).

That these conditions suffice can be seen by considering the other possibilities, and realizing that in each case, l is not clear.

Up until now we have not needed any second order logic. However, our axioms are insufficient to eliminate certain unwanted situations, such as having a block be on its own top. Therefore we consider domain constraints that eliminate these possibilities.

3 Domain Constraints

We will not be able to define our domain constraints in first order logic. We will need the notion of transitive closure, to state that our towers cannot be infinitely tall. This cannot be captured in first order logic.

We define an operator ∗ that takes a binary predicate on blocks into its transitive closure. We write ∗(P) as P^{∗}

\begin{matrix}(∀b, b′.P (b, b′) → P^{∗}(b, b′))∧ \\ (∀b, b′, b′′.P (b, b′) ∧ P^{∗}(b′, b′′) → P^{∗}(b, b′′))∧ \\ ∀Φ. [ \begin{matrix}(∀b, b′.P (b, b′) → Φ(b, b′))∧ \\ (∀b, b′, b′′.P (b, b′) ∧ Φ(b′, b′′) → Φ(b, b′′))∧ \\ ∀b, b′.Φ(b, b′) → P^{∗}(b, b′) \end{matrix} ] → \\ ∀b, b′.P^{∗}(b, b′)) → Φ(b, b′) \end{matrix}  (6)

We define the predicate above(b, b′, s) as the transitive closure of λb, b′.On(b, top(b′), s).

∀b, b′, s.above(b, b′, s) ≡ ∗(λb, b′.On(b, top(b′), s))(b, b′)  (7)

We can now write some domain constraints about the blocks-world. No block is above itself, ∀b, s.¬above(b, b, s). Every block is somewhere. ∀b, s.∃l.On(b, l, s).

Every block is above or equal to a block that is on the table.

∀b, s∃b′.On(b′, T able, s) ∧ (above(b, b′, s) ∨ b = b′)  (8)

Every block is on a single location.

\begin{matrix}∀b, s¬On(b, T able, s) → ∃b′.On(b, top(b′), s) ∧ ∀b_{1}.On(b, top(b_{1}), s) → b_{1} = b′ \\ ∀b, b′, s.On(b, top(b′), s) → ¬On(b, T able, s) \end{matrix}  (9)

Every location has at most one block on it.

∀b, b_{1}, b_{2}, s.On(b_{1}, top(b), s) ∧ On(b_{2}, top(b), s) → b_{1} = b_{2}  (10)

There is a clear block above or equal to every block.

∀b, s∃b′.∀b′′¬On(b′′, top(b′), s) ∧ (above(b′, b, s) ∨ b = b′)  (11)

These last four domain constraints are enough to prove that every situation has a set of towers, where a tower is a finite list of blocks (A_{i_{0}}, …, A_{i_{m}}) where On(A_{i_{j+2}}, top(A_{i_{j+1}}), s) and On(A_{i_{0}}, T able, s), and no other blocks are on any other locations.

Theorem: 1 Every model 𝔄 of the axioms 8, 9, 10,and 11 at a given situation s can be modeled by a set of totally ordered finite disjoint sets of blocks, such that their union is the entire universe of blocks. Let the set of sets be D = {B_{i}|i ∈ I} They are disjoint, ∀i, j.i ≠ j → B_{i} ∩ B_{j} = ∅. Each set is totally ordered, let these order relations on each B_{i} be <_{i}.

We now interpret every model of 𝔄 as a set D, as follows. We let our index setI be the set of blocks on the table.

for all b.b ∈ I =^{def} 𝔄 ⊧ On(b, T able, s)

We let our sets of blocks B_{i} be

for all b.b′ ∈ B_{b} =^{def} 𝔄 ⊧ above(b′, b, s) ∨ b = b′

We let our order relation <_{b} be

for all b.b′ <_{b} b′′ =^{def} 𝔄 ⊧ (above(b′, b, s) ∨ b = b′) ∧ above(b′′, b′, s)

This shows that our theory of blocksworld agrees with the intuitive notion of a collection of disjoint finite towers. It also suggests the proof of the next theorem, which relies on the representation of blocksworld as a set of total orders.

Theorem: 2 The second order theory of the static blocksworld, 8, 9, 10 and 11 is decidable.

Proof-Sketch: We reduce this to the decidability of the second order theory of linear order.

The basic idea is to introduce a unary predicate I true just of the blocks on the ground, then all the towers are ordered, and the ≤ relation is true of two blocks, if one is in a lower tower than the other, or lower in the same tower. Now above can be recovered from ≤ and our new predicate I. The other domain constraints can be stated in this language. We also have the harder question of the dynamic blocksworld. We can also show that this is decidable.