ITL
© 1996-2018







5 First order proof system

Some axioms for the first order case are shown in Table 8.
Let v refer to both static and state variables.
We denote by f[ev] that in formula f expression e is substituted for variable v.


Table 8: Some First Order Axioms and Rules for ITL.
ForallSub
v f f[ev],
where the expression e has the same data
and temporal type as the variable v and
is free for v in f.
ForallImplies
v (f1 f2) (f1 v f2),
where v doesn’t occur freely in f1.
SubstAxiom
(v1 = v2) f f[v2v1].
StaticWeakNext
w w,
where w only contains static variables.
ExistsChopRight
v (f1 ; f2) (v f1) ; f2,
where v doesn’t occur freely in f2.
ExistsChopLeft
v (f1 ; f2) f1 ; (v f2),
where v doesn’t occur freely in f1.
ForallGen
f ⇒ ⊢ v f,
for any variable v.







2018-03-10
Contact | Home | ITL home | Course | Proofs | Algebra | FL