Equivalence of EC and DEC
In this appendix, we prove that EC and DEC are logically equivalent if the timepoint sort is restricted to the integers.1 Our proof is structured as follows: We must show that EC implies DEC and that DEC implies EC. It is easy to show that EC implies DEC. This follows by universal instantiation, substituting t1 + 1 for t2. Showing that DEC implies EC is more difficult. We prove a number of lemmas stating that individual EC axioms follow from DEC.
If the timepoint sort is restricted to the integers, then
Proof: Suppose DEC. Let τ1 and τ2 be arbitrary integer timepoints and β be an arbitrary fluent. ...