mean those atomic formulas formed by fluents. An equality **atom is one of the form** u = v, where u and v are variables or constants, and an inequality constraint is **one of the form**
u 6= v. Actions are represented by functions, and they are assumed **to be the only functions**
with positive arities in the language.

Our action description language includes the following components.

## 2.1 Type Definitions

A type definition is specified by expressions of the following **form:**
Domain(p, {a1**, ..., a**n}),
where p is a type, and a1, ..., an **are constants. The intuitive meaning of this expression is** that the domain (extension) of the type p is the set {a1, ..., an}**. For instance, in the blocks**
world, we may have a type called block**, and have, say, five blocks named numerically:**
Domain(block, {1, 2, 3, 4, 5}). In a logistics domain, we may have a type called loc for locations, and have, say, 3 locations l1, l2, and l3: Domain(loc, {l1, l2, l3}).

## 2.2 Primitive Fluent Definitions

Primitive fluents are defined by expressions of the following **form:**
Fluent(f(x1, ..., xn), p1(x1) ∧ · · · ∧ pn(xn) ∧ e1 **∧ · · · ∧** em),
where f is an n-ary fluent, each pi, 1 ≤ i ≤ n, a type, and each ei, 1 ≤ i ≤ m**, an**
inequality constraint of the form xj 6= xk, for some 1 ≤ j < k ≤ n**. The intuitive meaning**
of this expression is that f(x1, ..., xn**) is a legal fluent atom if the second argument is true.**
For instance, in the blocks world, given the type definition Domain(block, {1, 2, 3}**), the** following fluent specification:
Fluent(on(x, y), block(x)∧ **block**(y) ∧ x 6= y)
would generate the following six legal fluent atoms:
on(1, 2), on(1, 3),on(2, 1),on(2, 3),on(3, 1),on(3, 2).

Clearly, there should be exactly one fluent definition for each fluent.

## 2.3 Complex Fluent Definitions

Given a set of primitive fluents, one may want to define some new **ones. For instance,** in the blocks world, given the primitive fluent on, we can define clear in terms of on as: (∀x)clear(x) ≡ ¬(∃y)on(**y, x**).

To specify complex fluents like clear, we first define fluent formulas **as follows:**

- t1 = t2 is a fluent formula, where t1 and t2 **are terms, i.e. either a constant in the**
domain of a type or a variable.

- f(t1, ..., tn) is a fluent formula, where t1, ..., tn are terms, and f **is either an n-ary**
primitive fluent, a complex fluent, or a static relation.