
## 2.5 Domain Axioms

Domain axioms are constraints on static relations. For instance, for the static proposition connected(d, r1, r2), we may want to impose the following constraint: connected(d, r1, r2) ≡ connected(d, r2, r**1). In our language, domain axioms are specified by expressions of the** form:
Axiom(ϕ),
where ϕ **is a fluent formula that does not mention any fluents, i.e. it mentions only static** relations and equality. For instance, the above constraint on connected **is written as:**
Axiom(∀(d, door)∀(r1, room)∀(r2, room)connected(d, r1, r2) ≡
connected(d, r2, r1)),
where door and room **are types.**

## 2.6 Action Definitions

Actions are defined by expressions of the following form:
Action(a(x1, ..., xn), p1(x1) ∧ · · · ∧ pn(xn) ∧ e1 **∧ · · · ∧** em),
where a is an n-ary action, and pi's and ei**'s are the same as in primitive fluent definitions.**
For instance, in the blocks world, given the type definition Domain(block, {1, 2, 3}**), the**
following action specification:
Action(stack(x, y), block(x)∧ **block**(y) ∧ x 6= y)
would generate the following six action instances:
stack(1, 2), stack(1, 3),stack(2, 1),stack(2, 3), stack(3, 1)**,stack**(3, 2).

There should be exactly one action definition for each action.

## 2.7 Action Precondition Definitions

Action precondition definitions are specified by expressions of the following form:
Precond(a(x1, ..., xn), ϕ),
where a is an n-ary action, ϕ is a fluent formula whose free variables are among x1**, ..., x**n.

There should be exactly one precondition definition for each **action. For instance, in the**
blocks world, we may have:
Precond(stack(x, y), clear(x)∧ clear(y) ∧ **ontable**(x)),
which says that for the action stack(x, y) to be executable in a situation, clear(x), **clear**(y),
and ontable(x**) must be true in it.**