Expressiveness and Completeness of an Interval Tense Logic

摘要

The paper discusses a new tense logic introduced by J.Y. Halpern and Y. Shoham called the system HS. The tense logic is based on intervals. The paper gives an introduction to the system HS and to structures in which it can be interpreted. It is shown that the intervalstructure induced by a linear order can be represented spatially. The expressive strength of the system is discussed. First a comparison with arbitrary point-based systems is made. After that HS is compared to other interval-based logics. In the last section a general result concerning expressive completeness is proved. The last chapter of the paper shows that one can find a complete axiomatization for the class of all temporal orders, as well as for some other classes.