Skip Navigation

Journal of Logic and Computation 2004 14(5):703-730; doi:10.1093/logcom/14.5.703
© 2004 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrow Search for citing articles in:
ISI Web of Science (5)
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Mueller, E. T.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Original Article

Event Calculus Reasoning Through Satisfiability

Erik T. Mueller

IBM Thomas J. Watson Research Center, P.O. Box 704, Yorktown Heights, NY 10598 USA. E-mail: etm{at}us.ibm.com

We present an implemented method for encoding reasoning problems of a discrete version of the classical logic event calculus in propositional conjunctive normal form, enabling the problems to be solved efficiently by off-the-shelf complete satisfiability (SAT) solvers. We build on the previous encoding method of Shanahan and Witkowski, extending it to support causal constraints, concurrent events, determining fluents, effect axioms with conditions, events triggered by conditions, gradual change, incompletely specified initial situations, state constraints, and release from the commonsense law of inertia. We present an alternative classical logic axiomatization of the event calculus and prove its equivalence to a standard axiomatization for integer time. We describe our encoding method based on the alternative axiomatization and prove its correctness. We evaluate the method on 14 benchmark reasoning problems for the event calculus and compare performance with the causal calculator on eight problems in the zoo world domain.

Keywords: Commonsense reasoning, reasoning about action and change, event calculus, satisfiability, automated deduction

Received 17 June 2003.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?


This article has been cited by other articles:


Home page
 Lit Linguist ComputingHome page
E. T. Mueller
Modelling Space and Time in Narratives about Restaurants
Lit Linguist Computing, April 1, 2007; 22(1): 67 - 84.
[Abstract] [Full Text] [PDF]


Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.