Abstract: 
Allen’s interval calculus is a qualitative temporal representation of
time events. Allen introduced 13 binary relations that describe all
the possible arrangements between two events, i.e. intervals with
nonzero finite length. The compositions are pertinent to
reasoning about knowledge of time. In particular, a consistency
problem of relation constraints is commonly solved with a guideline
from these compositions. We formalize the relations together with an
axiomatic system. We proof the validity of the 169 compositions of
these relations. We also define nests as the sets of intervals that
share a meeting point. We prove that nests give the ordering
properties of points without introducing a new datatype for points.
[1] J.F. Allen. Maintaining Knowledge about Temporal Intervals. In
Commun. ACM, volume 26, pages 832–843, 1983. [2] J. F. Allen and P. J.
Hayes. A Commonsense Theory of Time. In Proceedings of the 9th
International Joint Conference on Artificial Intelligence (IJCAI’85),
pages 528–531, 1985. 
BibTeX: 
@article{Allen_CalculusAFP,
author = {Fadoua Ghourabi},
title = {Allen's Interval Calculus},
journal = {Archive of Formal Proofs},
month = sep,
year = 2016,
note = {\url{http://isaafp.org/entries/Allen_Calculus.html},
Formal proof development},
ISSN = {2150914x},
}
