Reasoning in Event Calculus

Existing Systems

• Shanahan's EC planner - uses abductive logic programming
• Shanahan and Witkowski's EC planner - uses SAT solvers
• Mueller's DEC reasoner - uses SAT solvers

Using First-order ATP

• No known previous attempts to use ATP

• This work limited to DEC, but EC coming soon
• Produces humanly-understandable proofs
• Requires encoding techniques

• Not as powerful at SAT based systems