Information Technology Reference
In-Depth Information
ontological aspects, then this necessitates a change of the original entailment
relation. Axiomatizing the way conclusions are drawn from action scenarios
by means of some general purpose logic provides an elegant circumvention of
this problem. Any modication or extension of an action theory then amounts
to modifying or extending the axiomatization; it avoids both changing the
semantics of the underlying logic and adapting the inference engine.
Our axiomatization shall be based on classical logic in conjunction with a
representation technique called
Fluent Calculus
. The distinguishing feature
of this technique is a special way of formalizing states, which allows high-
est flexibility in view of dening how states are manipulated. This principle
is introduced in the following Section 2.9.1. Section 2.9.2 is then devoted
to axiomatizing action laws and causal relationships, and in Section 2.9.3
we formalize all remaining notions, viz. observations, interpretations, and
models of action scenarios. The entire axiomatization is accompanied by a
mathematical proof of its correctness wrt. our action theory.
2.9.1 Reifying States
The common principle of Fluent Calculus-based formalizations of action the-
ories is a particular axiomatization of the fundamental entity, namely, the
state. A state is encoded as a term, accordingly called
state term
, which con-
tains as sub-terms the fluent literals that are true in that state. This enables
the use of rst-order formulas to dene how state terms evolve in the course of
time. Representing fluents by terms instead of predicates follows a standard
technique in logic known as
reication
, which generally allows for a restricted
form of meta-reasoning without appealing to higher-order logic nor to exten-
sions of classical logic. Sub-terms representing fluent literals compose state
terms by employing a special binary function, which is illustratively denoted
by the symbol \
" and is written in inx notation. For example, a term
representation of the state
f:
up
(
s
1
)
;
up
(
s
2
)
; :
light
g
is
(
:
up
(
s
1
)
up
(
s
2
))
:
light
(2.17)
where formally each
n
-place fluent becomes an
n
-place function, each entity
becomes a constant, and where the negation symbol is a distinguished unary
function.
Obviously, it should be irrelevant at which position a fluent literal occurs
in a state term. That is, (2.17) and
up
(
s
2
)
(
:
light
:
up
(
s
1
)), say, represent
identical states. Moreover, double application of function
:
should always
neutralize. This intuition is formally captured by stipulating the following
formal properties of our special functions:
8x; y; z:
(
x y
)
z
=
x
(
y z
)
(associativity)
8x; y:
x y
=
y x
(commutativity)
8x:
x ;
=
x
(unit element)
8x:
::x
=
x
(double negation)
