© 1996-2019







1.5 First order proof system

Some axioms for the first order case are shown in Table 8.
Let V denote a state variable.
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 finite 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
(V 1 = V 2) f f[V 2V 1].
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 .







2019-05-10
Contact | Home | ITL home | Course | Proofs | Algebra | FL