  In this paper, we propose an implementation of temporal semantics which is
suitable for inference problems. This implementation translates syntax trees to
logical formulas, suitable for consumption by the Coq proof assistant. We
support several phenomena including: temporal references, temporal adverbs,
aspectual classes and progressives. We apply these semantics to the complete
FraCaS testsuite. We obtain an accuracy of 81 percent overall and 73 percent
for problems explicitly marked as related to temporal reference.
