APPENDIX B

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 *t*_{1} + 1 for *t*_{2}. 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. ...

Start Free Trial

No credit card required