A tool for satisfiability-based commonsense reasoning in the event calculus

Abstract

We present a tool for commonsense reasoning in the classical logic event calculus using satisfiability. We describe the tool, which takes event calculus reasoning problems as input, encodes the problems as prepositional satisfiability problems, runs a satisfiability solver on the encoded problems, and produces solutions to the reasoning problems as output. We describe the encoding method and how various commonsense phenomena are expressed using the tool. We evaluate the tool on 14 benchmark commonsense reasoning problems for the event calculus, compare its performance with the causal calculator on eight zoo world test problems, and discuss two natural understanding applications built using the tool.