1% this is both a latex file and a quintus prolog file
    2% the only difference is that the latex version comments out the following
    3% line:
    4
    5:- module(snark_theorist,[]).    6                          
    7:- module(snark_theorist).    8
    9/* 
   10\documentstyle[12pt,makeidx]{article}
   11\pagestyle{myheadings}
   12\markright{Theorist to Prolog (th2.tex)}
   13\makeindex
   14\newtheorem{example}{Example}
   15\newtheorem{algorithm}{Algorithm}
   16\newtheorem{theorem}{Theorem}
   17\newtheorem{lemma}[theorem]{Lemma}
   18\newtheorem{definition}{Definition}
   19\newtheorem{corollary}[theorem]{Corollary}
   20\newenvironment{proof}{\begin{quote} {\bf Proof: }}{$\Box$\end{quote}}
   21\newenvironment{prolog}{\begin{tabbing} \hbox{2cm}\=\hbox{1cm}\=\kill
   22    }{\end{tabbing}}
   23\newcommand{\IF}{\ $:-$\\\>}
   24\newcommand{\AND}{,\\\>}
   25\title{A Theorist to Prolog Compiler (th2.tex)\thanks{Copyright \copyright 1990
   26David Poole. All rights reserved.}}
   27\author{David Poole\\
   28Department of Computer Science,\\
   29University of British Columbia,\\
   30Vancouver, B.C. Canada V6T 1W5
   31(604) 228-6254\\
   32poole@cs.ubc.ca}
   33\begin{document}
   34\maketitle
   35\begin{abstract}
   36Artificial intelligence researchers have been designing representation
   37systems for default and abductive reasoning.
   38Logic Programming researchers have been working on techniques to improve
   39the efficiency of Horn Clause deduction systems.
   40This paper describes how {\em Theorist\/} can be
   41translated into Quintus Prolog.
   42The verbatim code is the actual running code.
   43
   44This should not be seen as {\em The Theorist System}, but rather
   45as one implementation of the Theorist framework. Theorist should be
   46seen as the idea that much reasoning can be done by theory formation
   47from a fixed set of possible hypotheses.
   48This implementation is based on a complete linear resolution theorem prover
   49which does not multiply out subterms. It also carries out incremental
   50consistency checking.
   51Note that there is nothing in this document which forces the control strategy
   52of Prolog. This is a compiler from Theorist to a Horn-clause reasoner
   53with negation as failure; nothing precludes any other search strategy
   54(e.g., dependency directed backtracking, constraint propagation).
   55This is intended to be a runnable specification, which runs fast
   56(e.g., for the common intersection between Theorist and Prolog (i.e., Horn
   57clauses) Theorist code runs about half the speed of compiled Quintus
   58Prolog code).
   59
   60This code is available electronically from the author.
   61\end{abstract}
   62\tableofcontents
   63\section{Introduction}
   64Many people in Artificial Intelligence have been working on default reasoning
   65and abductive diagnosis systems 
   66\cite{reiter80,mccarthy86,cox87,poole:lf}. The systems implemented so far
   67(eg., \cite{brewka86,lifschitz85,ginsberg87,pga}) are only prototypes or
   68have been developed in ways that cannot take full advantage in the
   69advances of logic programming implementation technology.
   70
   71Many people are working on making logic programming systems more efficient.
   72These systems, however, usually assume that the input is in the form of
   73Horn clauses with negation as failure. This paper shows how to implement
   74the default reasoning system Theorist \cite{poole:lf,pga}
   75by compiling its input into Horn clauses with negation as failure, thereby
   76allowing direct
   77use the advances in logic programming implementation technology.
   78Both the compiler and the compiled code can take advantage of 
   79these improvements.
   80
   81We have been running this implementation on standard
   82Prolog compilers (in particular Quintus Prolog) and it outperforms
   83all other default reasoning systems that the author is aware of.
   84It is, however, not restricted to the control structure of Prolog. There is
   85nothing in the compiled code which forces it to use Prolog's
   86search strategy.
   87Logic programming and other researchers are working on alternate
   88control structures which seem very appropriate for default 
   89and abductive reasoning.
   90Advances in parallel inference (e.g.,\ \cite{pie}),
   91constraint satisfaction \cite{dincbas,vanh} and dependency directed backtracking
   92\cite{dekleer86,doyle79,cox82} 
   93should be able to be directly applicable to the code produced by this compiler.
   94
   95We are thus effecting a clear
   96distinction between the control and logic of our default reasoning systems
   97\cite{kowalski}. We can let the control people concentrate on efficiency
   98of Horn clause systems, and these will then be directly applicable to
   99those of us building richer representation systems.
  100The Theorist system has been designed to allow maximum flexibility in
  101control strategies while still giving us the power of assumption-based
  102reasoning that are required for default and abductive reasoning.
  103
  104This is a step towards having representation and reasoning systems
  105which are designed for correctness being able to use the most
  106efficient of control
  107strategies, so we can have the best of expressibility and efficiency.
  108\section{Theorist Framework} \label{theorist}
  109
  110Theorist \cite{poole:lf,pga} is a logical reasoning system for default reasoning
  111and diagnosis. It is based on the idea of theory formation from a fixed
  112set of possible hypotheses.
  113
  114This implementation is of the version of Theorist described in \cite{poole:lf}.
  115The user provides three sets of first order formulae
  116\begin{itemize}
  117\item[${\cal F}$] is a set of closed formulae called the {\em facts\/}.
  118These are intended to be true in the world being modelled.
  119\item[$\Delta$] is a set of formulae which
  120act as {\em possible hypotheses}, any ground instance of which
  121can be used in an explanation if consistent.
  122\item[$\cal C$] is a set of closed formulae taken as constraints.
  123The constraints restrict what can be hypothesised.
  124\end{itemize}
  125
  126We assume that ${\cal F}\cup C$ is consistent.
  127
  128\begin{definition} \em
  129a {\bf  scenario} of ${\cal F},\Delta$ is a set $D \cup {\cal F}$ where
  130$D$ is a set of ground instances of elements
  131of $\Delta$ such that $D\cup {\cal F} \cup C$ is consistent.
  132\end{definition}
  133
  134\begin{definition} \em
  135If $g$ is a closed formula then an {\bf explanation} of $g$ from ${\cal F},\Delta$
  136is a  scenario of ${\cal F},\Delta$ which implies $g$.
  137\end{definition}
  138That is, $g$ is explainable from ${\cal F},\Delta$ if there is a set
  139$D$ of ground instances of elements of $\Delta$ such that
  140\begin{quote}
  141${\cal F} \cup D \models g$ and\\
  142${\cal F} \cup D \cup C$ is consistent
  143\end{quote}
  144${\cal F} \cup D$ is an explanation of $g$.
  145
  146In other papers we have described how this can be the basis of
  147default and abductive reasoning systems \cite{pga,poole:lf,poole:dc,poole:dd}.
  148If we are using this for prediction then possible hypotheses can be seen
  149as defaults. \cite{poole:lf} describes how this formalism can account
  150for default reasoning. This is also a framework for abductive reasoning
  151where the possible hypotheses are the base causes we are prepared
  152to accept as to why some observation was made \cite{pga}.
  153We will refer to possible hypotheses as defaults.
  154
  155One restriction that can be made with no loss of expressive power
  156is to restrict possible hypotheses to just atomic forms with no
  157structure \cite{poole:lf}. This is done by naming the defaults.
  158\subsection{Syntax} \label{syntax}
  159The syntax of Theorist is designed to be of maximum flexibility.
  160Virtually any syntax is appropriate for wffs; the formulae are translated
  161into Prolog clauses without mapping out subterms. The theorem
  162prover implemented in the Compiler can be seen as a non-clausal theorem
  163prover \cite{poole:clausal}.
  164
  165A {\em wff\/} is a well formed formula made up of arbitrary combination of
  166equivalence (``=='', ``$equiv$''),
  167implication (``$=>$'', ``$<-$''), disjunction (``$or$'', ``;''),
  168conjunction (``$and$'', ``$\&$'', ``,'') and negation (``$not$'', ``\~{}'')
  169of atomic symbols. Variables follow the Prolog convention
  170of being in upper case. There is no explicit quantification.
  171
  172A {\em name\/} is an atomic symbol with only free variables as arguments.
  173
  174The following gives the syntax of the Theorist code:
  175\begin{description}
  176\item[\bf fact]
  177$w.$\\
  178where $w$ is a wff,
  179means that $(\forall w) \in {\cal F}$; i.e., the universal closure of $w$ (all
  180variables universally quantified) is a fact.
  181\item[\bf default]
  182$d.$\\
  183where $d$ is a name,
  184means that $d\in \Delta$; i.e., $d$ is a default (a possible hypothesis).
  185\item[\bf default]
  186$d:w.$\\
  187where $d$ is a name and $w$ is a wff means $w$, with name $d$ can
  188be used in a scenario if it is consistent.
  189Formally it means $d\in  \Delta$ and
  190$(\forall d\Rightarrow w) \in {\cal F}$.
  191\item[\bf constraint]
  192$w.$\\
  193where $w$ is a wff means $\forall w\in \cal C$.
  194\item[\bf prolog]
  195$p.$\\
  196where $p$ is an atomic symbol means any Theorist call to $p$ should
  197be proven in Prolog. This allows us to use built-in predicates of pure Prolog.
  198One should not expect Prolog's control predicates to work.
  199\item[\bf explain]
  200$w.$\\
  201where $w$ is an arbitrary wff,
  202gives all explanations of $\exists w$.
  203\item[\bf predict]
  204$w.$\\
  205where $w$ is a arbitrary ground wff,
  206returns ``yes'' if $w$ is in every extension of the defaults
  207and ``no'' otherwise.
  208If it returns ``yes'', a set of explanations is returned, if
  209it returns ``no'' then a scenario from which $g$ cannot be explained is
  210returned (this follows the framework of \cite{poole:dc}).
  211
  212\end{description}
  213
  214In this compiler these are interpreted as commands to Prolog.
  215The interface will thus be the Prolog interface with some predefined
  216commands.
  217
  218\subsection{Compiler Directives}
  219The following are compiler directives:
  220\begin{description}
  221\item[\bf thconsult] {\em filename.}\\
  222reads commands from {\em filename}, and asserts and/or executes them.
  223\item[\bf thtrans] {\em filename.}\\
  224reads commands from {\em filename} and translates them into Prolog
  225code in the file {\em filename.pl}.
  226\item[\bf thcompile] {\em filename.}\\
  227reads commands from {\em filename}, translates them into the file
  228{\em filename.pl} and then compiles this file. ``explain'' commands in
  229the file are not interpreted.
  230\item[\bf dyn] {\em atom.}\\
  231should be in a file and declares that anything matching the atom
  232is allowed to be asked or added to. This should appear before any
  233use of the atom. This corresponds to the ``dynamic'' declaration of
  234Quintus Prolog. This is ignored except when compiling a file.
  235\end{description}
  236There are some other commands which allow one to set flags. See section
  237\ref{flags} for more detail on setting checking and resetting flags.
  238
  239\section{Overview of Implementation}
  240In this section we assume that we have a deduction system 
  241(denoted $\vdash$) which has the 
  242following properties (such a deduction system will be defined in the
  243next section):
  244\begin{enumerate}
  245\item It is sound (i.e., if $A\vdash g$ then $A\models g$).
  246\item It is complete in the sense that if $g$ follows from a consistent
  247set of formulae, then $g$ can be proven. I.e., if $A$ is consistent and
  248$A\models g$ then $A\vdash g$.
  249\item If $A\vdash g$ then $A\cup B\vdash g$; i.e., adding in extra facts will
  250not prevent the system from finding a proof which previously existed.
  251\item It can return instances of predicates which were used in the proof.
  252\end{enumerate}
  253
  254The basic idea of the implementation follows the definition on explainability:
  255\begin{algorithm}\em \label{basic-alg}
  256to explain $g$
  257\begin{enumerate}
  258\item try to prove $g$ from ${\cal F}\cup \Delta$. If no proof exists, then
  259$g$ is not explainable. If there is a proof, let $D$ be the set of instances of
  260elements of $\Delta$ used in the proof. We then know
  261\[{\cal F}\cup D \models g\]
  262by the soundness of our proof procedure.
  263\item show $D$ is consistent with ${\cal F}\cup C$
  264by failing to prove it is inconsistent.
  265\end{enumerate}
  266\end{algorithm}
  267
  268\subsection{Consistency Checking}
  269The following two theorems are important for implementing the consistency
  270check:
  271\begin{lemma} \label{incremantal}
  272If $A$ is a consistent set of formulae and
  273$D$ is a finite set of ground instances of possible hypotheses, then
  274if we impose arbitrary ordering on the elements of $D=\{d_1,...,d_n\}$
  275\begin{center}
  276$A\cup D$ is inconsistent\\if and only if\\
  277there is some $i$, $1\leq i \leq n$ such that
  278$A\cup \{d_1,...,d_{i-1}\}$ is consistent and\\
  279$A\cup \{d_1,...,d_{i-1}\}\models \neg d_i$.
  280\end{center}
  281\end{lemma}
  282\begin{proof}
  283If $A \cup D $ is inconsistent there is some least $i$ such
  284that $A\cup \{d_1,...,d_i\}$ is inconsistent. Then we must have
  285$A\cup \{d_1,...,d_{i-1}\}$ is consistent (as $i$ is minimal) and
  286$A\cup \{d_1,...,d_{i-1}\}\models \neg d_i$ (by inconsistency).
  287\end{proof}
  288
  289This lemma says that we can show that ${\cal F}\cup C \cup \{d_1,...,d_n\}$ is 
  290consistent if we can show that for all $i$, $1\leq i \leq n$,
  291${\cal F}\cup C\cup \{d_1,...,d_{i-1}\}\not\vdash \neg d_i$.
  292If our theorem prover can show there is no proof of all of
  293the $\neg d_i$, then we have consistency.
  294
  295This lemma indicates that we can implement Theorist by incrementally failing to
  296prove inconsistency. We need to try to prove the negation of the
  297default in the context of all previously assumed defaults.
  298Note that this ordering is arbitrary.
  299
  300The following theorem expands on how explainability can be computed:
  301\begin{theorem} \label{consisthm}
  302If ${\cal F} \cup C$ is consistent,
  303$g$ is explainable from ${\cal F},\Delta$ if and only if there is a ground
  304proof of $g$ from ${\cal F}\cup D$ where $D=\{d_1,...,d_n\}$
  305is a set of ground instances
  306of elements of $\Delta$ such that
  307${\cal F} \wedge C \wedge \{d_1,...,d_{i-1}\}\not\vdash \neg d_i$
  308for all $i,1\leq i \leq n$.
  309\end{theorem}
  310\begin{proof}
  311If $g$ is explainable from ${\cal F},\Delta$, there is a set $D$ of ground instances
  312of elements of $\Delta$ such that ${\cal F}\cup D \models g$ and ${\cal F} \cup D \cup C$
  313is consistent. So there is a ground proof of $g$ from ${\cal F} \cup D$.
  314By the preceding lemma
  315${\cal F}\cup D \cup C$ is consistent so there can be no sound proof
  316of inconsistency. That is, we cannot prove
  317${\cal F} \wedge C \wedge \{d_1,...,d_{i-1}\}\vdash \neg d_i$ for any $i$.
  318\end{proof}
  319
  320This leads us to the refinement of algorithm \ref{basic-alg}:
  321\begin{algorithm} \em
  322to explain $g$ from ${\cal F},\Delta$
  323\begin{enumerate}
  324\item Build a ground proof of $g$ from ${\cal F}\cup \Delta$. Make $D$ 
  325the set of instances of elements of $\Delta$ used in the proof.
  326\item For each $i$, try to prove $\neg d_i$ from ${\cal F} \wedge C
  327\wedge \{d_1,...,d_{i-1}\}$. If all
  328such proofs fail, $D$ is an explanation for $g$.
  329\end{enumerate}
  330\end{algorithm}
  331
  332Note that the ordering imposed on the $D$ is arbitrary. A sensible one is
  333the order in which the elements of $D$ were generated. Thus when
  334a new hypothesis is used in the proof, we try to prove its negation from
  335the facts and the previously used hypotheses. These proofs are independent
  336of the original proof and can be done as they are generated
  337as in negation as failure (see section \ref{incremental}), or can be done
  338concurrently.
  339
  340\subsection{Variables}
  341Notice that theorem \ref{consisthm} says that $g$ is explainable
  342if there is a ground proof. There is a problem that arises
  343to translate the preceding algorithm (which assumes ground proofs)
  344into an algorithm which does not build ground proofs (eg., a standard
  345resolution theorem prover), as we may have variables in the forms
  346we are trying to prove the negation of.
  347
  348A problem arises
  349when there are variables in the $D$ generated.
  350 Consider the following example:
  351\begin{example}\em
  352Let $ \Delta = \{p(X)\}$. That is, any instance of $p$ can be used if it is
  353consistent.
  354Let ${\cal F} = \{ \forall Y (p(Y) \Rightarrow g), \neg p(a)\}$. That is, $g$ is
  355true if there is a $Y$ such that $p(Y)$.
  356
  357According to our semantics,
  358$g$ is explainable with the explanation $\{p(b)\}$,
  359which is consistent with ${\cal F}$ (consider the interpretation $I=\{\neg p(a),p(b)\}$
  360on the domain $\{a,b\}$), and implies $g$.
  361
  362However,
  363if we try to prove $g$, we generate $D=\{p(Y)\}$ where $Y$ is free
  364(implicitly a universally quantified variable).
  365The existence of the fact $\neg p(a)$ should not make it
  366inconsistent, as we want $g$ to be explainable.
  367\end{example}
  368\begin{theorem}
  369It is not adequate to only consider interpretations in the
  370Herbrand universe of ${\cal F}\cup \Delta \cup C$ to determine explainability.
  371\end{theorem}
  372\begin{proof}
  373consider the example above; the Herbrand universe is just
  374the set $\{a\}$. Within this domain there is no consistent 
  375explanation to explain $g$.
  376\end{proof}
  377
  378This shows that Herbrand's theorem is not applicable to the whole system.
  379It is, however, applicable to each of the deduction steps \cite{chang}.
  380
  381So we need to generate a ground proof of $g$. This leads us to:
  382
  383\begin{algorithm} \em \label{det-alg}
  384To determine if $g$ is explainable from ${\cal F},\Delta$
  385\begin{enumerate}
  386\item generate a proof of $g$ using elements of ${\cal F}$ and $ \Delta$ as axioms.
  387Make $D_0$ the set of instances of $ \Delta$ used in the proof;
  388\item form $D_1$ by replacing free variables in $D_0$ with unique constants;
  389\item add $D_1$ to ${\cal F}$ and try to prove an inconsistency (as in the
  390previous case). If a
  391complete search for a proof fails, $g$ is explainable.
  392\end{enumerate}
  393\end{algorithm}
  394
  395This algorithm can now be directly implemented by a resolution theorem prover.
  396
  397\begin{example}\em
  398Consider ${\cal F}$ and $\Delta$ as in example 1 above.
  399If we try to prove $g$, we use the hypothesis instance $p(Y)$.
  400This means that $g$ is provable from any instance of $p(Y)$.
  401To show $g$ cannot be explained, we must show that all of the instances
  402are inconsistent. The above algorithm says
  403we replace $Y$ with a constant $\beta$.
  404$p(\beta)$ is consistent with the facts.
  405Thus we can show $g$ is explainable.
  406\end{example}
  407
  408\subsection{Incremental Consistency Checking} \label{incremental}
  409Algorithm \ref{det-alg} assumed that we only check consistency at the end.
  410We cannot replace free variables by a unique constant until the end
  411of the computation.
  412This algorithm can be further refined by considering cases
  413where we can check consistency at the time the hypothesis is generated.
  414
  415Theorem \ref{incremantal} shows that we can check consistency incrementally
  416in whatever order we like. The problem is to determine whether we have
  417generated the final version of a set of hypotheses.
  418If there are no variables in our set of hypotheses, then we can check
  419consistency as soon as they are generated.
  420If there are variables in a hypothesis, then we cannot guarantee that the
  421form generated will be the final form of the hypothesis.
  422\begin{example}\em
  423Consider the two alternate set of facts:
  424\begin{eqnarray*}
  425\Delta&=\{&p(X)\ \}\\
  426{\cal F}_1&=\{&\forall X \ p(X) \wedge q(X) \Rightarrow g,\\
  427&&\neg p(a),\\
  428&&q(b) \ \}\\
  429{\cal F}_2&=\{&\forall X \ p(X) \wedge q(X) \Rightarrow g,\\
  430&&\neg p(a),\\
  431&&q(a) \ \}
  432\end{eqnarray*}
  433Suppose we try to explain $g$ by first explaining $p$ and then explaining $q$.
  434Once we have generated the hypothesis $p(X)$, we have not enough information to
  435determine whether the consistency check should succeed or fail.
  436The consistency check for ${\cal F}_1$ should succeed (i.e, we should conclude
  437with a consistent instance, namely $X=b$), but the 
  438consistency check for ${\cal F}_2$ should fail (there is no consistent value
  439for the $X$ which satisfies $p$ and $q$).
  440We can only determine the consistency after we have proven $q$.
  441\end{example}
  442
  443There seems to be two obvious solutions to this problem,
  444the first is to allow the consistency check to return constraints on the
  445values (eg., \cite{edmonson}). The alternate (and simpler) solution is
  446to delay the evaluation of the consistency check until all of the variables
  447are bound (as in \cite{naish86}), or until we know that the variables
  448cannot be bound any more. In particular we know that a variable cannot be
  449bound any more at the end of the computation.
  450
  451The implementation described in this paper
  452does the simplest form of incremental consistency checking, namely it computes
  453consistency immediately for those hypotheses with no variables and delays
  454consistency checking until the end for hypotheses containing variables
  455at the time they are generated.
  456\section{The Deduction System} \label{deduction}
  457
  458This implementation is based on linear resolution \cite{chang,loveland78}.
  459This is complete in the
  460sense that if $g$ logically follows from some {\em consistent} set of
  461clauses $A$, then there is a linear resolution proof of $g$ from $A$.
  462
  463SLD resolution of Prolog \cite{lloyd} can be seen as linear resolution with
  464the contrapositive and ancestor search removed.
  465
  466To implement linear resolution in Prolog, we add two things
  467\begin{enumerate}
  468\item we use the contrapositive of our clauses. If we have the clause
  469\begin{verse}
  470$L_1 \vee L_2 \vee ... \vee L_n$
  471\end{verse}
  472then we create the $n$ rules
  473\begin{verse}
  474$L_1 \leftarrow \neg L_2 \wedge ... \wedge \neg L_n$\\
  475$L_2 \leftarrow \neg L_1 \wedge \neg L_3 \wedge ... \wedge \neg L_n$\\
  476$...$\\
  477$L_n \leftarrow \neg L_1 \wedge ... \wedge \neg L_{n-1}$
  478\end{verse}
  479as rules. Each of these can then be used to prove the left hand literal
  480if we know the other literals are false. Here we are treating the negation
  481of an atom as a different Prolog atom (i.e.,\ we treat $\neg p(\overline{X})$
  482as an atom $notp(\overline{X})$).
  483\item the ancestor cancellation rule. While trying to prove $L$ we can assume
  484$\neg L$. We have a subgoal proven if it unifies with the negation of
  485an ancestor in the proof tree.
  486This is an instance of proof by contradiction. We can see this as assuming
  487$\neg L$ and then when we have proven $L$ we can discharge the assumption.
  488\end{enumerate}
  489
  490One property of the deduction system that we want is the ability to
  491implement definite clauses with a constant factor overhead over
  492using Prolog. One way to do this is to keep two lists of ancestors
  493of any node: $P$ the positive (non negated atoms) ancestors
  494and $N$ the negated ancestors. Thus for a positive subgoal we
  495only need to search for membership in $N$ and for a negated subgoal we only
  496need to search $P$.
  497When we have definite clauses, there are no negated subgoals, and so 
  498$N$ is always empty. Thus the ancestor search always consists
  499of checking for membership in an empty list. The alternate
  500contrapositive form of the clauses are never used.
  501
  502Alternate, more complicated ways to do ancestor search
  503have been investigated \cite{poole:grace}, but this implementation
  504uses the very simple form given above.
  505Another tempting possibility is to use the near-Horn resolution
  506of \cite{loveland87}. More work needs to be done on this area.
  507\subsection{Disjunctive Answers}
  508For the compiler to work properly we need to be able to return
  509disjunctive answers. We need disjunctive answers for the case
  510that we can prove only a disjunctive form of the query.
  511
  512For example, if we can prove $p(a)\vee p(b)$ for the
  513query $?p(X)$, then we want the answer $X= a$ or $b$.
  514This can be seen as ``if the answer is not $a$ then the
  515answer is $b$''.
  516
  517To have the answer $a_1\vee...\vee a_n$, we need to have a proof
  518of ``If the answer is not $a_1$ and not $a_2$ and ... and not $a_{n-1}$
  519then the answer is $a_n$''.
  520We collect up conditions on the proof of
  521alternate answers that we are assuming are not true in order to have
  522the disjunctive answer.
  523
  524This is implemented by being able to assume the negation of the top level
  525goal as long as we add it to the set of answers. To do this we carry a list
  526of the alternate disjuncts that we are assuming in proving the top level goal.
  527\subsection{Conversion to Clausal Form}
  528It is desirable that we can convert an
  529arbitrary well formed formula into clausal (or rule) form
  530without mapping out subterms. Instead of distributing, we do this by
  531creating a new term to refer to the disjunct.
  532
  533Once a formula is in negation normal form, then the normal way 
  534to convert to clausal form \cite{chang} is to
  535convert something of the form
  536\[\alpha \vee (\beta \wedge \gamma)\]
  537by distribution into
  538\[(\alpha \vee \beta) \wedge (\alpha \vee \gamma)\]
  539and so mapping out subterms.
  540
  541The alternate \cite{poole:clausal} is to create a new relation $p$ parameterised
  542with the variables in common with $\alpha$ and $\beta \wedge \gamma$.
  543We can then replace $\beta \wedge \gamma$ by $p$ and then add
  544\[(\neg p \vee \beta)\wedge (\neg p \vee \gamma)\]
  545to the set of formulae.
  546
  547This can be embedded into the compiler by using
  548Prolog ``or'' instead of actually building the $p$. 
  549(Alternatively we can define ``or'' by defining the
  550clause $(p;q)\leftarrow p$ and $(p;q)\leftarrow q$.)
  551We build up the clauses so that the computation runs
  552without any multiplying out of subterms.
  553This is an instance of the general procedure of making clausal
  554theorem provers into non-clausal theorem provers \cite{poole:clausal}.
  555\section{Details of the Compiler}
  556In this section we give actual code which converts
  557Theorist code into Prolog code.
  558The compiler is described here in a bottom up fashion; from the
  559construction of the atoms to compilation of general formulae.
  560
  561The compiler is written in Prolog and the
  562target code for the compiler is Prolog code (in particular Horn
  563clauses with negation as failure). There are no ``cuts'' or other
  564non-logical ``features'' of Prolog which depend on Prolog's
  565search strategy in the compiled code.
  566Each Theorist wff gets locally translated into a set of
  567Prolog clauses.
  568\subsection{Target Atoms}
  569For each Theorist predicate symbol $r$ there are 4 target predicate
  570symbols, with the following informal meanings:
  571\begin{description}
  572\item[prv\_tru\_r] meaning $r$ can be proven from the facts and the constraints.
  573\item[prv\_not\_r] meaning $\neg r$ can be proven from the facts 
  574and the constraints.
  575\item[ex\_tru\_r] meaning $r$ can be explained from ${\cal F},\Delta$.
  576\item[ex\_not\_r] meaning $\neg r$ can be explained from ${\cal F},\Delta$.
  577\end{description}
  578
  579The arguments to these built predicate symbols will contain all
  580of the information that we need to prove or explain instances of the source
  581predicates.
  582\subsubsection{Proving}
  583For relation $r(-args-)$ in the source code we want to produce object
  584code which says that $r(-args-)$ (or its negation)
  585can be proven from the facts and constraints and the current set
  586of assumed hypotheses.
  587
  588For the source relation
  589\[r( - args -)\]
  590(which is to mean that $r$ is a relation with $-args-$ being the
  591sequence of its arguments),
  592we have the corresponding target relations
  593\[prv\_tru\_r( - args - , Ths, Anc)\]
  594\[prv\_not\_r( - args - , Ths, Anc)\]
  595which are to mean that $r$ (or $\neg r$) can be proven
  596>from the facts and ground hypotheses
  597$Ths$ with ancestor structure $Anc$.
  598These extra arguments are:
  599
  600\begin{description}
  601\item $Ths$ is a list of ground defaults.
  602These are the defaults we have already assumed and so define the context in
  603which to prove $r(-args-)$.
  604\item $Anc$ is a structure of the form $anc(P,N)$ where $P$ and $N$ are
  605lists of source atoms. Interpreted procedurally,
  606$P$ is the list of positive (not negated) ancestors of
  607the goal in a proof and $N$ is the list of negated ancestors
  608in a proof. As described in section \ref{deduction} we conclude some goal
  609if it unifies with its negated ancestors.
  610\end{description}
  611
  612Declaratively,
  613\[prv\_tru\_r( - args - , Ths, anc(P,N))\]
  614means
  615\[{\cal F}\cup Ths \cup \neg P \cup N \models r(-args-)\]
  616
  617\subsubsection{Explaining}
  618There are two target relations for explaining associated with
  619each source relation $r$. These are $ex\_tru\_r$ and $ex\_not\_r$.
  620
  621For the source relation:
  622\[r( - args -)\]
  623we have two target new relations for explaining $r$:
  624\[ex\_tru\_r( - args - , Ths, Anc, Ans)\]
  625\[ex\_not\_r( - args - , Ths, Anc, Ans)\]
  626These mean that $r(-args-)$ (or $\neg r(-args-)$) can be explained, with
  627\begin{description}
  628\item[$Ths$] is the structure of the incrementally built hypotheses
  629used in explaining $r$. There are two statuses of hypotheses we
  630use; one the defaults that are ground and so can be proven
  631consistent at the time of generation;
  632the other the hypotheses with free variables at the time they
  633are needed in the proof, for which we defer consistency
  634checking (in case the free variables get instantiated later in the proof).
  635$Ths$ is essentially
  636two difference lists, one of the ground defaults already
  637proven consistent and one of the
  638deferred defaults. $Ths$ is of the form
  639\[ths(T_1,T_2,D_1,D_2)\]
  640which is to mean that $T_1$ is the consistent hypotheses before
  641we try to explain $r$, and
  642and $T_2$ is the list of consistent hypotheses which includes
  643$T_1$ and those hypotheses assumed to explain $r$.
  644Similarly, $D_1$ is the list of deferred hypotheses before we consider the goal
  645and $D_2$ is the list of resulting deferred hypotheses used in explaining $r$.
  646
  647\item[$Anc$] contains the ancestors of the goal. As in the previous case,
  648this is a pair of the form
  649$anc(P,N)$ where $P$ is the list of positive ancestors of the goal,
  650and $N$ is the list of negated ancestors of the goal.
  651
  652\item[$Ans$] contains the answers we are considering in difference list form
  653$ans(A_1,A_2)$, where $A_1$ is the answers before
  654proving the goal, and $A_2$ is the answers after proving the goal.
  655\end{description}
  656
  657The semantics of
  658\[ex\_tru\_r(-args-,ths(T_1,T_2,D_1,D_2),anc(P,N),ans(A_1,A_2))\]
  659is defined by
  660\[{\cal F}\cup T_2 \cup D_2 \cup \neg P \cup N \cup A_2 \models r(-args-) \]
  661where $T_1\subseteq T_2$, $D_1\subseteq D_2$ and $A_1\subseteq A_2$, and
  662such that
  663\[{\cal F}\cup T_2 \hbox{ is consistent}\]
  664
  665\subsubsection{Building Atoms}
  666The procedure {\em new\_lit$($Prefix, Reln, Newargs, Newreln\/}$)$ constructs
  667a new atom, $Newreln$, with predicate symbol made up of
  668$Prefix$ prepended to the
  669predicate symbol of $Reln$, and taking as arguments the arguments of $Reln$
  670together with $Newargs$.
  671For example,
  672\begin{quote}
  673?-- new\_lit(`ex\_tru\_`,reln(a,b,c),[T,A,B],N).
  674\end{quote}
  675yields
  676\begin{quote}
  677N = ex\_tru\_reln(a,b,c,T,A,B)
  678\end{quote}
  679
  680The procedure is defined as follows\footnote{The verbatim code
  681is the actual implementation code given in standard Edinburgh notation.
  682I assume that the reader is familiar with such notation.}:
  683\index{new\_lit}
  684\index{add\_prefix}
  685\begin{verbatim} */
  686
  687
  688new_lit(_Prefix, Reln, _NewArgs, NewReln) :- is_thbuiltin(Reln),!,NewReln=Reln.
  689
  690new_lit(Prefix, Reln, NewArgs, NewReln) :-
  691   Reln =.. [Pred | Args],
  692   add_prefix(Prefix,Pred,NewPred),
  693   append(Args, NewArgs, AllArgs),
  694   NewReln =.. [NewPred | AllArgs].
  695
  696add_prefix(Prefix,Pred,NewPred) :-
  697   string_codes(Prefix,PrefixC),
  698   name(Pred,PredName),
  699   append(PrefixC, PredName, NewPredName),
  700   name(NewPred,NewPredName).
  701
  702
  703/* \end{verbatim}
  704\subsection{Compiling Rules}
  705The next simplest compilation form we consider is the intermediate form
  706called a ``rule''.
  707Rules are statements of how to conclude
  708the value of some relation. Each Theorist fact corresponds to a number
  709of rules (one for each literal in the fact).
  710Each rule gets translated into Prolog rules to explain
  711and prove the head of the rule. 
  712
  713Rules use the intermediate form called a ``literal''.
  714A literal is either an atomic symbol or of the form $n(A)$ where $A$ is
  715an atomic symbol.
  716A rules is either a literal or
  717of the form {\em H $\leftarrow$ Body} (written ``{\tt if(H,Body)}'')
  718where $H$ is a literal
  719and $Body$ is a conjunction and disjunction of literals.
  720
  721We translate rules of the form
  722\[h(-x-) \leftarrow b_1(-x_1-), b_2(-x_2-), ... ,b_N(-x_n-);\]
  723into the internal form (assuming that $h$ is not negated)
  724\begin{prolog}
  725$ex\_tru\_h(-x-,ths(T_0,T_n,D_0,D_n), anc(P,N), ans(A_0,A_n)) $\IF
  726$ex\_tru\_b_1(-x_1-,ths(T_0,T_1,D_0,D_1), anc([h(-x-)|P],N), ans(A_0,A_1))$\AND
  727$ex\_tru\_b_2(-x_2-,ths(T_1,T_2,D_1,D_2), anc([h(-x-)|P],N), ans(A_1,A_2))$\AND
  728$...$\AND
  729$ex\_tru\_b_n(-x_n-,ths(T_{n-1},T_n,D_{n-1},D_n), anc([h(-x-)|P],N),
  730ans(A_{n-1},A_n)).$
  731\end{prolog}
  732That is, we explain $h$ if we explain each of the $b_i$,
  733accumulating the explanations and the answers.
  734Note that if $h$ is negated, then the head of the clause will be of
  735the form $ex\_not\_h$, and the ancestor form will be
  736$anc(P,[h(-x-)|N])$. If any of the $b_i$ are negated, then the
  737corresponding predicate will be $ex\_not\_b_i$.
  738
  739\begin{example}\em
  740the rule
  741\begin{quote}
  742$gr(X,Y) \leftarrow f(X,Z), p(Z,Y)$
  743\end{quote}
  744gets translated into
  745\begin{prolog}
  746$ex\_tru\_gr(X,Y,ths(D,E,F,G),anc(H,I),ans(J,K))$\IF
  747$ex\_tru\_f(X,Z,ths(D,M,F,N),anc([gr(X,Y)|H],I),ans(J,O))$\AND
  748$ex\_tru\_p(Z,Y,ths(M,E,N,G),anc([gr(X,Y)|H],I),ans(O,K)).$
  749\end{prolog}
  750To explain $gr$ we explain both $f$ and $p$.
  751The initial assumptions for $f$ should be the initial assumptions for
  752$gr$, and the initial assumptions for $p$ should be the initial assumptions
  753plus those made to explain $f$. The resulting assumptions after proving $p$ are
  754are the assumptions made in explaining $gr$.
  755\end{example}
  756
  757\begin{example} \em the fact
  758\begin{quote}
  759$father(randy,jodi)$
  760\end{quote}
  761gets translated into
  762\begin{quote}
  763$ex\_tru\_father(randy,jodi,ths(T,T,D,D),\_,ans(A,A)).$
  764\end{quote}
  765We can explain $father(randy,jodi)$ independently of the ancestors;
  766we need no extra assumptions, and we create no extra answers.
  767\end{example}
  768
  769Similarly we translate rules of the form
  770\[h(-x-) \leftarrow b_1(-x_1-), b_2(-x_2-), ... ,b_N(-x_n-);\]
  771into
  772\begin{prolog}
  773$prv\_tru\_h(-x-, T, anc(P,N))$\IF
  774$prv\_tru\_b_1(-x_1-,T,anc([h(-x-)|P],N))$\AND
  775$...$\AND
  776$prv\_tru\_b_n(-x_n-,T,anc([h(-x-)|P],N)).$
  777\end{prolog}
  778
  779\begin{example} \em the rule
  780\begin{quote}
  781$gr(X,Y) \leftarrow f(X,Z), p(Z,Y)$
  782\end{quote}
  783gets translated into
  784\begin{prolog}
  785$prv\_tru\_gr(X,Y,D,anc(H,I))$\IF
  786$prv\_tru\_f(X,Z,D,anc([gr(X,Y)|H],I))$\AND
  787$prv\_tru\_p(Z,Y,D,anc([gr(X,Y)|H],I)).$
  788\end{prolog}
  789That is, we can prove $gr$ if we can prove $f$ and $p$.
  790Having $gr(X,Y)$ in the ancestors means that we can prove $gr(X,Y)$
  791by assuming that $\neg gr(X,Y)$ and then proving $gr(X,Y)$.
  792\end{example}
  793
  794\begin{example} \em the fact
  795\begin{quote}
  796$father(randy,jodi)$
  797\end{quote}
  798gets translated into
  799\begin{quote}
  800$prv\_tru\_father(randy,jodi,\_,\_).$
  801\end{quote}
  802Thus we can prove $father(randy,jodi)$ for any explanation and
  803for any ancestors.
  804\end{example}
  805
  806Disjuncts in the source body (;) get mapped into Prolog's disjunction.
  807The answers and assumed hypotheses should be accumulated from
  808whichever branch was taken.
  809This is then executed without mapping out subterms.
  810\begin{example} \em
  811The rule
  812\begin{quote}
  813$p(A) \leftarrow q(A),(r(A),s(A);t(A)),m(A).$
  814\end{quote}
  815gets translated into
  816\begin{tabbing}\hbox{2cm}\=\hbox{1cm}\=\kill
  817$prv\_tru\_p(A,B,anc(C,D)):-$\\
  818\>$prv\_tru\_q(A,B,anc([p(A)|C],D)),$\\
  819\>(\>$prv\_tru\_r(A,B,anc([p(A)|C],D)),$\\
  820\>\>$prv\_tru\_s(A,B,anc([p(A)|C],D))$\\
  821\>;\>$prv\_tru\_t(A,B,anc([p(A)|C],D))),$\\
  822\>$prv\_tru\_m(A,B,anc([p(A)|C],D)).$\\\\
  823
  824$ex\_tru\_p(A,ths(B,C,D,E),anc(F,G),ans(H,I)):-$\\
  825\>$ex\_tru\_q(A,ths(B,J,D,K),anc([p(A)|F],G),ans(H,L)),$\\
  826\>(\>$ex\_tru\_r(A,ths(J,M,K,N),anc([p(A)|F],G),ans(L,O)),$\\
  827\>\>$ex\_tru\_s(A,ths(M,P,N,Q),anc([p(A)|F],G),ans(O,R))$\\
  828\>;\>$ex\_tru\_t(A,ths(J,P,K,Q),anc([p(A)|F],G),ans(L,R))),$\\
  829\>$ex\_tru\_m(A,ths(P,C,Q,E),anc([p(A)|F],G),ans(R,I))$
  830\end{tabbing}
  831Note that $P$ is the resulting explanation from either executing
  832$r$ and $s$ or executing $t$ from the explanation $J$.
  833\end{example}
  834
  835\subsubsection{The Code to Compile Rules}
  836The following relation builds the desired structure for the bodies:
  837\[make\_bodies(B,T,[Ths,Anc,Ans],ProveB,ExB)\]
  838where $B$ is a disjunct/conjunct of literals (the body
  839of the rule), $T$ is a theory for the proving,
  840$Ths$ is a theory structure for explaining,
  841$Anc$ is an ancestor
  842structure (of form $anc(P,N)$), $Ans$ is an answer structure
  843(of form $ans(A0,A1)$). This procedure
  844makes $ProveB$ the body of forms $prv\_tru\_b_i$ (and $prv\_not\_b_i$),
  845and $ExB$ a body of the forms $ex\_tru\_b_i$.
  846
  847\index{make\_bodies}
  848\begin{verbatim} */
  849
  850
  851make_bodies(CoA,(H,B), T, [ths(T1,T3,D1,D3), Anc, ans(A1,A3)],
  852                    (ProveH,ProveB), (ExH,ExB)) :-
  853   !,
  854   make_bodies(CoA,H,T,[ths(T1,T2,D1,D2),Anc,ans(A1,A2)],ProveH,ExH),
  855   make_bodies(CoA,B,T,[ths(T2,T3,D2,D3),Anc,ans(A2,A3)],ProveB,ExB).
  856
  857make_bodies(CoA,(H;B),T,Ths,(ProveH;ProveB),(ExH;ExB)) :-
  858   !,
  859   make_bodies(CoA,H,T,Ths,ProveH,ExH),
  860   make_bodies(CoA,B,T,Ths,ProveB,ExB).
  861
  862
  863make_bodies(callable,n(Builtin),_,[ths(T,T,D,D),_,ans(A,A)], \+ Builtin, \+ Builtin) :- is_thbuiltin(Builtin),!.
  864make_bodies(_CoA,n(A), T, [Ths,Anc,Ans], ProveA, ExA) :-
  865   !,
  866   new_lit(`prv_not_`, A, [T,Anc], ProveA),
  867   new_lit(`ex_not_`, A, [Ths,Anc,Ans], ExA).
  868
  869make_bodies(_CoA,Builtin,_,[ths(T,T,D,D),_,ans(A,A)],Builtin,Builtin) :- is_thbuiltin(Builtin),!.
  870make_bodies(_CoA,A, T, [Ths,Anc,Ans], ProveA, ExA) :- !, 
  871   new_lit(`prv_tru_`, A, [T,Anc], ProveA),
  872   new_lit(`ex_tru_`, A, [Ths,Anc,Ans], ExA).
  873
  874
  875:- dynamic(declared_as_prolog/1).  876is_thbuiltin(V):- var(V),fail.
  877is_thbuiltin(true).
  878is_thbuiltin(unif(_,_)).
  879is_thbuiltin( \+ (_)).
  880is_thbuiltin(call(_)).
  881is_thbuiltin('{}'(_)).
  882is_thbuiltin(G):-declared_as_prolog(G).
  883
  884
  885/* \end{verbatim}
  886
  887The procedure $rule(F,R)$ declares $R$ to be a fact
  888or constraint rule (depending on the value of $F$).
  889Constraints can only be used for proving;
  890facts can be used for explaining as well as proving.
  891$R$ is either a literal or of the form $if(H,B)$ where $H$ is a literal
  892and $B$ is a body.
  893
  894This $rule$ first checks to see whether we want sound unification and
  895then uses $drule(F,R)$ to decare the rule.
  896
  897$prolog\_cl(C)$ is a way of asserting to Prolog the clause $C$.
  898This can either be asserted or written to a file to be consulted
  899or compiled. The simplest form is to just assert $C$.
  900
  901$make\_anc(H)$ is a procedure which ensures that the ancestor search
  902is set up properly for $H$. It is described in section \ref{anc-section},
  903and can be ignored on first reading.
  904
  905\index{rule}
  906\index{drule}
  907\begin{verbatim} */
  908
  909drule(X):- default(X).
  910
  911rule(F,R) :-
  912   flagth((sound_unification,on)),!,
  913   make_sound(R,S),
  914   drule(F,S).
  915rule(F,R) :-
  916   drule(F,R).
  917
  918drule(F,if(H,B)) :-
  919   !,
  920   make_anc(H),
  921   make_bodies(assertable,H,T,[Ths,Anc,Ans],ProveH,ExH),
  922   form_anc(H,Anc,Newanc),
  923   make_bodies(callable,B,T,[Ths,Newanc,Ans],ProveB,ExB),
  924   prolog_cl((ProveH:-ProveB)),
  925   ( F= (fact),
  926     prolog_cl((ExH:-ExB))
  927   ; F= (constraint)).
  928
  929drule(F,H) :-
  930   make_anc(H),
  931   make_bodies(assertable,H,T,[ths(T,T,D,D),_,ans(A,A)],ProveH,ExH),
  932   prolog_cl(ProveH),
  933   ( F= 'fact' -> prolog_cl(ExH) ; F='constraint').
  934
  935
  936/* \end{verbatim}
  937
  938$form\_anc(L,A1,A2)$ means that $A2$ is the ancestor form for
  939subgoal $L$ with previous ancestor form $A1$.
  940
  941\index{form\_anc}
  942\begin{verbatim} */
  943
  944
  945form_anc(n(G), anc(P,N), anc(P,[G|N])) :- !.
  946form_anc(G, anc(P,N), anc([G|P],N)).
  947
  948
  949/* \end{verbatim}
  950\subsection{Forming Contrapositives}
  951For both facts and constraints we convert the user
  952syntax into negation normal
  953form (section \ref{nnf}), form the contrapositives,
  954and declare these as rules.
  955
  956Note that here we choose an arbitrary ordering for the clauses
  957in the bodies of the contrapositive forms of the facts. No
  958attempt has been made to optimise this, although it is noted that some
  959orderings are more efficient than others (see for example \cite{smith86}
  960for a discussion of such issues).
  961
  962The declarations are as follows:
  963\index{declare\_fact}
  964\index{declare\_constraint}
  965\begin{verbatim} */
  966
  967
  968declare_fact(F) :-
  969   nnf(F,even,N),
  970   %wdmsgl(nnf=N),
  971   rulify(fact,N).
  972
  973declare_constraint(C) :-
  974   nnf(C,even,N),
  975   % wdmsgl(cnnf=N),
  976   rulify(constraint,N).
  977
  978
  979/* \end{verbatim}
  980
  981{\em nnf\/$($Wff,Parity,Nnf\/$)$} (section \ref{nnf})
  982means that {\em Nnf\/} is the negation normal form
  983of {\em Wff} if {\em Parity=even} and of $\neg${\em Wff}
  984if {\em Parity=odd}. Note that we {\em rulify} the normal form
  985of the negation of the formula.
  986
  987{\em rulify\/}$(H,N)$ where $H$ is
  988either ``{\em fact\/}'' or ``{\em constraint\/}''
  989and $N$ is the negation of a fact or constraint
  990in negation normal form (see section \ref{nnf}),
  991means that all rules which can be formed from $N$ (by allowing each
  992atom in $N$ being the head of some rule) should be declared as such.
  993\index{rulify}
  994\begin{verbatim} */
  995
  996
  997rulify(H,(A,B)) :- !,
  998   contrapos(H,B,A),
  999   contrapos(H,A,B).
 1000
 1001rulify(H,(A;B)) :- !,
 1002   rulify(H,A),
 1003   rulify(H,B).
 1004
 1005rulify(H,n(A)) :- !,
 1006   rule(H,A).
 1007
 1008rulify(H,A) :-
 1009   rule(H,n(A)).
 1010
 1011
 1012/* \end{verbatim}
 1013
 1014$contrapos(H,D,T)$ where $H$ is either ``{\em fact\/}'' 
 1015or ``{\em constraint\/}'', and $(D,T)$ is (the negation of)
 1016a formula in negation normal form means that all rules
 1017which can be formed from $(D,T)$ with head of the rule coming from $T$
 1018should be formed.
 1019Think of $D$ as the literals for which the rules with them as heads
 1020have been formed, and $T$ as those which remain to be as the head of
 1021some rule.
 1022\index{contrapos}
 1023\begin{verbatim} */
 1024
 1025
 1026contrapos(H,D, (L,R)) :- !,
 1027   contrapos(H,(R,D),L),
 1028   contrapos(H,(L,D),R).
 1029
 1030contrapos(H,D,(L;R)) :- !,
 1031   contrapos(H,D,L),
 1032   contrapos(H,D,R).
 1033
 1034contrapos(H,D,n(A)) :- !,
 1035   rule(H,if(A,D)).
 1036
 1037contrapos(H,D,A) :-
 1038   rule(H,if(n(A),D)).
 1039
 1040
 1041/* \end{verbatim}
 1042\begin{example} \em
 1043if we are to {\em rulify} the negation normal form
 1044\begin{quote}
 1045$n(p(A)),q(A),(r(A),s(A);t(A)),m(A)$
 1046\end{quote}
 1047we generate the following rule forms, which can then be given to {\em rule}
 1048\begin{quote}
 1049$p(A)\leftarrow q(A),(r(A),s(A);t(A)),m(A)$\\
 1050$n(q(A))\leftarrow (r(A),s(A);t(A)),m(A),n(p(A))$\\
 1051$n(r(A))\leftarrow s(A),m(A),q(A),n(p(A))$\\
 1052$n(s(A))\leftarrow r(A),m(A),q(A),n(p(A))$\\
 1053$n(t(A))\leftarrow m(A),q(A),n(p(A))$\\
 1054$n(m(A))\leftarrow (r(A),s(A);t(A)),q(A),n(p(A))$
 1055\end{quote}
 1056\end{example}
 1057\subsection{Sound Unification}
 1058Sound unification works, by checking for repeated variables in the left
 1059hand side of a rule, and then unifies them by hand. This idea was stolen from 
 1060Stickel's implementation.
 1061
 1062\index{make\_sound}
 1063\index{rms}
 1064\begin{verbatim} */
 1065
 1066
 1067make_sound(if(H,B),if(NH,NB)) :- !,
 1068   rms(H,NH,[],_,B,NB).
 1069
 1070make_sound(H,NR) :-
 1071   rms(H,NH,[],_,true,NB),
 1072   (NB=true,NR=H;
 1073    NR=if(NH,NB)),!.
 1074
 1075rms(V,V1,L,L,B,(unif(V,V1),B)) :-
 1076   var(V),
 1077   id_member(V,L),!.
 1078rms(V,V,L,[V|L],B,B) :-
 1079   var(V),!.
 1080rms([H|T],[H1|T1],L1,L3,B1,B3) :- !,
 1081   rms(H,H1,L1,L2,B1,B2),
 1082   rms(T,T1,L2,L3,B2,B3).
 1083rms(A,A,L,L,B,B) :-
 1084   atomic(A),!.
 1085rms(S,S2,L1,L2,B1,B2) :-
 1086   S =.. L,
 1087   rms(L,LR,L1,L2,B1,B2),
 1088   S2 =.. LR.
 1089
 1090
 1091/* \end{verbatim}
 1092
 1093\index{unif}
 1094\index{appears\_in}
 1095\begin{verbatim} */
 1096
 1097unif(X,Y) :- unify_with_occurs_check(X,Y).
 1098/*
 1099unif(X,Y) :-
 1100   var(X), var(Y), X=Y,!.
 1101unif(X,Y) :-
 1102   var(X),!,
 1103   \+ appears_in(X,Y),
 1104   X=Y.
 1105unif(X,Y) :-
 1106   var(Y),!,
 1107   \+ appears_in(Y,X),
 1108   X=Y.
 1109unif(X,Y) :-
 1110   atomic(X),!,X=Y.
 1111unif([H1|T1],[H2|T2]) :- !,
 1112   unif(H1,H2),
 1113   unif(T1,T2).
 1114unif(X,Y) :-
 1115   \+ atomic(Y),
 1116   X=..XS,
 1117   Y=..YS,
 1118   unif(XS,YS).
 1119
 1120appears_in(X,Y) :-
 1121   var(Y),!,X==Y.
 1122appears_in(X,[H|T]) :- !,
 1123   (appears_in(X,H); appears_in(X,T)).
 1124appears_in(X,S) :-
 1125   \+ atomic(S),
 1126   S =.. L,
 1127   appears_in(X,L).
 1128*/
 1129
 1130/* \end{verbatim}
 1131\subsection{Possible Hypotheses}
 1132The other class of things we have to worry about is the class
 1133of possible hypotheses. As described in \cite{poole:lf}
 1134and outlined in section \ref{theorist},
 1135we only need worry about atomic possible hypotheses.
 1136
 1137If $d(-args-)$ is a possible hypothesis (default),
 1138then we want to form the target code as follows:
 1139
 1140\begin{enumerate}
 1141\item We can only prove a hypothesis if we have already assumed it:
 1142\begin{prolog}
 1143$prv\_tru\_d(-args-,Ths,Anc) $\IF
 1144$member(d(-args-),Ths).$
 1145\end{prolog}
 1146\item We can explain a default if we have already assumed it:
 1147\begin{prolog}
 1148$ex\_tru\_d(-args-,ths(T,T,D,D),Anc,ans(A,A)) $\IF
 1149$member(d(-args-),T).$
 1150\end{prolog}
 1151\item We can explain a hypothesis by assuming it,
 1152if it has no free variables, we have not
 1153already assumed it and it is consistent with everything assumed before:
 1154\begin{prolog} \em
 1155$ex\_tru\_d(-args-,ths(T,[d(-args-)|T],D,D),Anc,ans(A,A)) $\IF
 1156variable\_free$(d(-args-))$\AND
 1157$\backslash+(member(d(-args-),T))$\AND
 1158$\backslash+(prv\_not\_d(-args-,[d(-args-)|T],anc([],[]))).$
 1159\end{prolog}
 1160\item 
 1161If a hypothesis has free variables, it can be explained
 1162by adding it to the deferred defaults list (making no assumptions about
 1163its consistency; this will be checked at the end of the explanation phase):
 1164\begin{prolog}
 1165$ex\_tru\_d(-args-,ths(T,T,D,[d(-args-)|D],Anc,ans(A,A)) $\IF
 1166$\backslash+($variable\_free$(d(-args-))).$
 1167\end{prolog}
 1168\end{enumerate}
 1169
 1170The following compiles directly into such code:
 1171\index{declare\_default}
 1172\begin{verbatim} )*/
 1173
 1174
 1175declare_default(D) :-
 1176   make_anc(D),
 1177   new_lit(`prv_tru_`,D,[T,_],Pr_D),
 1178   prolog_cl((Pr_D :- member(D,T))),
 1179   new_lit(`ex_tru_`,D, [ths(T,T,Defer,Defer), _, ans(A,A)], ExD),
 1180   prolog_cl((ExD :- member(D, T))),
 1181   new_lit(`ex_tru_`,D, [ths(T,[D|T],Defer,Defer), _, ans(A,A)], ExDass),
 1182   new_lit(`prv_not_`,D, [[D|T],anc([],[])],Pr_not_D),
 1183   prolog_cl((ExDass :- variable_free(D), \+member(D,T),
 1184                 \+Pr_not_D)),
 1185   new_lit(`ex_tru_`,D, [ths(T,T,Defer,[D|Defer]), _, ans(A,A)], ExDefer),
 1186   prolog_cl((ExDefer :- \+ variable_free(D))).
 1187
 1188
 1189/* \end{verbatim}
 1190
 1191\begin{example}\em
 1192The default
 1193\begin{quote} \em
 1194birdsfly$(A)$
 1195\end{quote}
 1196gets translated into \em
 1197\begin{prolog}
 1198prv\_tru\_birdsfly$(A,B,C):-$\\
 1199\>member$(\hbox{birdsfly}(A),B)$\\
 1200ex\_tru\_birdsfly$(A,ths(B,B,C,C),D,ans(E,E)):-$\\
 1201\>member$(\hbox{birdsfly}(A),B)$\\
 1202ex\_tru\_birdsfly$(A,ths(B,[\hbox{birdsfly}(A)|B],C,C),D,ans(E,E)):-$\\
 1203\>variable\_free$(\hbox{birdsfly}(A)) ,$\\
 1204\>$\backslash+$member$(\hbox{birdsfly}(A),B),$\\
 1205\>$\backslash+$prv\_not\_birdsfly$(A,[\hbox{birdsfly}(A)|B],anc([],[]))$\\
 1206ex\_tru\_birdsfly$(A,ths(B,B,C,[\hbox{birdsfly}(A)|C]),D,ans(E,E)):- $\\
 1207\>$\backslash+$variable\_free$(\hbox{birdsfly}( A))$
 1208\end{prolog}
 1209\end{example}
 1210\subsection{Relations defined in Prolog}
 1211We can define some relations to be executed in Prolog.
 1212This means that we can prove the $prove$ and $ex$ forms by calling 
 1213the appropriate Prolog definition.
 1214\index{declare\_prolog}
 1215\begin{verbatim} */
 1216            
 1217declare_prolog(G) :- declared_as_prolog(G),!.
 1218declare_prolog(G) :-
 1219   prolog_cl(declared_as_prolog(G)),
 1220   new_lit(`ex_tru_`,G, [ths(T,T,D,D), _, ans(A,A)], ExG),
 1221   prolog_cl((ExG :- G)),
 1222   new_lit(`prv_tru_`,G,[_,_],PrG),
 1223   prolog_cl((PrG :- G)),!.
 1224
 1225
 1226/* \end{verbatim}
 1227
 1228\subsection{Explaining Observations}
 1229$expl(G,T0,T1,A)$ means that $T1$ is an explanation of $G$ or $A$ ($A$ being
 1230the alternate answers) from the facts given $T0$ is already assumed.
 1231$G$ is an arbitrary wff.
 1232\index{expl}
 1233\begin{verbatim} */
 1234
 1235
 1236expl(G,T0,T1,Ans) :-
 1237   make_ground(N),
 1238   once(declare_fact('<-'(newans(N,G) , G))),
 1239     ex_tru_newans(N,G,ths(T0,T,[],D),anc([],[]),ans([],Ans)),
 1240   make_ground(D),
 1241   check_consis(D,T,T1).
 1242
 1243
 1244/* \end{verbatim}
 1245
 1246\index{check\_consis}
 1247\begin{verbatim} */
 1248
 1249
 1250check_consis([],T,T).
 1251check_consis([H|D],T1,T) :-
 1252   new_lit(`prv_not_`,H, [T1,anc([],[])], Pr_n_H),
 1253   \+ Pr_n_H,
 1254   check_consis(D,[H|T1],T).
 1255
 1256
 1257/* \end{verbatim}
 1258To obtain disjunctive answers we have to know if the negation of the top
 1259level goal is called. This is done by declaring the fact
 1260$newans(G) \leftarrow G$, and if we ever try to
 1261prove the negation of a top level goal, we add that instance to the
 1262list of alternate answers. In this implementation we also check
 1263that $G$ is not identical to a higher level goal. This removes most cases
 1264where we have a redundant assumption (i.e., when we are not gaining a new
 1265answer, but only adding redundant information).
 1266\index{ex\_not\_newans}
 1267\index{id\_anc}
 1268\begin{verbatim} */
 1269
 1270
 1271:- dynamic ex_not_newans/5. 1272:- dynamic ex_tru_newans/5. 1273:- dynamic prv_not_newans/4. 1274ex_not_newans(N,G,ths(T,T,D,D),anc(Pos,Neg),ans(A,[G|A])) :-
 1275   member(newans(N,_),Pos),
 1276   \+ id_anc(G,anc(Pos,Neg)).
 1277
 1278id_anc(n(G),anc(_,N)) :- !, id_member(G,N).
 1279id_anc(G,anc(P,_)) :- id_member(G,P).
 1280
 1281
 1282/* \end{verbatim}
 1283
 1284\subsection{Ancestor Search} \label{anc-section}
 1285Our linear resolution
 1286theorem prover must recognise that a goal has been proven if
 1287it unifies with an ancestor in the search tree. To do this, it keeps
 1288two lists of ancestors, one containing the positive (non negated)
 1289ancestors and the other the negated ancestors.
 1290When the ancestor search rules for predicate $p$ are defined, we assert
 1291{\em ancestor\_recorded(p)}, so that we do not attempt to redefine the
 1292ancestor search rules.
 1293\index{make\_ex\_tru\_anc}
 1294\index{flagth,ancestor\_search}
 1295\index{flagth,loop\_check}
 1296\begin{verbatim} */
 1297
 1298
 1299:- dynamic ancestor_recorded/1. 1300ancestor_recorded(P):-is_thbuiltin(P). 
 1301
 1302make_anc(_) :-
 1303   flagth((ancestor_search,off)),
 1304   flagth((loop_check,off)),
 1305   flagth((depth_bound,off)),
 1306   !.
 1307make_anc(Name) :-
 1308   ancestor_recorded(Name),
 1309   !.
 1310make_anc(n(Goal)) :-
 1311   !,
 1312   make_anc(Goal).
 1313
 1314make_anc(Goal) :-
 1315   Goal =.. [Pred|Args],
 1316   same_length(Args,Nargs),
 1317   NG =.. [Pred|Nargs],
 1318   make_bodies(assertable,NG,_,[ths(T,T,D,D),anc(P,N),ans(A,A)],ProveG,ExG),
 1319   make_bodies(assertable,n(NG),_,[ths(T,T,D,D),anc(P,N),ans(A,A)],ProvenG,ExnG),
 1320   ( flagth((loop_check,off))
 1321   ;
 1322     prolog_cl((ProveG :- id_member(NG,P),!,fail)),
 1323     prolog_cl((ProvenG :- id_member(NG,N),!,fail)),
 1324     prolog_cl((ExG :- id_member(NG,P),!,fail)),
 1325     prolog_cl((ExnG :- id_member(NG,N),!,fail))
 1326   ),
 1327   ( flagth((ancestor_search,off))
 1328   ;
 1329     prolog_cl((ProveG :- member(NG,N))),
 1330     prolog_cl((ProvenG :- member(NG,P))),
 1331     prolog_cl((ExG :- member(NG,N))),
 1332     prolog_cl((ExnG :- member(NG,P)))
 1333   ),
 1334   ( flagth((depth_bound,off)), !
 1335   ;
 1336     prolog_cl((ProveG :- (flagth((depth_bound,MD))),
 1337            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail)),
 1338     prolog_cl((ProvenG :- (flagth((depth_bound,MD))),
 1339            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail)),
 1340     prolog_cl((ExG :- (flagth((depth_bound,MD))),
 1341            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail)),
 1342      prolog_cl((ExnG :- (flagth((depth_bound,MD))),
 1343            number(MD),length(P,LP),length(N,LN),LP+LN>MD,!,fail))
 1344   ),
 1345   assert(ancestor_recorded(NG)),
 1346   !.
 1347
 1348
 1349/* \end{verbatim}
 1350
 1351\begin{example} \em
 1352If we do a call
 1353\begin{quote}
 1354make\_anc(gr(A,B))
 1355\end{quote}
 1356we create the Prolog clauses
 1357\begin{prolog}
 1358prv\_tru\_gr(A,B,C,anc(D,E))\IF
 1359member(gr(A,B),E).\\
 1360prv\_not\_gr(A,B,C,anc(D,E))\IF
 1361member(gr(A,B),D).\\
 1362ex\_tru\_gr(A,B,ths(C,C,D,D),anc(E,F),ans(G,G))\IF
 1363member(gr(A,B),F).\\
 1364ex\_not\_gr(A,B,ths(C,C,D,D),anc(E,F),ans(G,G))\IF
 1365member(gr(A,B),E).
 1366\end{prolog}
 1367This is only done once for the $gr$ relation.
 1368\end{example}
 1369
 1370\section{Interface}
 1371In this section a minimal interface is given. We try to give
 1372enough so that we can understand the conversion of the wff form
 1373into negation normal form and
 1374the parsing of facts and defaults. There is, of course,
 1375much more in any usable interface than described here.
 1376\subsection{Syntax Declarations}
 1377All of the declarations we use will be defined as operators.
 1378This will allow us to use infix forms of our wffs, for extra readability.
 1379Here we use the standard Edinburgh operator declarations which are
 1380given in the spirit of being enough to make the rest of the description
 1381self contained.
 1382\begin{verbatim} */
 1383
 1384     
 1385:- dynamic((flagth)/1). 1386:- op(1150,fx,'drule'). 1387:- op(1150,fx,'default'). 1388:- op(1150,fx,'fact'). 1389:- op(1150,fx,constraint). 1390:- op(1150,fx,prolog). 1391:- op(1150,fx,explain). 1392:- op(1150,fx,predict). 1393:- op(1150,fx,define). 1394:- op(1150,fx,set). 1395:- op(1150,fx,flagth). 1396:- op(1150,fx,reset). 1397:- op(1150,fy,h). 1398:- op(1150,fx,thconsult). 1399:- op(1150,fx,thtrans). 1400:- op(1150,fx,thcompile). 1401:- op(1130,xfx,:). 1402
 1403:- op(1120,xfx,==). 1404:- op(1120,xfx,<=>). 1405:- op(1120,xfx,equiv). 1406:- op(1110,xfx,<-). 1407:- op(1110,xfx,=>). 1408:- op(1100,xfy,or). 1409:- op(1000,xfy,and). 1410:- op(1000,xfy,&). 1411:- op(950,fy,~). 1412:- op(950,fy,not). 1413
 1414
 1415/* \end{verbatim}
 1416
 1417
 1418\subsection{Converting to Negation Normal Form} \label{nnf}
 1419We want to convert an arbitrarily complex formula into a standard form
 1420called {\em negation normal form\/}. Negation normal form of a formula is
 1421an equivalent formula consisting of conjunctions and disjunctions of
 1422literals (either an atom or of the form $n(A)$ where $A$ is an atom).
 1423The relation defined here puts formulae into negation normal form
 1424without mapping out subterms.
 1425Usually we want to find the negation normal form of the negation of the
 1426formula, as this is the form suitable for use in the body of a rule.
 1427
 1428The predicate used is of the form
 1429\[nnf(Fla,Parity,Body)\]
 1430where
 1431\begin{description}
 1432\item[$Fla$] is a formula with input syntax
 1433\item[$Parity$] is either $odd$ or $even$ and denotes whether $Fla$ is
 1434in the context of an odd or even number of negations.
 1435\item[$Body$] is a tuple which represents the negation normal form
 1436of the negation of $Fla$
 1437if parity is even and the negation normal form of $Fla$ if parity is odd. 
 1438\end{description}
 1439\index{nnf}
 1440\begin{verbatim} */
 1441
 1442
 1443nnf((X equiv Y), P,B) :- !,
 1444   nnf(((Y or not X) and (X or not Y)),P,B).
 1445nnf((X == Y), P,B) :- !,
 1446   nnf(((Y or not X) and (X or not Y)),P,B).
 1447nnf('<=>'(X , Y), P,B) :- !,
 1448   nnf(((Y or not X) and (X or not Y)),P,B).
 1449nnf(all(_, Y), P,B) :- !,nnf(Y, P,B).
 1450nnf(exists(E, Y), P,exists(E, B)) :- !,nnf(Y, P,B).
 1451nnf(if(X , Y), P,B) :- !,
 1452   nnf((Y or not X),P,B).
 1453nnf((X => Y), P,B) :- !,
 1454   nnf((Y or not X),P,B).
 1455nnf((Y <- X), P,B) :- !,
 1456   nnf((Y or not X),P,B).
 1457nnf((X & Y), P,B) :- !,
 1458   nnf((X and Y),P,B).
 1459nnf((X , Y), P,B) :- !,
 1460   nnf((X and Y),P,B).
 1461nnf((X ; Y), P,B) :- !,
 1462   nnf((X or Y),P,B).
 1463nnf((X and Y),P,B) :- !,
 1464   opposite_parity(P,OP),
 1465   nnf((not X or not Y),OP,B).
 1466nnf((X or Y),even,(XB,YB)) :- !,
 1467   nnf(X,even,XB),
 1468   nnf(Y,even,YB).
 1469nnf((X or Y),odd,(XB;YB)) :- !,
 1470   nnf(X,odd,XB),
 1471   nnf(Y,odd,YB).
 1472nnf((~ X),P,B) :- !,
 1473   nnf((not X),P,B).
 1474nnf((not X),P,B) :- !,
 1475   opposite_parity(P,OP),
 1476   nnf(X,OP,B).
 1477
 1478nnf(F,odd,FF):- xlit(F,FF).
 1479
 1480nnf(n(F),even,FF) :- !,xlit(F,FF).
 1481nnf(F,even,n(FF)):- xlit(F,FF).
 1482
 1483xlit(F,F):- \+ compound(F).
 1484xlit({X},{X}).
 1485xlit(=(A,B),sameObjects(A,B)).
 1486xlit(neq(A,B),{dif(A,B)}).
 1487xlit([F|Args],OUT):- maplist(xlit,[F|Args],OUT).
 1488xlit(P,PP):- P=..[F|Args],maplist(xlit,Args,FArgs),PP=..[F|FArgs].
 1489
 1490
 1491/* \end{verbatim}
 1492\index{opposite\_parity}
 1493\begin{verbatim} */
 1494
 1495
 1496opposite_parity(even,odd).
 1497opposite_parity(odd,even).
 1498
 1499
 1500/* \end{verbatim}
 1501
 1502\begin{example} \em
 1503the wff
 1504\begin{quote} \em
 1505(a or not b) and c $\Rightarrow$ d and (not e or f)
 1506\end{quote}
 1507with parity {\em odd} gets translated into
 1508\begin{quote}
 1509$d,(e;f);n(a),b;n(c) $
 1510\end{quote}
 1511the same wff with parity {\em even} (i.e., the negation of the wff)
 1512has negation normal form:
 1513\begin{quote}
 1514$(n(d);e,n(f)),(a;n(b)),c$
 1515\end{quote}
 1516\end{example}
 1517
 1518\subsection{Theorist Declarations}
 1519The following define the Theorist declarations.
 1520Essentially these operators just call the appropriate compiler
 1521instruction. These commands cannot be undone by doing a retry to them;
 1522the compiler assertions will be undone on backtracking.
 1523\index{fact}
 1524\begin{verbatim} */
 1525
 1526
 1527fact(F) :- declare_fact(F),!.
 1528
 1529
 1530/* \end{verbatim}
 1531
 1532The $default$ declaration makes the appropriate equivalences between the
 1533named defaults and the unnamed defaults.
 1534\index{default}
 1535\begin{verbatim} */
 1536
 1537
 1538default((N : H)):-
 1539   !,
 1540   declare_default(N),
 1541   declare_fact((H <-N)),
 1542   !.
 1543default( N ):-
 1544   declare_default(N),
 1545   !.
 1546
 1547
 1548/* \end{verbatim}
 1549\index{default}
 1550\begin{verbatim} */
 1551
 1552
 1553constraint((C)) :-
 1554   declare_constraint(C),
 1555   !.
 1556
 1557                       
 1558/* \end{verbatim}
 1559The $prolog$ command says that the atom $G$ should be proven in the
 1560Prolog system. The argument of the $define$ statement is a Prolog
 1561definition which should be asserted (N.B. that it should be in
 1562parentheses if it contains a ``{\tt :-}''.
 1563\index{prolog}
 1564\begin{verbatim} 
 1565)
 1566*/
 1567
 1568                                   
 1569prolog(( G )) :-
 1570   declare_prolog(G).
 1571
 1572
 1573/* \end{verbatim}
 1574\index{define}
 1575\begin{verbatim} */
 1576
 1577
 1578define( G ):-
 1579   prolog_cl(G).
 1580
 1581
 1582/* \end{verbatim}
 1583
 1584The $explain$ command keeps writing out all of the explanations found.
 1585This is done by finding one, writing the answer, and then retrying so that
 1586the next answer is found. This is done so that the computation is left in
 1587an appropriate state at the end of the computation.
 1588\index{explain}
 1589\begin{verbatim} */
 1590
 1591explain G :- ignore((explain_goal(G)*->fail;(format('~nUntrue: ~p.~n',[G]),forall(explain_goal(~G),true)))).
 1592
 1593explain_goal(G) :-
 1594   (flagth((timing,on))),!,
 1595    statistics(runtime,_),
 1596    expl(G,[],D,A),
 1597    statistics(runtime,[_,Time]),
 1598    writeans(G,D,A),
 1599    format('took ~3d sec.~n~n',[Time])
 1600    
 1601  ;
 1602    expl(G,[],D,A),
 1603    writeans(G,D,A).
 1604/* \end{verbatim}
 1605\index{writeans}
 1606\index{writedisj}
 1607\begin{verbatim} */
 1608
 1609
 1610writeans(G,D,A) :-
 1611   format('~nAnswer is ~p', [G]),
 1612   writedisj(A),
 1613   format('~nTheory is ~p~n', [D]),
 1614   !.
 1615
 1616writedisj([]).
 1617writedisj([H|T]) :-
 1618   writedisj(T),
 1619   format(' or ~p',[H]).
 1620
 1621
 1622/* \end{verbatim}
 1623
 1624\subsection{Prediction}
 1625In \cite{poole:lf} we present a sceptical view of prediction
 1626argue that one should predict what is in every extension.
 1627The following theorem proved in \cite{poole:lf} gives us a hint
 1628as to how it should be implemented.
 1629\begin{theorem} \label{everythm}
 1630$g$ is not in every extension iff there exists a scenario $S$ such
 1631that $g$ is not explainable from $S$.
 1632\end{theorem}
 1633
 1634The intuition is that
 1635if $g$ is not in every extension then there is no reason to rule out
 1636$S$ (based on the information given) and so we should not predict $g$.
 1637                      
 1638We can use theorem \ref{everythm} to consider another way to view membership
 1639in every extension. Consider two antagonistic agents $Y$ and $N$ trying to
 1640determine whether $g$ should be predicted or not. $Y$ comes
 1641up with explanations of $g$, and $N$ tries to find where these explanations
 1642fall down (i.e., tries to find a scenario $S$ which is inconsistent with
 1643all of $Y$''s explanations). $Y$ then tries to find an explanation of $g$
 1644given $S$.
 1645If $N$ cannot find a defeater for $Y$'s explanations then
 1646$g$ is in every extension, and if $Y$ cannot find an explanation from
 1647some $S$ constructed by $N$ then $g$ is not in every extension.
 1648                                                                       
 1649The following code implements this, but (as we cannot implement
 1650coroutines as needed above in Prolog), it may generate more
 1651explanations of the goal than is needed. What we really want is for the
 1652first ``bagof'' to generate the explanations in a demand-driven fashion,
 1653and then just print the explanations needed.
 1654
 1655\index{predict}
 1656\begin{verbatim} */
 1657                     
 1658
 1659predict(( G )):-
 1660  bagof(E,expl(G,[],E,[]),Es),
 1661  predct(G,Es). 
 1662 
 1663predct(G,Es) :- 
 1664  simplify_expls(Es,SEs),
 1665    ( find_counter(SEs,[],S),
 1666      !,
 1667      format('No, ~q is not explainable from ~q.~n',[G,S])
 1668    ; format('Yes, ~q is in all extensions.~nExplanations are:~n',[G]),
 1669      list_scens(1,SEs)).
 1670
 1671
 1672/* \end{verbatim}
 1673
 1674\index{find\_counter}
 1675\begin{verbatim} */
 1676
 1677
 1678find_counter([],S,S).
 1679find_counter([E|R],S0,S2) :-
 1680   member(D,E),
 1681   expl2not(D,S0,S1),
 1682   find_counter(R,S1,S2).
 1683
 1684
 1685/* \end{verbatim}
 1686
 1687\index{list\_scens}
 1688\begin{verbatim} */
 1689
 1690
 1691list_scens(_,[]).
 1692list_scens(N,[H|T]) :-
 1693   format('~q: ~q.~n',[N,H]),
 1694   N1 is N+1,
 1695   list_scens(N1,T).
 1696
 1697
 1698/* \end{verbatim}
 1699
 1700$expl2not(G,T0,T1)$ is true if ground $\neg G$ is explainable starting from
 1701scenario $T0$, with resulting explanation $T1$. No disjunctive answers are
 1702formed.
 1703\index{expl2}
 1704\begin{verbatim} */
 1705
 1706
 1707expl2not(G,T0,T1) :-
 1708   new_lit(`ex_not_`,G,[ths(T0,T,[],D),anc([],[]),ans([],[])],ExG),
 1709   ExG,
 1710   make_ground(D),
 1711   check_consis(D,T,T1).
 1712
 1713
 1714/* \end{verbatim}
 1715
 1716\subsection{Simplifying Explanations}
 1717\index{simplify\_obs}
 1718\begin{verbatim} */
 1719                                   
 1720
 1721simplify_expls([S],[S]).
 1722
 1723simplify_expls([H|T], S) :-
 1724   simplify_expls(T, TS),
 1725   mergeinto(H,TS,S).
 1726
 1727
 1728/* \end{verbatim}
 1729\index{mergeinto}
 1730\begin{verbatim} */
 1731
 1732
 1733mergeinto(L,[],[L]).
 1734
 1735mergeinto(L,[A|R],[A|R]) :-
 1736   instance_of(A,L),
 1737   !.
 1738
 1739mergeinto(L,[A|R],N) :-
 1740   instance_of(L,A),
 1741   !,
 1742   mergeinto(L,R,N).
 1743
 1744mergeinto(L,[A|R],[A|N]) :-
 1745   mergeinto(L,R,N).
 1746
 1747                         
 1748/* \end{verbatim}
 1749
 1750\index{instance\_of}
 1751\begin{verbatim} */
 1752
 1753
 1754instance_of(D,S) :-
 1755   remove_all(D,S,_).
 1756                           
 1757
 1758/* \end{verbatim}
 1759
 1760\subsection{File Handling}
 1761To consult a Theorist file, you should do a,
 1762\begin{verse}
 1763{\bf thconsult} \em filename.
 1764\end{verse}
 1765The following is the definition of {\em thconsult}. Basicly we just
 1766keep reading the file and executing the commands in it until we stop.
 1767\index{thconsult}
 1768\begin{verbatim} */
 1769
 1770thconsult(( File0 )):-
 1771   fix_absolute_file_name(File0,File),
 1772   current_input(OldFile),
 1773   open(File,read,Input),
 1774   set_input(Input),
 1775   th_read(T),
 1776   read_all(T),!,
 1777   set_input(OldFile).
 1778
 1779
 1780/* \end{verbatim}
 1781\index{read\_all}
 1782\begin{verbatim} */
 1783
 1784
 1785:- meta_predicate(read_all(*)). 1786read_all(end_of_file) :- !.
 1787
 1788read_all(T) :-
 1789   ((flagth(( asserting,on))),!; format('~n% ~p.~n',[T])),
 1790   (thmust(T) *-> true ; format('% Warning: ~p failed~n',[T])),
 1791   th_read(T2),
 1792   read_all(T2).
 1793
 1794th_read(T):- read_term(T,[module(snark_theorist),variable_names(Vs)/*,double_quotes(codes)*/]),b_setval('$variable_names',Vs).
 1795                 
 1796thmust(G):- call(G),!.
 1797thmust(G):- rtrace(G),!.
 1798
 1799/* \end{verbatim}
 1800
 1801{\em thtrans} is like the previous version, but the generated code is written
 1802to a file. This code is neither loaded or compiled.
 1803\index{thtrans}
 1804\begin{verbatim} */
 1805
 1806fix_absolute_file_name(I,O):- is_list(I),!,string_to_atom(I,A),absolute_file_name(A,O).
 1807fix_absolute_file_name(I,O):- absolute_file_name(I,O),!.
 1808fix_absolute_file_name(I,O):- I=O.
 1809
 1810
 1811thtrans(( File0 )):-
 1812   fix_absolute_file_name(File0,File),
 1813   string_codes(File, Fname),
 1814   append(Fname,`.pl`,Plfname),
 1815   name(Plfile, Plfname),
 1816   current_output(Oldoutput),
 1817   open(Plfile,write,Output),
 1818   set_output(Output),
 1819   thtrans2out(File),
 1820   close(Output),
 1821   set_output(Oldoutput),!.
 1822   
 1823
 1824thtrans2out(File0):-
 1825   fix_absolute_file_name(File0,File),
 1826   current_input(Oldinput),
 1827   open(File,read,Input),
 1828   set_input(Input),
 1829   format(':- dynamic contrapos_recorded/1.~n',[]),
 1830   format(':- style_check(- singleton).~n',[]),
 1831   format(':- style_check(- discontiguous).~n',[]),
 1832   (setth((asserting,off))),
 1833   th_read(T),
 1834   read_all(T),
 1835   set_input(Oldinput),
 1836   resetth(( asserting)),!.
 1837
 1838/* \end{verbatim}
 1839To compile a Theorist file, you should do a,
 1840\begin{verse}
 1841{\bf thconsult} \em filename.
 1842\end{verse}
 1843
 1844This translates the code to Prolog and then compiles the prolog code.
 1845
 1846{\em thcompile} translates the file to Prolog
 1847which is then compiled using the Prolog compiler.
 1848\index{thcompile}
 1849\begin{verbatim} */
 1850
 1851
 1852thcompile(( File )):-
 1853   (thtrans(( File))),
 1854%   no_style_check(all),
 1855   compile(File).  
 1856
 1857
 1858/* \end{verbatim}
 1859
 1860
 1861\subsection{Flag Setting} \label{flags}
 1862There are a number of Theorist options which can be set by flagth declarations.
 1863Flags, by default, are {\tt on}.
 1864To set the flagth $f$ to value $v$ you can issue the command
 1865\begin{verse}
 1866\bf set $f,v.$
 1867\end{verse}
 1868To find out the value of the flagth $f$ issue the command
 1869\begin{verse}
 1870\bf flagth $f,V.$
 1871\end{verse}
 1872You can reset the value of flagth $f$ to its old value by
 1873\begin{verse}
 1874\bf reset $f.$
 1875\end{verse}
 1876The list of all flags is given by the command
 1877\begin{verse}
 1878\bf flags.
 1879\end{verse}
 1880
 1881The following is the definition of these
 1882\index{set}
 1883\begin{verbatim} */
 1884
 1885
 1886setth((F,V)):-
 1887   prolog_decl((flagth((F,V1)):- !,V=V1)),!.
 1888
 1889
 1890/* \end{verbatim}
 1891\index{flagth}
 1892\begin{verbatim} */
 1893
 1894
 1895flagth((_,on)).
 1896
 1897
 1898/* \end{verbatim}
 1899\index{reset}
 1900\begin{verbatim} */
 1901
 1902
 1903resetth(F) :-
 1904   retract((flagth((F,_)) :- !,_=_)).
 1905
 1906
 1907/* \end{verbatim}
 1908\index{flags}
 1909\begin{verbatim} */
 1910
 1911
 1912flags :- list_flags([asserting,ancestor_search,loop_check,
 1913                     depth_bound,sound_unification,timing]).
 1914list_flags([]).
 1915list_flags([H|T]) :-
 1916   (flagth((H,V))),
 1917   format('flagth((~w,~w)).~n',[H,V]),
 1918   list_flags(T).
 1919                          
 1920
 1921/* \end{verbatim}
 1922\subsection{Compiler Directives}
 1923There are some compiler directives which need to be added to Theorist
 1924code so that the Prolog to assembly language compiler can work
 1925(these are translated into the appropriate Quintus compiler directives).
 1926
 1927So that the Quintus compiler can correctly compile the code,
 1928we should declare that all calls for which we can assert the goal
 1929or the negative are dynamic, this is done by the command
 1930\begin{verse}
 1931\bf dyn $n.$
 1932\end{verse}
 1933This need only be given in files,
 1934and should be given before the atomic symbol $n$ is ever used.
 1935
 1936The following gives the appropriate translation.
 1937Essentially we then must say that the appropriate Prolog code is dynamic.
 1938\index{explainable}
 1939\begin{verbatim} */
 1940
 1941
 1942:- op(1150,fx,(dyn)). 1943dyn(n(G)) :-
 1944   !,
 1945   (dyn(G)).
 1946dyn(G):-
 1947   G =.. [R|Args],
 1948   add_prefix(`ex_not_`,R,ExNR),
 1949   add_prefix(`ex_tru_`,R,ExR),
 1950   length(Args,NA),
 1951   ExL is NA + 3,
 1952   decl_dyn(ExNR/ExL),
 1953   decl_dyn(ExR/ExL),
 1954   add_prefix(`prv_not_`,R,PrNR),
 1955   add_prefix(`prv_tru_`,R,PrR),
 1956   PrL is NA + 2,
 1957   decl_dyn(PrNR/PrL),
 1958   decl_dyn(PrR/PrL).
 1959
 1960decl_dyn(F/A) :- (flagth((asserting, on))),!,dynamic(F/A).
 1961decl_dyn(FA):- format(':- dynamic ~q.~n',[FA]).
 1962
 1963
 1964:- op(1150,fx,explainable). 1965explainable G :- dyn G. 
 1966
 1967                       
 1968/* \end{verbatim}
 1969
 1970\subsection{Using the Compiled Rules}
 1971The use of conditional asserting (prolog\_cl) is twofold.
 1972The first is to write the condition to a file if that is desired.
 1973The second is to be a backtrackable assert otherwise.
 1974\index{prolog\_cl}
 1975\index{flagth,asserting}
 1976\begin{verbatim} */
 1977
 1978% if_dbg(_G):-true,!.
 1979if_dbg(G):-call(G).
 1980
 1981print_clause(C) :- portray_clause(C).
 1982/*
 1983print_clause(C) :- 
 1984   \+ \+ (    
 1985     tnumbervars(C,0,_),
 1986     writeq(C),
 1987     write('.'),
 1988     nl).
 1989*/
 1990%prolog_cl(({C}:-B)):- !, prolog_cl((C:-B)).
 1991%prolog_cl({C}):- !, prolog_cl(C).
 1992
 1993prolog_cl((C:-B)):- \+ \+ ( C = B),!.
 1994prolog_cl(C) :-    
 1995   flagth((asserting,off)),!,
 1996   print_clause(C),!.
 1997
 1998prolog_cl(C) :-
 1999   (clause_asserted(C)->! ; (assertz(C),call(if_dbg(print_clause((C)))))),!.
 2000prolog_cl(C) :-
 2001   if_dbg(print_clause(retract(C))),
 2002   break,retract(C),
 2003   fail.
 2004
 2005
 2006/* \end{verbatim}
 2007$prolog\_decl$ is like the above predicate, but is both
 2008written to the file and asserted.
 2009\index{prolog\_decl}
 2010\begin{verbatim} */
 2011                     
 2012
 2013prolog_decl(C) :-
 2014   flagth((asserting,off)),
 2015   print_clause(C),
 2016   fail.
 2017prolog_decl(C) :-
 2018   asserta(C).
 2019prolog_decl(C) :-
 2020   retract(C),
 2021   fail.          
 2022              
 2023
 2024/* \end{verbatim}
 2025\subsection{Saving Theorist}
 2026The command ``save'' automagically saves the state of the Theorist code
 2027as the command `theorist`. This is normally done straight after compiling this
 2028file.
 2029\index{save}
 2030\begin{verbatim} */
 2031
 2032
 2033save :-
 2034   call(call,quintus:save_program(th,
 2035   format('~nWelcome to THEORIST 1.1.1  (4 December 89 version)
 2036For help type ``h.''.
 2037Any Problems see David Poole (poole@cs.ubc.ca)~n',
 2038  []))).
 2039
 2040
 2041/* \end{verbatim}
 2042\section{Utility Functions}
 2043\subsection{List Predicates}
 2044$append(X,Y,Z)$ is the normal append function
 2045\index{append}
 2046\begin{verbatim} 
 2047append([],L,L).
 2048
 2049append([H|X],Y,[H|Z]) :-
 2050   append(X,Y,Z).
 2051\end{verbatim}
 2052
 2053\index{member}
 2054\begin{verbatim} */
 2055
 2056/*
 2057member(A,[A|_]).
 2058member(A,[_|R]) :-
 2059   member(A,R).
 2060*/
 2061
 2062/* \end{verbatim}
 2063
 2064$id\_member(X,L)$ is true if $X$ is identical to some member of list $L$.
 2065\index{id\_member}
 2066\begin{verbatim} */
 2067
 2068
 2069id_member(A,[B|_]) :-
 2070   A==B.
 2071id_member(A,[_|R]) :-
 2072   id_member(A,R).
 2073
 2074
 2075/* \end{verbatim}
 2076
 2077\index{same\_length}
 2078\begin{verbatim} */
 2079
 2080
 2081same_length([],[]).
 2082same_length([_|L1],[_|L2]) :-
 2083   same_length(L1,L2).
 2084
 2085
 2086/* \end{verbatim}
 2087
 2088\index{remove}
 2089\begin{verbatim} */
 2090
 2091
 2092remove(A,[A|B],B).
 2093remove(A,[H|T],[H|R]) :-
 2094   remove(A,T,R).
 2095
 2096
 2097/* \end{verbatim}
 2098
 2099\index{remove\_all}
 2100\begin{verbatim} */
 2101
 2102
 2103remove_all([],L,L).
 2104remove_all([H|T],L,L2) :-
 2105   remove(H,L,L1),
 2106   remove_all(T,L1,L2).
 2107
 2108
 2109/* \end{verbatim}
 2110
 2111\subsection{Looking at Terms}
 2112\index{variable\_free}
 2113\begin{verbatim} */
 2114
 2115variable_free(X) :- !, \+ ground(X).
 2116
 2117variable_free(X) :-
 2118   atomic(X),
 2119   !.
 2120variable_free(X) :-
 2121   var(X),
 2122   !,
 2123   fail.
 2124variable_free([H|T]) :-
 2125   !,
 2126   variable_free(H),
 2127   variable_free(T).
 2128variable_free(X) :-
 2129   X =.. Y,
 2130   variable_free(Y).
 2131
 2132
 2133/* \end{verbatim}
 2134
 2135\index{make\_ground}
 2136\begin{verbatim} */
 2137
 2138
 2139make_ground(X) :-
 2140   retract(groundseed(N)),
 2141   tnumbervars(X,N,NN),
 2142   asserta(groundseed(NN)).
 2143
 2144:- dynamic groundseed/1. 2145groundseed(26).
 2146
 2147
 2148
 2149/* \end{verbatim}
 2150
 2151\index{reverse}
 2152\begin{verbatim} */
 2153
 2154
 2155reverse([],T,T).
 2156reverse([H|T],A,B) :-
 2157   reverse(T,A,[H|B]).
 2158
 2159
 2160/* \end{verbatim}
 2161                                                     
 2162\subsection{Help Commands}
 2163\index{h}
 2164\begin{verbatim} */
 2165
 2166
 2167(h) :- format('This is Theorist 1.1 (all complaints to David Poole)
 2168For more details issue the command:
 2169   h H.
 2170where H is one of:~n',
 2171[]),
 2172   unix(system('ls /faculty/poole/theorist/help')).
 2173
 2174(h(( H))) :- !,
 2175   add_prefix(`more /faculty/poole/theorist/help/`,H,Cmd),
 2176   unix(system(Cmd)).
 2177                              
 2178
 2179
 2180/* \end{verbatim}
 2181
 2182\subsection{Runtime Considerations}
 2183What is given here is the core part of our current implementation of
 2184Theorist.
 2185This code has been used with Waterloo Unix Prolog, Quintus Prolog,
 2186C-prolog and Mac-Prolog.
 2187For those Prologs with compilers we can actually compile the resulting
 2188code from this translater as we could any other Prolog code;
 2189this make it very fast indeed.
 2190
 2191The resulting code when the Theorist code is of the form of definite clauses 
 2192(the only case where a comparison makes sense,
 2193as it is what the two systems have in common), runs at about a quarter
 2194the speed
 2195of the corresponding interpreted or compiled code of the underlying
 2196Prolog system. About half of this extra cost is
 2197for the extra arguments to unify,
 2198and the other factor is for one membership
 2199of an empty list for each procedure call.
 2200For each procedure call we do one extra Prolog call which immediately fails.
 2201For the definite clause case, the contrapositive of the clauses are never used.
 2202\section{Conclusion}
 2203This paper has described in detail how we can translate Theorist code into
 2204prolog so that we can use the advances in Prolog implementation Technology.
 2205
 2206As far as this compiler is concerned there are a few issues which
 2207arise:
 2208\begin{itemize}                      
 2209\item Is there a more efficient way to determine that a goal can succeed because
 2210it unifies with an ancestor \cite{poole:grace,loveland87}?
 2211\item Can we incorporate a cycle check that has a low overhead?
 2212A simple, but expensive, version is implemented in some versions of
 2213our compiler which checks for identical ancestors.
 2214\item Are there optimal ordering which we can put the compiled
 2215clauses in so that we get answer most quickly \cite{smith86}?
 2216At the moment the compiler just puts the elements of the bodies
 2217in an arbitrary ordering. The optimal ordering depends, of course,
 2218on the underlying control structure.
 2219\item Are there better ways to do the consistency checking when there are
 2220variables in the hypotheses?
 2221\end{itemize}
 2222
 2223
 2224We are currently working on many applications of default and abductive
 2225reasoning.
 2226Hopefully with compilers based on the ideas presented in this paper
 2227we will be able to take full advantage of
 2228advances in Prolog implementation technology while still allowing
 2229flexibility in specification of the problems to be solved.
 2230\section*{Acknowledgements}
 2231This work could not have been done without the ideas,
 2232criticism and feedback from Randy Goebel, Eric Neufeld,
 2233Paul Van Arragon, Scott Goodwin and Denis Gagn\'e.
 2234Thanks to Brenda Parsons and Amar Shan for valuable comments on
 2235a previous version of this paper.
 2236This research was supported under NSERC grant A6260.
 2237\begin{thebibliography}{McDer80}
 2238\bibitem[Brewka86]{brewka86}
 2239G.\ Brewka,
 2240``Tweety -- Still Flying: Some Remarks on Abnormal Birds, Applicable Rules
 2241and a Default Prover'',
 2242{\em Proc.\ AAAI-86}, pp.\ 8-12.
 2243
 2244\bibitem[Chang73]{chang}
 2245C-L.\ Chang and R.\ C-T.\ Lee,
 2246{\em Symbolic Logic and Mechanical Theorem Proving},
 2247Academic Press, 1973.
 2248
 2249\bibitem[Cox82]{cox82}
 2250P.\ T.\ Cox, {\em Dependency-directed backtracking for Prolog Programs}.
 2251
 2252\bibitem[Cox87]{cox87}
 2253P.\ T.\ Cox and T.\ Pietrzykowski, {\em General Diagnosis by Abductive
 2254Inference}, Technical report CS8701, School of Computer Science,
 2255Technical University of Nova Scotia, April 1987.
 2256
 2257\bibitem[Dincbas87]{dincbas}
 2258M.~Dincbas, H.~Simonis and P.~Van Hentenryck,
 2259{\em Solving Large Combinatorial Problems in Logic Programming\/},
 2260ECRC Technical Report, TR-LP-21, June 1987.
 2261
 2262\bibitem[Doyle79]{doyle79}
 2263J.\ Doyle,
 2264``A Truth Maintenance System'',
 2265{\em Artificial Intelligence},
 2266Vol.\ 12, pp 231-273.
 2267
 2268\bibitem[de Kleer86]{dekleer86}
 2269J.\ de Kleer,
 2270``An Assumption-based TMS'',
 2271{\em Artificial Intelligence, Vol.\ 28, No.\ 2}, pp.\ 127-162.
 2272
 2273\bibitem[Edmonson87]{edmonson}
 2274R.~Edmonson, ????
 2275
 2276\bibitem[Enderton72]{enderton}
 2277H.\ B.\ Enderton, {\em A Mathematical Introduction to Logic},
 2278Academic Press, Orlando.
 2279
 2280\bibitem[Genesereth87]{genesereth87}
 2281M.\ Genesereth and N.\ Nilsson,
 2282{\em Logical Foundations of Artificial Intelligence},
 2283Morgan-Kaufmann, Los Altos, California.
 2284
 2285\bibitem[Ginsberg87]{ginsberg87}
 2286M.~L.~Ginsberg, {\em Computing Circumscription\/},
 2287Stanford Logic Group Report Logic-87-8, June 1987.
 2288
 2289\bibitem[Goebel87]{goebel87}
 2290R.\ G.\ Goebel and S.\ D.\ Goodwin,
 2291``Applying theory formation to the planning problem''
 2292in F.\ M.\ Brown (Ed.),
 2293{\em Proceedings of the 1987 Workshop on The Frame Problem in Artificial
 2294Intelligence}, Morgan Kaufmann, pp.\ 207-232.
 2295
 2296\bibitem[Kowalski79]{kowalski}
 2297R.~Kowalski, ``Algorithm = Logic + Control'',
 2298{\em Comm.~A.C.M.} Vol 22, No 7, pp.~424-436.
 2299
 2300\bibitem[Lifschitz85]{lifschitz85}
 2301V.~Lifschitz, ``Computing Circumscription'',
 2302{\em Proc.~IJCAI85}, pp.~121-127.
 2303
 2304\bibitem[Lloyd87]{lloyd}
 2305J.~Lloyd, {\em Foundations of Logic Programming},
 2306Springer-Verlag, 2nd Edition.
 2307
 2308\bibitem[Loveland78]{loveland78}
 2309D.~W.~Loveland, {\em Automated Theorem Proving: a logical basis},
 2310North-Holland, Amsterdam.
 2311
 2312\bibitem[Loveland87]{loveland87}
 2313D.~W.~Loveland, ``Near-Horn Logic Programming'',
 2314{\em Proc. 6th International Logic Programming Conference}.
 2315
 2316\bibitem[McCarthy86]{mccarthy86}
 2317J.\ McCarthy, ``Applications of Circumscription to Formalising
 2318Common Sense Knowledge'', {\em Artificial Intelligence}, Vol.\ 28, No.\ 1,
 2319pp.\ 89-116.
 2320
 2321\bibitem[Moto-Oka84]{pie}
 2322T.~Moto-Oka, H.~Tanaka, H.~Aida, k.~Hirata and T.~Maruyama,
 2323``The Architecture of a Parallel Inference Engine --- PIE'',
 2324{\em Proc.\ Int.\ Conf.\ on Fifth Generation Computing Systems},
 2325pp.~479-488.
 2326
 2327\bibitem[Naish86]{naish86}
 2328L.~Naish, ``Negation and Quantifiers in NU-PROLOG'',
 2329{\em Proc.~3rd Int.\ Conf.\ on Logic Programming},
 2330Springer-Verlag, pp.~624-634.
 2331
 2332\bibitem[Neufeld87]{neufeld87}
 2333E.\ M.\ Neufeld and D.\ Poole,
 2334``Towards solving the multiple extension problem:
 2335combining defaults and probabilities'',
 2336{\em Proc.\ Third AAAI Workshop on Reasoning with Uncertainty},
 2337Seattle, pp.\ 305-312.
 2338
 2339\bibitem[Poole84]{poole:clausal}
 2340D.\ L.\ Poole,
 2341``Making Clausal theorem provers Non-clausal'',
 2342{\em Proc.\ CSCSI-84}. pp.~124-125.
 2343
 2344\bibitem[Poole86]{poole:grace}
 2345D.\ L.\ Poole,
 2346``Gracefully adding Negation to Prolog'',
 2347{\em Proc.~Fifth International Logic Programming Conference},
 2348London, pp.~635-641.
 2349
 2350\bibitem[Poole86]{poole:dd}
 2351D.\ L.\ Poole,
 2352``Default Reasoning and Diagnosis as Theory Formation'',
 2353Technical Report, CS-86-08, Department of Computer Science,
 2354University of Waterloo, March 1986.
 2355
 2356\bibitem[Poole87a]{poole:vars}
 2357D.\ L.\ Poole,
 2358``Variables in Hypotheses'', 
 2359{\em Proc.~IJCAI-87}, pp.\ 905-908.
 2360
 2361\bibitem[Poole87b]{poole:dc}
 2362D.\ L.\ Poole,
 2363{\em Defaults and Conjectures: Hypothetical Reasoning for Explanation and
 2364Prediction}, Research Report CS-87-54, Department of
 2365Computer Science, University of Waterloo, October 1987, 49 pages.
 2366
 2367\bibitem[Poole88]{poole:lf}
 2368D.\ L.\ Poole,
 2369{\it A Logical Framework for Default Reasoning},
 2370to appear {\em Artificial Intelligence}, Spring 1987.
 2371
 2372\bibitem[PGA87]{pga}
 2373D.\ L.\ Poole, R.\ G.\ Goebel and R.\ Aleliunas,
 2374``Theorist: A Logical Reasoning System for Defaults and Diagnosis'',
 2375in N. Cercone and G. McCalla (Eds.)
 2376{\it The Knowledge Frontier: Essays in the Representation of
 2377Knowledge},
 2378Springer Varlag, New York, 1987, pp.\ 331-352.
 2379
 2380\bibitem[Reiter80]{reiter80}
 2381R.\ Reiter,
 2382``A Logic for Default Reasoning'',
 2383{\em Artificial Intelligence},
 2384Vol.\ 13, pp 81-132.
 2385                      
 2386\bibitem[Smith86]{smith86}
 2387D.~Smith and M.~Genesereth,
 2388``Ordering Conjunctive Queries'',
 2389{\em Artificial Intelligence}.
 2390
 2391\bibitem[Van Hentenryck87]{vanh}
 2392P.\ Van Hentenryck,
 2393``A Framework for consistency techniques in Logic Programming''
 2394IJCAI-87, Milan, Italy.
 2395\end{thebibliography}
 2396\printindex
 2397\end{document}
 2398*/
 2399
 2400tnumbervars(Term, N, M):- numbervars(Term, N, M).
 2401/*
 2402tnumbervars(Term, N, Nplus1) :-
 2403  var(Term), !,
 2404  Term = var/N,
 2405  Nplus1 is N + 1.
 2406tnumbervars(Term, N, M) :-
 2407  Term =.. [_|Args],
 2408  numberargs(Args,N,M).
 2409
 2410numberargs([],N,N) :- !.
 2411numberargs([X|L], N, M) :-
 2412  numberargs(X, N, N1),
 2413  numberargs(L, N1, M).      
 2414*/
 2415
 2416
 2417:- include(snark_klsnl). 2418
 2419:- thconsult(all_ex). 2420
 2421:- fixup_exports.