Go backward to
Predicates as Actions
Go up to
Top
Go forward to
Rigid Variables and Quantifiers
Validity and Provability
Action
A
is
valid
(|=
A
)
Every step is an
A
step.
|=
A
<=>
forall
s,t
in
St
:
s
[[
A
]]
t
|=
P
<=>
forall
s
in
St
:
s
[[
P
]]
True regardless of what values are substituted for primed and unprimed variables.
(
x'+y
in
Nat
)
=>
(
2(x'+y)
>=
x'+y
)
Formula
F
is provable (|-
F
)
Formal derivation by rules of logic.
Soundness
of the logic.
Every provable formula is valid.
|-
F
=>
|=
F
.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998