- If ϕ and ϕ
′ **are fluent formula, then** ¬ϕ, ϕ ∨ ϕ
′, ϕ ∧ ϕ
′, ϕ ⊃ ϕ
′**, and** ϕ ≡ ϕ
′ **are also**
fluent formulas.

- If ϕ is a fluent formula, x a variable, and p a type, then ∀(x, p)ϕ (for all x **of type** p, ϕ holds) and ∃(x, p)ϕ (for some x of type p, ϕ **holds) are fluent formulas. Notice that** we require types to have finite domains, so these quantifications are really shorthands:
If the domain of p is {a1, ..., an}, then ∀(x, p)ϕ **stands for**
.$\lor\,\varphi(x/c)$
ϕ(x/a1) ∧ · · · ∧ ϕ(x/an),
and ∃(x, p)ϕ **stands for**
ϕ(x/a1) ∨ · · · ∨ ϕ(x/an).

A complex fluent is then specified in our language by a pair of expressions of the following form:
Complex(f(x1, ..., xn), p1(x1) ∧ · · · ∧ pn(xn) ∧ e1 **· · · ∧** em),
Defined(f(x1, ..., xn), ϕ),
where pi's and ei's are the same as in primitive fluent definitions, and ϕ **a fluent formula**
that does not mention any complex fluents and whose free variables are among x1**, ..., x**n.

The first expression specifies the syntax and the second the semantics of the complex fluent.

For instance, the complex fluent clear **in the blocks world can be specified as:**
Complex(clear(x)**, block**(x)), Defined(clear(x), ¬∃(y, block)on(y,x)).

As we mentioned above, quantifiers here are just shorthands because each type must have a finite domain. For instance, given the following specification:
Domain(**block,** {1, 2, 3}), Fluent(on(x, y), block(x)∧ **block**(y))
the above fluent definition for clear **will be expanded to:**
Defined(clear(1), ¬(on(1, 1)∨ on(2, 1) ∨ on(3, **1)))**,
Defined(clear(2), ¬(on(1, 2)∨ on(2, 2) ∨ on(3, **2)))**, Defined(clear(3), ¬(on(1, 3)∨ on(2, 3) ∨ on(3, **3)))**.

## 2.4 Static Relation Definitions

As we mentioned, a static relation is one that is not changed by any action in the domain.

For instance, in the robot navigation domain, we may have a proposition connected(d, r1, r2) meaning that door d connects rooms r1 and r**2. The truth value of this proposition cannot**
be changed by the navigating robot that just rolls from room to room.

In our language, a static relation is defined by an expression **of the following form:**
Static(g(x1, ..., xn), p1(x1) ∧ · · · ∧ pn(xn) ∧ e1 **∧ · · · ∧** em),
where g is an n-ary predicate, and pi's and ei**'s are the same as in primitive fluent definitions.**
The meaning of this expression is similar to a fluent definition, and there should be exactly one definition for each static relation.