Reasoning in the event calculus using first-order automated theorem proving

Abstract

The event calculus (EC) (Shanahan 1999) is a powerful and highly usable formalism for reasoning about action and change, which is rapidly finding application in such areas as natural language processing and robotics. Kowalski and Sergot (1986) introduced the original event calculus, which was expressed as a logic program, and Shanahan and Miller introduced axiomatizations of the event calculus in first- order logic (Shanahan 1997; Miller & Shanahan 2002). The discrete event calculus (DEC) was developed by Mueller (2004) in order to facilitate solution of event calculus rea- soning problems using satisfiability (SAT) solvers. Since the introduction of the EC and DEC axiomatiza- tions, several event calculus reasoning systems have been implemented. However, to our knowledge, nobody has ever attempted to solve event calculus reasoning problems using first-order logic automated theorem proving (ATP) systems.