CHAPTER 13

The Discrete Event Calculus Reasoner

This chapter describes the Discrete Event Calculus Reasoner, which uses satisfiability (SAT) to solve event calculus problems. The program can be used to perform automated deduction, abduction, postdiction, and model finding. We discuss the architecture of the program and the encoding of SAT problems. We present some simple examples of how the program is used and then present a more complicated example. We discuss the language used to describe commonsense reasoning problems to the program. The Discrete Event Calculus Reasoner can be downloaded from decreasoner.sourceforge.net.

13.1 Discrete Event Calculus Reasoner Architecture

The architecture of the Discrete Event Calculus Reasoner is shown in ...

Get Commonsense Reasoning now with the O’Reilly learning platform.

O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.