Go backward to
Actions
Go up to
Top
Go forward to
Validity and Provability
Predicates as Actions
s
[[
P
]] is boolean for any
s
.
View
P
as action without primed variables.
s
[[
P
]]
t
=
s
[[
P
]] for any
s,t
.
s,t
is a
P
step
iff
s
satisfies
P
.
Replacement of unprimed variables:
State function or predicate
F
.
F'
:=
F
(
forall
'
v
':
v'
/
v
).
s
[[
P'
]]
t
=
t
[[
P
]]
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998