Information Technology Reference
In-Depth Information
2.9.2 Axiomatizing Action Laws and Causal Relationships
Having dened a suitable representation of states, we now axiomatize two
ways of state modication, namely, by means of action laws and causal rela-
tionships. To begin, let
f 1 [ x 1 ]= a 1 transforms C 1 into E 1 ;:::; n [ x n ]= a n transforms C n into E n g
be the underlying set of action laws. These laws dene the ternary predicate
Action ( a; c; e ), an instance of which is true if and only if there exists an action
law for action a with condition 1
c
and eect 1
e
, that is,
_
Action ( a; c; e )
9x i [ a = a i ^ c = C i ^ e = E i ]
(2.24)
i =1
E.g., the familiar two action laws for toggling a switch may be encoded as
Action ( a; c; e ) 9x [ a = toggle ( x ) ^ ( c = : up ( x ) ^ e = up ( x )
_ c = up ( x ) ^ e = : up ( x ))]
which is a slightly more compact equivalent of the schematic instantiation
of (2.24).
Applicability and application of action laws are axiomatized with the help
of the properties of EUNA elaborated in the previous section. An action
law whose condition is represented by collection c is applicable to a state
represented by term s if and only if some term z can be found such that
c z equals s under EUNA . For the latter has been proved equivalent to
set 1
c being subset of s . Entailment of c z = s also guarantees that
z contains all fluent literals in s but not in c . A preliminary successor, or
rather a representation thereof, is then obtained by concatenating z and the
eect term e of the action law in question, yielding term z e . Correctness
of this axiomatization of applying action laws is guaranteed by the following
proposition.
Proposition 2.9.4. Let A be a set of action names, L a set of action
laws, S a state, and a an action. Furthermore, let s 0
be a collection of
fluent literals. Then
EUNA; (2 : 24) j = 9c; e; z [ Action ( a; c; e ) ^ c z = s ^ s 0 = z e ]
(2.25)
i there exists a preliminary successor S 0
of S and action a such that
EUNA j = s 0 = S 0 , else
EUNA; (2 : 24) j = :9c; e; z [ Action ( a; c; e ) ^ c z = s ^ s 0 = z e ]
Proof. Formula (2.24) for predicate Action in conjunction with the standard
equality axioms in EUNA imply that (2.25) holds i L contains an action
law instance a transforms C into E such that
EUNA j = 9z [ C z = s ^ s 0 = z E ]
This in turn holds i
 
Search WWH ::




Custom Search