# zbMATH — the first resource for mathematics

A normal form for temporal logics and its applications in theorem-proving and execution. (English) Zbl 0893.03003
The paper introduces a normal form, the separated normal form, for propositional temporal formulas. It is proved that every formula $$A$$ of propositional discrete linear temporal logic can be transformed into separated normal form $$\tau(A)$$ such that (i) if $$A$$ is satisfiable, then so is $$\tau(A)$$, and (ii) if $$\tau(A)$$ is satisfied in a model, then $$A$$ is also satisfied in the model. It is shown how the normal form can be extended to first-order temporal logic. Various applications of separated normal form for temporal descriptions of dynamic systems are discussed.

##### MSC:
 03B45 Modal logic (including the logic of norms) 03B35 Mechanization of proofs and logical operations 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
METATEM
Full Text: