Theorist: A Logical Reasoning System for Defaults and Diagnosis

Abstract

We provide an introduction to Theorist, a logic programming system that uses a uniform deductive reasoning mechanism to construct explanations of observations in terms of facts and hypotheses. Observations, facts, and possible hypotheses are each sets of logical formulas that represent, respectively, a set of observations on a partial domain, a set of facts for which the domain is a model, and a set of tentative hypotheses which may be required to provide a consistent explanation of the observations.

Theorist has been designed to reason in a fashion similar to how we reason with and construct scientific theories. Rather than monotonically deduce theorems from a fixed logical theory, theorist distinguishes facts from hypotheses and attempts to use deduction to construct consistent theories for which the observations are logical consequences. A prototype, implemented in Prolog, demonstrates how diagnosis, default reasoning, and a kind of learning can all be based on the Theorist framework.