22nd International Symposium on Temporal Representation and Reasoning (TIME), Kassel, Germany, 23 - 25 September 2015, pp.69-78
Allen's Interval Algebra is one of the most prominent formalisms in the area of qualitative temporal (and, by extension, spatial) reasoning. However, its applications are naturally restricted to linear flows of time. While there is some recent work focused on studying relations between intervals (and also between intervals and points) on branching structures, there is no rigorous study of the first-order theory of branching time. In this paper, we approach this problem under a very general definition of time structures as tree-like lattices. Allen's representation theorem shows that meets is expressively complete for the class of all unbounded linear orders, and it is easy to see that it is also complete for the class of all linear orders. Here we prove that, surprisingly, meets remains complete for the class of all unbounded tree-like lattices, and we provide an easy axiomatization of the class of all unbounded tree-like lattices in the branching language. Then, we show that meets becomes incomplete in the class of all tree-like lattices; we give a minimal complete set of three relations for this case along with an axiomatization, which turns out to be particularly challenging to obtain.