×

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)
Software:
METATEM
PDF BibTeX XML Cite
Full Text: DOI