In the last section, we introduced fluent formulas. We now extend H **to these formulas:**
for any fluent formula ϕ and situation s, H(ϕ, s**) is defined as follows:**
- H(t1 = t2, s**) is** t1 = t2.

- if P is a static proposition, then H(P, s**) is** P.

- inductively, H(¬ϕ, s) is ¬H(**ϕ, s**), H(ϕ∨ ϕ
′, s) is H(**ϕ, s**)∨ H(ϕ
′, s**), and similarly for**
other connectives.

- inductively, H(∀(x, p)ϕ, s) is ∀x.[p(x) ⊃ H(ϕ, s)] and H(∃(x, p)ϕ, s**) is** ∃x.[p(x) ∧
H(ϕ, s)].
According to this definition, H(ϕ, s**) will be expanded to a situation calculus formula where** H **is applied to fluents.**

## 4.2 A Translation To The Situation Calculus

Given a first-order language L **for writing action domain descriptions, we assume that there**
will be a corresponding language L
′**for the situation calculus such that constants in** L
will be constants of sort **object** in L
′, types in L **will be types (unary predicates) in** L
′,
static relations will be predicates of the same arities in L
′, fluents in L **will be functions**
of sort **fluent** in L
′, and actions in L will be functions of sort **action** in L
′**. Under these**
conventions, the following translation will map an action domain description to a situation calculus theory.

Let D be an action domain description. The translation of D **into a situation calculus**
theory is defined as follows:
- a type definition Domain(p, {a1, ..., ak}**) is translated to:**
(∀x).p(x) ≡ (x = a1 **∨ · · · ∨** x = ak),
a1 6= a2 6= **· · · 6**= ak.

- **a primitive fluent definition**
Fluent(f(x1, ..., xn), p1(x1) ∧ · · · ∧ pn(xn) ∧ e1 **∧ · · · ∧** em)
is translated to
(∀x1, ..., xn).Fluent(f(x1, ..., xn)) ≡ p1(x1) ∧ · · · ∧ pn(xn) ∧ e1 **∧ · · · ∧** em.

- **a complex fluent definition**
Complex(f(x1, ..., xn), p1(x1) ∧ · · · ∧ pn(x) ∧ e1 **· · · ∧** em),
Defined(f(x1, ..., xn), ϕ),
is translated to
(∀x1, ..., xn).Fluent(f(x1, ..., xn)) ≡ p1(x1) ∧ · · · ∧ pn(x) ∧ e1 **· · · ∧** em,
(∀x1, ..., xn, s).Fluent(f(x1, ..., xn)) ⊃ [H(f(x1, ..., xn), s) ≡ H(**ϕ, s**)].