Simple reasoning with time-dependent propositions

Simple practical reasoning with propositions whose truth values depend on time is a matter of logical engineering. One needs an expressive language in which simple inferences are productive. Here's one approach, along with some algorithms for implementing it. We also consider reified and non-reified logics, and show that, contrary to a claim of Bacchus et. al., a reified logic is more appropriate than its non-reified equivalent, even for Boolean logic, when time references are interpreted as union-of-convex intervals.