Commonsense Reasoning

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.¹ 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 for t₂. Showing that DEC implies EC is more difficult. We prove a number of lemmas stating that individual EC axioms follow from DEC.

LEMMA B.1

If the timepoint sort is restricted to the integers, then

Proof: Suppose DEC. Let τ₁ and τ₂ be arbitrary integer timepoints and β be an arbitrary fluent. ...