Theorist

Abstract: Theorist is a framework for assumption-based logical reasoning. It can be used for many automated reasoning tasks in artificial intelligence, including default (nonmonotonic) reasoning and abduction. It has been applied to diagnosis problems, user modelling, recognition, multimedia presentations, and many others. This page provides an overview and points to papers.

Theorist was developed by David Poole, Randy Goebel and Romas Aleliunas when they were at the University of Waterloo, and has been followed up at both the University of Alberta (by Randy Goebel) and the University of British Columbia (by David Poole). Here is David Poole's personal story of Theorist; I am sure Randy and Romas would give other stories.

Contents

  1. Early History
  2. Default Reasoning vs Abduction
  3. Specificity
  4. Implementation
  5. Diagnosis
  6. Other Applications

Early History

Theorist started in 1984, when we thought that there must be something more straight forward, simpler and more intuitive than the (then) current ideas on non-monotonic reasoning. If we want to investigate making assumptions about the world in a logic-based framework (i.e., default reasoning), why not investigate making assumptions within a logic-based framework? So arose this idea of having assumption-based reasoning where the forms of the possible hypotheses, as well as the facts are provided by the user.

One night in the Grad Club at the University of Waterloo, David claimed that it was easy to write an interpreter for such a language in Prolog. The following morning there existed such an interpreter, which could run most of the standard non-monotonic reasoning examples. There begun the Theorist enterprise!

Early papers on Theorist were (I don't have online versions of these; they were written in troff (I am not even sure if troff still exists)):

For a more recent overview of Theorist from my perspective see the following paper, which looks at considering the question of who chooses the assumptions: whether it is an adversary (which leads to sceptical default reasoning similar to circumscription), oneself (leading to brave default reasoning and abductive views of design) or nature (leading to probabilities over assumptions - and probabilistic Horn abduction). The ideas behind this have been refined considerably and now appear as the Independent Choice Logic. See ongoing research.

Default Reasoning vs Abduction

It soon became clear that there were two different activities that were going on: explanation and prediction. Explanation is where the proposition to be explained (the explanandum) is an observation in the world, and we want to explain why this occurred (this is one formalization of what C.S.Peirce called abduction). The second, prediction is where the explanandum is unknown, and the problem is to determine whether to predict the explanandum or not (forming a formalization of default reasoning).

It became clear that these are quite different, but that they naturally fit together. A common reasoning strategy is, given an observation, to explain it (using normality and abnormality assumptions) and then make predictions (using normality assumptions).

The following two, closely related, papers investigate these two activities and their integration:

This second paper contains many examples of representational methodologies, and more detailed applications including user modelling, depiction, etc.

The following paper considered this distinction in the context of mixing design and recognition. It argues that one can do both design and recognition using either abduction or prediction, but that if you want to share a knowledge base then design and recognition should use opposite strategies.

More recent work on probabilistic Horn abduction has shown the close relationship between Bayesian conditioning with abduction followed by prediction. The probabilities in probabilistic Horn abduction give us a finer-grained control than just normality and abnormality assumptions, and also gives us a clean and simple model-theoretic semantics. My guess is that this is the right strategy: namely to have a ``causal'' knowledge base, to abduce to base causes and then predict from there. This idea has also been followed up by Craig Boutilier in formalizations of update.

Specificity

One of the early problems that we saw as a deficiency in the then current nonmonotonic reasoning formalisms was the desire to prefer more specific defaults over more general defaults.

One of the early Theorist papers tried to formalise this notion:

After playing with default reasoning, another problem became apparent, namely that default conclusions cannot be arbitrarily conjoined. There are quite simple cases where quite anomalous behaviours arise (adding seemingly irrelevant defaults affected the conclusions drawn from other defaults). This problem did not only arise in the Theorist framework (in which we were experimenting), but occurred in all of the default frameworks. There was a dual notion of specificity to that in the 1985 paper that could be defined. The following paper investigated this: A later paper formalised what was known in that 1985 paper: namely that we have to distinguish between background and contingent knowledge if we want to prefer more specific defaults to more general ones. This distinction lets us clearly formalise the variant of Kyburg's lottery paradox that arises in default reasoning. Where does this take us now? The 1985 paper was extended in some work by Simari and Loui, which didn't really solve the problem completely. The use of specificity has been investigated by other authors, particularly in the use of conditional logics for default reasoning (e.g., the work of Craig Boutilier). As far as I know, there is still not a good mix of conditionals and the more traditional default reasoning such as Theorist (although the work of Hector Geffner may come close).

Implementation

After the first initial interpreter (see the Poole, Goebel and Aleliunas paper above), I have built compilers from Theorist to Prolog that are similar (but designed independently) to the latter Prolog technology theorem provers built by Mark Stickel of SRI.

For an overview of the compiler see:

There is runnable compiler that is available (including a user manual and example programs).

I have also done some work with Nicholas Helft and Katsumi Inoue on answer extraction for sceptical prediction (membership in all extensions) and circumscription. See

There is also an X-window version of Theorist that is available from Randy Goebel (goebel@cs.ualberta.ca).

Diagnosis

One of the early applications for Theorist was in diagnosis. This was in the form of what is now called `abductive diagnosis' (see the Poole, Goebel and Aleliunas paper above).

This was also a time when there were other formalizations of diagnosis (e.g., Reiter's). One of the first papers to show (a) that these forms of diagnosis were different and (b) that they were closely related, was:

This paper showed how the consistency-based diagnosis can be considered as the completion of the abductive theory. Note that this paper implicitly assumed an acyclic causal structure, and only considered the propositional version. The following paper studied the case of having richer languages for both consistency-based diagnosis and abductive diagnosis (it is also interesting as the first paper to use the term "consistency-based diagnosis", as far as I know). The FGCS-88 paper was followed up by L. Console and D. Theseider Dupre and P. Torasso, "On the Relationship between Abduction and Deduction", Journal of Logic and Computation, 1(5), 661-690, 1991 [considering the abductive theory as a logic program], and by K. Konolige, "Abduction versus closure in causal theories", Artificial Intelligence 53(2-3), 255-272, 1992 [who considered the case of possibly cyclic theories, but gave up on local completion]. For more recent results on the propositional, acyclic equivalence see: This is still not the last answer on this problem. I am sure that there is a more formal local equivalence that can be proved for the non-propositional case (e.g., based on the IJCAI-89 paper).

Other Applications

There has been many applications built using Theorist. Early ones included educational diagnosis (hypothesising what errors students were making using a CAI system) and user modelling by Marlene Jones, and Jim Tubman.

Another application in user modelling was in using presupposition to ascribe belief, following up from work by Robert Mercer:

Last updated 14 August 1998, David Poole, poole@cs.ubc.ca