Information Technology Reference
In-Depth Information
and is solved by proving whether or not the drawable conclusions are always
identical with what is entailed in terms of the action theory. This providing a
justication for an axiomatization is a major purpose of action theories and
the striving force for developing them. More to this in the brief historical
account in Section 1.3.
In this topic, we concern ourselves with two most fundamental challenges
for action theories, namely, to account for indirect eects of actions (the
Ramication Problem) and to treat unlikely but not impossible action dis-
qualications in a natural way (the Qualication Problem). We develop a
uniform action theory that provides solutions to both problems. We further
present a provably correct axiomatization of our theory by means of a gen-
eral purpose logic, viz. classical rst-order logic in the rst part, i.e., for the
Ramication Problem only, and classical logic augmented by a nonmonotonic
feature for our entire theory.
1
A Word on the Notation
The only expertise needed to understand all parts of the topic is some basic
knowledge of classical logic. But even this is not required except for Sec-
tions 2.9 and 3.6, where our action theory is axiomatized in formal logic.
We use the standard logical connectives, stated in order of decreasing
priority,
:
(negation),
^
(conjunction),
_
(disjunction),
(material im-
plication),
(equivalence),
8
(universal quantication), and
9
(existential
quantication). Both predicate symbols and constants start with a capital
letter whereas function symbols and variables are in lower case, sometimes
with sub- or superscripts. Free variables in formulas are assumed universally
quantied unless indicated otherwise. Special symbols used in example do-
mains are printed in typewriter style, like
turkey
,
potato
,or
tank-empty
.
We further use the basic set operations and relations
[
(union);
\
(inter-
section);
n
(dierence);
2
(membership);
,
(sub- and superset); and
, ! (proper sub- and superset). All other symbols used in this topic are
explained at the time of their rst appearance.
1.2 A Basic Action Theory
Having said much about action theories in general, we now get more for-
mal and introduce a particular, elementary action theory containing all of
the necessary basic ingredients. First of all, any action theory must provide
means for describing states. A state is a snapshot of the part of the world
being modeled at a particular instant of time. State descriptions need to be
composed of atomic propositions. This is vital for our purposes since actions
1
We use
Default Logic
, to be precise; see Section 3.6. The reason for pure classical
logic being insucient in view of the Qualication Problem will be given in due
course.
