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

Erik T. Mueller, IBM Research; and Geoff Sutcliffe, University of Miami

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.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.