ITL
© 1996-2016







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 o f ⊃ fve,                                   |
|                  where the expression e has the same data and       |
|                  temporal type as the variable v and is free for       |
|                  v in f.                                            |
| ForallImplies     ⊢ ∀v o (f1 ⊃ f2) ⊃ (f1 ⊃ ∀v o f2),                 |
|                  where v doesn’t occur freely in f .                 |
| SubstAxiom       ⊢ ! (A = B ) ⊃ f ≡ fB .       1                   |
| StaticWeakNext    ⊢ w ⊃   w,         A                              |
|                        c                                           |
|                  whereow only containsostatic variables.              |
| ExistsChopRight   ⊢ ∃v  (f1;f2) ⊃ (∃v   f1);f2,                      |
|                  whereov doesn’t occur freeoly in f2.                 |
| ExistsChopLeft    ⊢ ∃v  (f1;f2) ⊃ f1;(∃v   f2),                      |
|                  where v doesn’t occur freely in f1.                 |
| ForallGen         ⊢ f ⇒  ⊢ ∀v o f ,                                 |
-------------------for any-variable-v.---------------------------------