zbMATH — the first resource for mathematics

A decision procedure and complete axiomatization of finite interval temporal logic with projection. (English) Zbl 1050.03012
This paper is concerned with propositional interval temporal logic with projection. The specific connectives of the logic are the chop operator (;) and the projection operator (proj).
The main novelty of the paper is a proof of completeness for a logic with projection operator. This complete axiomatization is based on a tableaux procedure, for which the identification of normal forms for all connectives is crucial.
This fact suggests an executable interpretation of the logic.

03B44 Temporal logic
03B35 Mechanization of proofs and logical operations
03B25 Decidability of theories and sets of sentences
Full Text: DOI