document: Extending Kamp 's theorem to model time granularity In this paper , a generalization of Kamp 's theorem relative to the functional completeness of the until operator is proved . Such a generalization consists in showing the functional completeness of more expressive temporal operators with respect to the extension of the first-order theory of linear orders MFO -LSB- < -RSB- with an extra binary relational symbol . The result is motivated by the search of a modal language capable of expressing properties and operators suitable to model time granularity in omega - layered temporal structures
doc_bio_tags: O O O O O B I I O O O O O O O O O O O O O B I O O B I O O O O O O O O O O B I O O O B I O O O O O O O O O O B I O O O O O O O B I I O O O O O O O O O O O O O O O O O O O O B I I O O O O O O