Commonsense Reasoning, 2nd Edition

Appendix B

Equivalence of EC and DEC

Abstract We prove that EC, an axiomatization of the continuous event calculus, and DEC, an axiomatization of the discrete event calculus 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.

Keywords Event calculus, Discrete event calculus, Equivalence of EC and DEC, Equivalence proof

In this appendix, we prove that EC and DEC are logically equivalent if the ...