A Proof of the Compositions of Time Interval Relations
arXiv:1804.01637
Abstract
We prove the 169 compositions of time interval relations. The proof is first-order and inferred from an axiomatic system on time intervals. We show a general proof template that can alleviate the manual proof with Isar.
Proofs available for checking: https://www.isa-afp.org/entries/Allen_Calculus.html