Information Technology Reference
In-Depth Information
The algorithm outline still leaves some open issues:
1. How do we construct a ground formula
φ
that is the disjunctive normal form of
next
(
f
)
?
2. Which literal
true
(
f
)
do we select if there is more than one? Or, in other words,
which precondition
f
of
f
do we select?
We will discuss both issues in the following sections.
Constructing a DNF of
next
(f
)
4.1
Aformula
φ
in DNF is a set of formulas
{
ψ
1
,...,ψ
n
}
connected by disjunctions such
that each formula
ψ
i
is a set of literals connected by conjunctions. We propose the
algorithm in Figure 1 to construct
φ
such that
next
(
f
)
⊃
φ
.
Algorithm 1.
Constructing a formula
φ
in DNF with
next
(
f
)
⊃ φ
Input:
game description
D
, ground fluent
f
Output:
φ
, such that
next
(
f
)
⊃ φ
1:
φ
:=
next
(
f
)
2:
finished
:=
false
3:
while
¬finished
do
4:
Replace every positive occurrence of
does
(
r, a
)
in
φ
with
legal
(
r, a
)
.
5:
Select a positive literal
l
from
φ
such that
l
=
true
(
t
)
,l
=
distinct
(
t
1
,t
2
)
and
l
is
not a recursively defined predicate.
6:
if
there is no such literal
then
7:
finished
:=
true
8:
else
l
:=
9:
bσ
h
:-
b∈D,lσ
=
hσ
10:
φ
:=
φ{l/l}
11:
end if
12:
end while
13: Transform
φ
into disjunctive normal form, i.e.,
φ
=
ψ
1
∨ ...∨ ψ
n
and each formula
ψ
i
is a
conjunction of literals.
14:
for all
ψ
i
in
φ
do
15: Replace
ψ
i
in
φ
by a disjunction of all ground instances of
ψ
i
.
16:
end for
The algorithm starts with
φ
=
next
(
f
)
. Then, it selects a positive literal
l
in
φ
and unrolls this literal, that is, it replaces
l
with the bodies of all rules
h
:-
b
D
whose head
h
is unifiable with
l
with a most general unifier
σ
(lines 9, 10). The re-
placement is repeated until all predicates that are left are either of the form
true
(
t
)
,
distinct
(
t
1
,t
2
)
or recursively defined. Recursively defined predicates are not un-
rolled to ensure termination of the algorithm. Finally, we transform
φ
into disjunctive
normal form and replace each disjunct
ψ
i
of
φ
by a disjunction of all of its ground
instances in order to get a ground formula
φ
.
Note that in line 4, we replace every occurrence of
does
with
legal
to also include
the preconditions of the actions that are executed in
φ
. As a consequence the resulting
∈
