Reasoning in the Event Calculus Using First-Order Automated Theorem Proving

All Papers

The event calculus is a powerful and highly usable formalism for reasoning about action and change. The discrete event calculus limits time to integers. This paper shows how discrete event calculus problems can be encoded in first-order logic, and solved using a first-order logic automated theorem proving system. The following techniques are discussed: reification is used to convert event and fluent atoms into first-order terms, uniqueness-of-names axioms are generated to ensure uniqueness of event and fluent terms, predicate completion is used to convert second-order circumscriptions into first-order formulae, and a limited first-order axiomatization of integer arithmetic is developed.