%% -*-LATEX-*-
\documentstyle[12pt]{article}
\pagestyle{myheadings}
\markright{A Theorist User's Guide}
\makeindex
\newtheorem{example}{Example}
\newtheorem{algorithm}{Algorithm}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{corollary}[theorem]{Corollary}
\newenvironment{proof}{\begin{quote} {\bf Proof: }}{$\Box$\end{quote}}
\newenvironment{prolog}{\begin{tabbing} \hbox{2cm}\=\hbox{1cm}\=\kill
}{\end{tabbing}}
\newcommand{\IF}{\ $:-$\\\>}
\newcommand{\AND}{,\\\>}
\title{Local Users Guide to Theorist\thanks{Copyright \copyright 1990
David Poole. All rights reserved.}}
\author{David Poole\\
Department of Computer Science,\\
University of British Columbia,\\
Vancouver, B. C., Canada V6T 1W5.\\
(604) 228-6254\\
poole@cs.ubc.ca}
\begin{document}
\maketitle
\begin{abstract}
Theorist \cite{poole:lf,pga,poole:ep,poole:meth} is a logical
reasoning system for default reasoning and diagnosis. It is based on
the idea of theory formation from a fixed set of possible hypotheses.
This is a users manual for a compiler from Theorist to Prolog. This
code is as described in \cite{poole:comp}.
This compiler should not be seen as ``the'' theorist system, but of
one (rather simple and naive) implementation of the Theoirst
framework. For example, it finds all explanations of the given goal,
and does no simplification of the explanations.
\end{abstract}
\tableofcontents
\section{Introduction}
This paper describes the use of the Theorist compiler.
To run this you must have access to a machine with Sicstus Prolog or
Quintus Prolog, or many other Prologs that are similar. It is meant to
be portable.
When you execute this, you can type Theorist commands at it. N.B. you can also
type Prolog queries at it; the Theorist commands will just be Prolog queries.
The source code is in the file
\begin{quote}\tt
theorist.tex
\end{quote}
This can either be consulted as a Prolog program or typeset as a Latex
document with only one character editing at the start of the file.
\section{Theorist Framework} \label{theorist}
Theorist \cite{poole:lf,pga,poole:ep,poole:meth} is a logical
reasoning system for default reasoning and diagnosis. It is based on
the idea of theory formation from a fixed set of possible hypotheses.
This implementation is of the version of Theorist described in
\cite{poole:comp}. The user provides three sets of first order
formulae
\begin{itemize}
\item[${\cal F}$] is a set of closed formulae called the {\em facts\/}.
These are intended to be true in the world being modelled.
\item[$\Delta$] is a set of formulae which
act as {\em possible hypotheses}, any ground instance of which
can be used in an explanation if consistent.
\item[$\cal C$] is a set of closed formulae taken as constraints.
The constraints restrict what can be hypothesised.
\end{itemize}
We assume that ${\cal F}\cup C$ is consistent.
\begin{definition} \em
a {\bf scenario} of ${\cal F},\Delta$ is a set $D \cup {\cal F}$ where
$D$ is a set of ground instances of elements
of $\Delta$ such that $D\cup {\cal F} \cup C$ is consistent.
\end{definition}
\begin{definition} \em
If $g$ is a closed formula then an {\bf explanation} of $g$ from ${\cal F},\Delta$
is a scenario of ${\cal F},\Delta$ which implies $g$.
\end{definition}
That is, $g$ is explainable from ${\cal F},\Delta$ if there is a set
$D$ of ground instances of elements of $\Delta$ such that
\begin{quote}
${\cal F} \cup D \models g$ and\\
${\cal F} \cup D \cup C$ is consistent
\end{quote}
${\cal F} \cup D$ is an explanation of $g$.
In other papers we have described how this can be the basis of default
and abductive reasoning systems
\cite{pga,poole:lf,poole:ep,poole:meth}. If we are using this for
prediction then possible hypotheses can be seen as defaults.
\cite{poole:lf} describes how this formalism can account for default
reasoning. This is also a framework for abductive reasoning where the
possible hypotheses are the base causes we are prepared to accept as
to why some observation was made \cite{pga,poole:ep,poole:meth}. We
will refer to possible hypotheses as defaults.
One restriction that can be made with no loss of expressive power
is to restrict possible hypotheses to just atomic forms with no
structure \cite{poole:lf}. This is done by naming the defaults.
\subsection{Syntax} \label{syntax}
The syntax of Theorist is designed to be of maximum flexibility.
Virtually any syntax is appropriate for wffs; the formulae are
translated into Prolog clauses without mapping out subterms. The
theorem prover implemented in the Compiler can be seen as a
non-clausal theorem prover \cite{poole:clausal}.
A {\bf wff\/} is a well formed formula made up of arbitrary
combination of implication (``$=>$'', ``$<-$''), disjunction
(``$or$'', ``;''), conjunction (``$and$'', ``$\&$'', ``,'') and
negation (``$not$'', ``\~{}'') of atomic symbols. Variables follow the
Prolog convention of being in upper case. There is no explicit
quantification.
A {\bf name\/} is an atomic symbol with only free variables as arguments.
The following gives the syntax of the Theorist code:
\begin{description}
\item[\bf fact]
$w.$\\
where $w$ is a wff,
means that $(\forall w) \in {\cal F}$; i.e., the universal closure of $w$ (all
variables universally quantified) is a fact.
\item[\bf default]
$d.$\\
where $d$ is a name,
means that $d\in \Delta$; i.e., $d$ is a default (a possible hypothesis).
\item[\bf default]
$d:w.$\\
where $d$ is a name and $w$ is a wff means $w$, with name $d$ can
be used in a scenario if it is consistent.
Formally it means $d\in \Delta$ and
$(\forall d\Rightarrow w) \in {\cal F}$.
\item[\bf constraint]
$w.$\\
where $w$ is a wff means $\forall w\in \cal C$.
\item[\bf prolog]
$p.$\\
where $p$ is an atomic symbol means any Theorist call to $p$ should
be proven in Prolog. This allows us to use built-in predicates of pure Prolog.
One should not expect Prolog's control predicates to work.
\item[\bf explain]
$w.$\\
where $w$ is an arbitrary wff,
gives all explanations of $\exists w$.
\item[\bf predict]
$w.$\\
where $w$ is a arbitrary ground wff,
returns ``yes'' if $w$ is in every extension of the defaults
and ``no'' otherwise.
If it returns ``yes'', a set of explanations is returned, if
it returns ``no'' then a scenario from which $g$ cannot be explained is
returned (this follows the framework of \cite{poole:ep}).
\end{description}
In this compiler these are interpreted as commands to Prolog.
The interface will thus be the Prolog interface with some predefined
commands.
\subsection{Compiler Directives}
The following are compiler directives:
\begin{description}
\item[\bf thconsult] {\em filename.}\\
reads commands from {\em filename}, and asserts and/or executes them.
\item[\bf thtrans] {\em filename.}\\
reads commands from {\em filename} and translates them into Prolog
code in the file {\em filename.pl}.
\item[\bf thcompile] {\em filename.}\\
reads commands from {\em filename}, translates them into the file
{\em filename.pl} and then compiles this file. ``explain'' commands in
the file are not interpreted.
\item[\bf dyn] {\em atom.}\\
should be in a file and declares that anything matching the atom
is allowed to be asked or added to. This should appear before any
use of the atom. This corresponds to the ``dynamic'' declaration of
Quintus Prolog. This is ignored except when compiling a file.
\end{description}
\subsection{Flags}
There are some other commands which allow one to set flags.
There are a number of Theorist options which can be set by flag declarations.
Flags, by default, are {\tt on}.
To set the flag $f$ to value $v$ you can issue the command
\begin{verse}
\bf set $f,v.$
\end{verse}
To find out the value of the flag $f$ issue the command
\begin{verse}
\bf flag $f,V.$
\end{verse}
You can reset the value of flag $f$ to its old value by
\begin{verse}
\bf reset $f.$
\end{verse}
The following flags currently do something:
\begin{description}
\item[ancestor\_search] when on means that we check for ancestors. If this is
off we lose completeness for the general formula case. If we are only using
Horn clauses then we do not need an ancestor search.
\item[loop\_check] this turns on a simple loop check. It makes the system
propositionally complete. The overhead for long loops may be very high though.
If your program runs very slowly, then turn it off. Often dramatic improvements
can be acheived in this way. It does not affect correctness of answers found.
\item[asserting] when on, this asserts the compiled clauses into Prolog,
when off it writes the Prolog form of the assertions onto the standard output.
This is mainly used internally, but is useful for seeing the output
of the Theorist compiler.
\end{description}
\section{Examples}
This section contain many examples. The best source of descriptions of
more examples is \cite{poole:meth}.
\subsection{Default Reasoning}
The following example is a file to do the birdsfly example
\begin{verbatim}
dyn flies(X).
dyn bird(X).
default birdsfly(X): flies(X) <- bird(X).
constraint not birdsfly(X) <- not flies(X).
default emusdontfly(X): not flies(X) <- emu(X) .
constraint not emusdontfly(X) <- flies(X).
constraint not birdsfly(X) <- emu(X).
fact bird(X) <- emu(X).
fact bird(X) <- robin(X).
fact bird(tweety).
fact emu(polly).
fact robin(cohen).
\end{verbatim}
The following is a session with theorist. We assume that the preceeding code
is in a file called ``birdsfly''.
\begin{verbatim}
theorist
Welcome to THEORIST 1.1 (5 October 88 version)
Any Problems see David Poole (poole@vision.ubc.cdn)
yes
| ?- thconsult birdsfly.
yes
| ?- explain flies(tweety).
Answer is flies(tweety)
Theory is [birdsfly(tweety)]
no
| ?- explain flies(polly).
no
| ?- explain flies(X).
Answer is flies(cohen)
Theory is [birdsfly(cohen)]
Answer is flies(tweety)
Theory is [birdsfly(tweety)]
no
| ?-
\end{verbatim}
Note that the explain command always finds all answers and
then returns with ``no''
(note that, for simplicity, it is a Prolog command).
Note also that we did a ``thconsult''; we could have also done a ``thcompile''
but it would have taken longer to load the file, but would have executed
quicker. Note also that if we had typed the commands at the terminal
(which is the same a ``thconsult''ing them, but not ``thcompile''ing them, then
we did not need the ``dyn'' declaration).
\subsection{Cancelling Defaults}
We can do a more complicated example to show cancelling defaults
\begin{verbatim}
dyn flies(X).
default mammals_dont_fly(X): not flies(X) <- mammal(X).
constraint not mammals_dont_fly(X) <- flies(X).
default bats_fly(X): flies(X) <- bat(X).
constraint not bats_fly(X) <- not flies(X).
constraint not mammals_dont_fly(X) <- bat(X).
default dead_things_dont_fly(X): not flies(X) <- dead(X).
constraint not dead_things_dont_fly(X) <- flies(X).
constraint not bats_fly(X) <- dead(X).
fact mammal(X) <- bat(X).
fact mammal(bruce).
fact bat(paul).
fact bat(dracula).
fact dead(dracula).
\end{verbatim}
Give that file we can do the following
\begin{verbatim}
| ?- explain flies(X).
Answer is flies(paul)
Theory is [bats_fly(paul)]
no
| ?- explain not flies(X).
Answer is not flies(bruce)
Theory is [mammals_dont_fly(bruce)]
Answer is not flies(dracula)
Theory is [dead_things_dont_fly(dracula)]
no
\end{verbatim}
\subsection{Disjunctive Answers}
Consider the following session
\begin{verbatim}
| ?- fact p(a) or p(b).
yes
| ?- fact p(X) and not q(f(X)) => q(X).
X = _38
| ?- explain p(X).
Answer is p(a) or p(b)
Theory is []
Answer is p(b) or p(a)
Theory is []
no
| ?- explain q(X).
Answer is q(a) or q(f(b)) or q(b) or q(f(a))
Theory is []
Answer is q(b) or q(f(a)) or q(a) or q(f(b))
Theory is []
Answer is q(f(a)) or q(f(b)) or q(b) or q(a)
Theory is []
Answer is q(f(b)) or q(f(a)) or q(a) or q(b)
Theory is []
no
\end{verbatim}
Note that we get different orderings from the disjunct. This is because the
linear resolution method used finds each of the proofs with each of the
disjuncts as head, and we do not simplify the results.
\subsection{circuits}
This specifies an abductive program for the full adder:
\begin{verbatim}
% a circuit diagnosis program for a full adder
dyn diag(X,Y).
dyn val(X,Y).
% to use add in facts about the input of the circuit, such as
% fact val(in(1, f1), off).
% fact val(in(2, f1), off).
% fact val(in(3, f1), off).
% to get it to explain the output of the circuit do something lik
% diag(on, on).
fact gate(x1, xor).
fact gate(x2, xor).
fact gate(a1, and).
fact gate(a2, and).
fact gate(o1, or).
fact conn(in(1, f1), in(1, x1)).
fact conn(in(1, f1), in(1, a1)).
fact conn(in(2, f1), in(2, x1)).
fact conn(in(2, f1), in(2, a1)).
fact conn(in(3, f1), in(2, x2)).
fact conn(in(3, f1), in(1, a2)).
fact conn(out(1, x1), in(1, x2)).
fact conn(out(1, x1), in(2, a2)).
fact conn(out(1, a1), in(2, o1)).
fact conn(out(1, a2), in(1, o1)).
fact conn(out(1, x2), out(1, f1)).
fact conn(out(1, o1), out(2, f1)).
fact val(in(N, Device), anything).
default ok(Device).
fact val(out(1, Device), Out1) <-
ok(Device),
gate(Device, Type),
ttable(Type, In1, In2, Out1),
val(in(1, Device), In1),
val(in(2, Device), In2).
default faulty(Device).
fact val(out(1, Device), Out1) <-
faulty(Device),
gate(Device, Type),
ttable(Type, In1, In2, Eout),
opp(Eout, Out1),
val(in(1, Device), In1),
val(in(2, Device), In2).
fact n(ok(Device)) <- faulty(Device).
fact opp(on, off).
fact opp(off, on).
fact ttable(and, on, on, on).
fact ttable(and, off, anything, off).
fact ttable(and, anything, off, off).
fact ttable(or, off, off, off).
fact ttable(or, on, anything, on).
fact ttable(or, anything, on, on).
fact ttable(xor, off, on, on).
fact ttable(xor, off, off, off).
fact ttable(xor, on, X, Y) <- opp(X, Y).
fact val(Y, Z) <-
ne(Z, anything),
conn(X, Y),
val(X, Z).
% define enough of "ne" - not equals - to make this work
ne(on,anything ).
ne(off,anything ).
fact n(val(X, off)) <- val(X, on).
fact diag(Out1, Out2) <-
val(out(1, f1), Out1 ),
val(out(2, f1), Out2 ).
\end{verbatim}
We can do circuit diagnosis:
\begin{verbatim}
| ?- thcompile cir2.
[compiling /ubc-lcvfs1/poole/theorist/cir2.pl...]
[cir2.pl compiled 10.133 sec 29,868 bytes]
yes
| ?- fact val(in(1, f1), off).
yes
| ?- fact val(in(2, f1), off).
yes
| ?- fact val(in(3, f1), off).
yes
| ?- explain diag(on,on).
Answer is diag(on,on)
Theory is [faulty(a2),ok(o1),faulty(x1),ok(x2)]
Answer is diag(on,on)
Theory is [faulty(a1),ok(o1),faulty(x1),ok(x2)]
Answer is diag(on,on)
Theory is [faulty(a1),ok(o1),faulty(x1),ok(x2)]
Answer is diag(on,on)
Theory is [ok(a1),ok(a2),faulty(o1),faulty(x1),ok(x2)]
Answer is diag(on,on)
Theory is [ok(a1),ok(a2),faulty(o1),faulty(x1),ok(x2)]
Answer is diag(on,on)
Theory is [faulty(a2),ok(o1),ok(x1),faulty(x2)]
Answer is diag(on,on)
Theory is [faulty(a2),ok(o1),ok(x1),faulty(x2)]
Answer is diag(on,on)
Theory is [faulty(a1),ok(o1),ok(x1),faulty(x2)]
Answer is diag(on,on)
Theory is [faulty(a1),ok(o1),ok(x1),faulty(x2)]
Answer is diag(on,on)
Theory is [ok(a1),ok(a2),faulty(o1),ok(x1),faulty(x2)]
Answer is diag(on,on)
Theory is [ok(a1),ok(a2),faulty(o1),ok(x1),faulty(x2)]
Answer is diag(on,on)
Theory is [ok(a1),ok(a2),faulty(o1),ok(x1),faulty(x2)]
Answer is diag(on,on)
Theory is [ok(a1),ok(a2),faulty(o1),ok(x1),faulty(x2)]
no
\end{verbatim}
\subsection{Prediction}
We predict what is in every extension.
\begin{verbatim}
default quaker_so_dove(X): quaker(X) => dove(X).
default republican_so_hawk(X): republican(X) => hawk(X).
default hawk_so_motivated(X): hawk(X) => motivated(X).
default dove_so_motivated(X): dove(X) => motivated(X).
default dove_so_peaceful(X): dove(X) => peaceful(X).
fact not (hawk(X) and dove(X)).
fact republican(ron).
fact quaker(george).
fact republican(dick).
fact quaker(dick).
\end{verbatim}
The following tracing shows how prediction works.
\begin{verbatim}
| ?- predict motivated(ron).
Yes, motivated(ron) is in all extensions.
Explanations are:
1: [hawk_so_motivated(ron),republican_so_hawk(ron)].
yes
| ?- predict hawk(ron).
Yes, hawk(ron) is in all extensions.
Explanations are:
1: [republican_so_hawk(ron)].
yes
| ?- predict motivated(dick).
Yes, motivated(dick) is in all extensions.
Explanations are:
1: [dove_so_motivated(dick),quaker_so_dove(dick)].
2: [hawk_so_motivated(dick),republican_so_hawk(dick)].
yes
| ?- predict hawk(dick).
No, hawk(dick) is not explainable from [quaker_so_dove(dick)].
yes
| ?- predict peaceful(dick).
No, peaceful(dick) is not explainable from [republican_so_hawk(dick)].
yes
| ?- predict peaceful(george).
Yes, peaceful(george) is in all extensions.
Explanations are:
1: [dove_so_peaceful(george),quaker_so_dove(george)].
yes
\end{verbatim}
\section{Conclusion}
Any comments about the product or the manual please direct to the author.
Have fun.
\section*{Acknowledgements}
This work could not have been done without the ideas,
criticism and feedback from Randy Goebel, Eric Neufeld,
Paul Van Arragon, Scott Goodwin and Denis Gagn\'e.
Thanks to Brenda Parsons and Amar Shan for valuable comments on
a previous version of this paper.
This research was supported under NSERC grant A6260.
\begin{thebibliography}{McDer80}
\bibitem[Poole84]{poole:clausal}
D. Poole,
``Making Clausal theorem provers Non-clausal'',
{\em Proc.\ CSCSI-84}. pp.~124-125.
\bibitem[Poole88]{poole:lf}
D. Poole,
``A Logical Framework for Default Reasoning'',
{\em Artificial Intelligence} 36(1), 27--47, 1988.
\bibitem[Poole89]{poole:ep}
D. Poole,
``Explanation and prediction: an architecture for default
and abductive reasoning'', {\em Computational Intelligence} 5(2),
97--110, 1989.
\bibitem[Poole90]{poole:meth}
D. Poole, ``A methodology for using a default and abductive reasoning
system'', {\em International Journal of Intelligent Systems} 5(5),
521--548, 1990.
\bibitem[Poole91]{poole:comp}
D. Poole,
``Compiling a Default Reasoning System into {Prolog}'',
{\em New Generation Computing}, 9(1), 3--38, 1991.
\bibitem[PGA87]{pga}
D.\ L.\ Poole, R.\ G.\ Goebel and R.\ Aleliunas,
``Theorist: A Logical Reasoning System for Defaults and Diagnosis'',
in N. Cercone and G. McCalla (Eds.)
{\it The Knowledge Frontier: Essays in the Representation of
Knowledge},
Springer Varlag, New York, 1987, pp.\ 331-352.
\end{thebibliography}
\end{document}