Information Technology Reference
In-Depth Information
plausible the better they tackle the Frame Problem. Triggered by an increas-
ing number of action formalisms being erroneous in allowing unintended and
counter-intuitive conclusions, the reliability of action encodings became a
new major problem. The by far most popular case is the approach proposed
in [78], which uses so-called circumscription [77], a particular extension to
classical rst-order logic, to address the Frame Problem. Following common
practice, this approach was validated merely by example. Soon, however, a
serious flaw of this method was revealed with the help of yet another simple
example
12
which is treated against the intuition [49].
13
The increasing diculties with assessing the correctness of action for-
malisms just by appealing to the intuition led to the insight that formal
validation methods are needed in order to guarantee reliability. The rst step
in this direction was a generalization of an intuitively correct encoding of an
example domain so that a whole, well-dened class of domains is covered [66].
This generalization was accompanied by a formal proof that the encoding of
any such domain will yield the same results as obtained in the example, hence
will inherit the intuitive correctness. Although this result was established for
a very restricted class of domains (compared, e.g., to what is expressible in
our basic action theory), this was the rst time that an action formalism
itself was subject to a formal proof of its correctness.
The rst action theory that deserves this name in being truly independent
of a specic axiomatization was the
Action Description Language
, abbrevi-
ated
A
[34].
14
This formalism and our basic action theory have similar ex-
pressiveness except that
A
is restricted to nullary (i.e., propositional) fluents
and does not support non-deterministic actions. In fact, many of our notions
and notations were borrowed from this rst approach. The Action Descrip-
tion Language was rst employed to validate an encoding of action domains
based on Situation Calculus and using so-called extended logic programs [34].
Later,
A
has been employed for the evaluation of action formalisms such as
Situation Calculus based on abductive logic programs [24, 20], Situation Cal-
culus with so-called successor state axioms (see Section 2.10) and Situation
Calculus with circumscription, respectively [58], and Fluent Calculus (see
Section 2.9) based on so-called equational logic programs [108], just to men-
tion a few. Any of these results veries correctness of the respective action
formalisms if applied to domains expressible in
A
. In order to obtain more
general assessment results, the original Action Description Language has been
extended into various directions, among which we again mention just a few.
12
This famous example is known as the
Yale Shooting
scenario; see also Sec-
tions 3.7 and 2.8.
13
Moreover, the improvement to the original formulation proposed in [3], again
motivated solely by examples, has been proved (by a counter-example) re-
stricted to a stronger extent than originally claimed [59].
14
First published as [33]. The reader should not be misled by the name;
A
is not
just a language but comes along with a formal semantics of how expressions in
this language are to be interpreted in terms of state transitions, models, and
entailment.
