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(equiv(X , Y), P,B) :- !,
 1444   nnf(((Y or not X) and (X or not Y)),P,B).
 1445nnf((X == Y), P,B) :- compound(X), compound(Y), !, nnf(equiv(X , Y), P,B).
 1446nnf('<=>'(X , Y), P,B) :- !, nnf(equiv(X , Y), P,B).
 1447
 1448nnf(all(_, Y), P,B) :- !,nnf(Y, P,B).
 1449nnf(exists(E, Y), P, exists(E, B)) :- !,nnf(Y, P,B).
 1450nnf(if(X , Y), P,B) :- !,
 1451   nnf((Y or not X),P,B).
 1452nnf(=>(X,Y), P,B) :- !, nnf(if(X , Y), P,B).
 1453nnf(->(X,Y), P,B) :- !, nnf(if(X , Y), P,B).
 1454
 1455nnf((Y <- X), P,B) :-  !,
 1456   nnf((Y or not X),P,B).
 1457
 1458nnf(^(X, Y), P,B) :- !, nnf(and(X, Y),P,B).
 1459nnf((X & Y), P,B) :- !, nnf(and(X, Y),P,B).
 1460nnf((X , Y), P,B) :- !, nnf(and(X, Y),P,B).
 1461nnf(and(X, Y),P,B) :- !,
 1462   opposite_parity(P,OP),
 1463   nnf((not X or not Y),OP,B).
 1464
 1465nnf((X | Y), P,B) :- !, nnf(xor(X,Y),P,B).
 1466nnf(xor(X, Y), P,B) :- !, nnf(or(and(not(X),Y),and(X,not(Y))),P,B).
 1467
 1468nnf((X ; Y), P,B) :- !, nnf(or(X,Y),P,B).
 1469nnf(v(X, Y), P,B) :- !, nnf(or(X,Y),P,B).
 1470
 1471nnf(or(X,Y),even,(XB,YB)) :- !,
 1472   nnf(X,even,XB),
 1473   nnf(Y,even,YB).
 1474nnf(or(X,Y),odd,(XB;YB)) :- !,
 1475   nnf(X,odd,XB),
 1476   nnf(Y,odd,YB).
 1477
 1478nnf((~ X),P,B) :- !,
 1479   nnf((not X),P,B).
 1480
 1481nnf((not X),P,B) :- !,
 1482   opposite_parity(P,OP),
 1483   nnf(X,OP,B).
 1484
 1485nnf(F,odd,FF):- xlit(F,FF).
 1486
 1487nnf(n(F),even,FF) :- !,xlit(F,FF).
 1488nnf(F,even,n(FF)):- xlit(F,FF).
 1489
 1490xlit(F,F):- \+ compound(F).
 1491xlit({X},{X}).
 1492xlit(=(A,B),sameObjects(A,B)).
 1493xlit(neq(A,B),{dif(A,B)}).
 1494xlit([F|Args],OUT):- maplist(xlit,[F|Args],OUT).
 1495xlit(P,PP):- P=..[F|Args],maplist(xlit,Args,FArgs),PP=..[F|FArgs].
 1496
 1497
 1498/* \end{verbatim}
 1499\index{opposite\_parity}
 1500\begin{verbatim} */
 1501
 1502
 1503opposite_parity(even,odd).
 1504opposite_parity(odd,even).
 1505
 1506
 1507/* \end{verbatim}
 1508
 1509\begin{example} \em
 1510the wff
 1511\begin{quote} \em
 1512(a or not b) and c $\Rightarrow$ d and (not e or f)
 1513\end{quote}
 1514with parity {\em odd} gets translated into
 1515\begin{quote}
 1516$d,(e;f);n(a),b;n(c) $
 1517\end{quote}
 1518the same wff with parity {\em even} (i.e., the negation of the wff)
 1519has negation normal form:
 1520\begin{quote}
 1521$(n(d);e,n(f)),(a;n(b)),c$
 1522\end{quote}
 1523\end{example}
 1524
 1525\subsection{Theorist Declarations}
 1526The following define the Theorist declarations.
 1527Essentially these operators just call the appropriate compiler
 1528instruction. These commands cannot be undone by doing a retry to them;
 1529the compiler assertions will be undone on backtracking.
 1530\index{fact}
 1531\begin{verbatim} */
 1532
 1533
 1534fact(F) :- declare_fact(F),!.
 1535
 1536
 1537/* \end{verbatim}
 1538
 1539The $default$ declaration makes the appropriate equivalences between the
 1540named defaults and the unnamed defaults.
 1541\index{default}
 1542\begin{verbatim} */
 1543
 1544
 1545default((N : H)):-
 1546   !,
 1547   declare_default(N),
 1548   declare_fact((H <-N)),
 1549   !.
 1550default( N ):-
 1551   declare_default(N),
 1552   !.
 1553
 1554
 1555/* \end{verbatim}
 1556\index{default}
 1557\begin{verbatim} */
 1558
 1559
 1560constraint((C)) :-
 1561   declare_constraint(C),
 1562   !.
 1563
 1564                       
 1565/* \end{verbatim}
 1566The $prolog$ command says that the atom $G$ should be proven in the
 1567Prolog system. The argument of the $define$ statement is a Prolog
 1568definition which should be asserted (N.B. that it should be in
 1569parentheses if it contains a ``{\tt :-}''.
 1570\index{prolog}
 1571\begin{verbatim} 
 1572)
 1573*/
 1574
 1575                                   
 1576prolog(( G )) :-
 1577   declare_prolog(G).
 1578
 1579
 1580/* \end{verbatim}
 1581\index{define}
 1582\begin{verbatim} */
 1583
 1584
 1585define( G ):-
 1586   prolog_cl(G).
 1587
 1588
 1589/* \end{verbatim}
 1590
 1591The $explain$ command keeps writing out all of the explanations found.
 1592This is done by finding one, writing the answer, and then retrying so that
 1593the next answer is found. This is done so that the computation is left in
 1594an appropriate state at the end of the computation.
 1595\index{explain}
 1596\begin{verbatim} */
 1597
 1598explain G :- ignore((explain_goal(G)*->fail;(format('~nUntrue: ~p.~n',[G]),forall(explain_goal(~G),true)))).
 1599
 1600explain_goal(G) :-
 1601   (flagth((timing,on))),!,
 1602    statistics(runtime,_),
 1603    expl(G,[],D,A),
 1604    statistics(runtime,[_,Time]),
 1605    writeans(G,D,A),
 1606    format('took ~3d sec.~n~n',[Time])
 1607    
 1608  ;
 1609    expl(G,[],D,A),
 1610    writeans(G,D,A).
 1611/* \end{verbatim}
 1612\index{writeans}
 1613\index{writedisj}
 1614\begin{verbatim} */
 1615
 1616
 1617writeans(G,D,A) :-
 1618   format('~nAnswer is ~p', [G]),
 1619   writedisj(A),
 1620   format('~nTheory is ~p~n', [D]),
 1621   !.
 1622
 1623writedisj([]).
 1624writedisj([H|T]) :-
 1625   writedisj(T),
 1626   format(' or ~p',[H]).
 1627
 1628
 1629/* \end{verbatim}
 1630
 1631\subsection{Prediction}
 1632In \cite{poole:lf} we present a sceptical view of prediction
 1633argue that one should predict what is in every extension.
 1634The following theorem proved in \cite{poole:lf} gives us a hint
 1635as to how it should be implemented.
 1636\begin{theorem} \label{everythm}
 1637$g$ is not in every extension iff there exists a scenario $S$ such
 1638that $g$ is not explainable from $S$.
 1639\end{theorem}
 1640
 1641The intuition is that
 1642if $g$ is not in every extension then there is no reason to rule out
 1643$S$ (based on the information given) and so we should not predict $g$.
 1644                      
 1645We can use theorem \ref{everythm} to consider another way to view membership
 1646in every extension. Consider two antagonistic agents $Y$ and $N$ trying to
 1647determine whether $g$ should be predicted or not. $Y$ comes
 1648up with explanations of $g$, and $N$ tries to find where these explanations
 1649fall down (i.e., tries to find a scenario $S$ which is inconsistent with
 1650all of $Y$''s explanations). $Y$ then tries to find an explanation of $g$
 1651given $S$.
 1652If $N$ cannot find a defeater for $Y$'s explanations then
 1653$g$ is in every extension, and if $Y$ cannot find an explanation from
 1654some $S$ constructed by $N$ then $g$ is not in every extension.
 1655                                                                       
 1656The following code implements this, but (as we cannot implement
 1657coroutines as needed above in Prolog), it may generate more
 1658explanations of the goal than is needed. What we really want is for the
 1659first ``bagof'' to generate the explanations in a demand-driven fashion,
 1660and then just print the explanations needed.
 1661
 1662\index{predict}
 1663\begin{verbatim} */
 1664                     
 1665
 1666predict(( G )):-
 1667  bagof(E,expl(G,[],E,[]),Es),
 1668  predct(G,Es). 
 1669 
 1670predct(G,Es) :- 
 1671  simplify_expls(Es,SEs),
 1672    ( find_counter(SEs,[],S),
 1673      !,
 1674      format('No, ~q is not explainable from ~q.~n',[G,S])
 1675    ; format('Yes, ~q is in all extensions.~nExplanations are:~n',[G]),
 1676      list_scens(1,SEs)).
 1677
 1678
 1679/* \end{verbatim}
 1680
 1681\index{find\_counter}
 1682\begin{verbatim} */
 1683
 1684
 1685find_counter([],S,S).
 1686find_counter([E|R],S0,S2) :-
 1687   member(D,E),
 1688   expl2not(D,S0,S1),
 1689   find_counter(R,S1,S2).
 1690
 1691
 1692/* \end{verbatim}
 1693
 1694\index{list\_scens}
 1695\begin{verbatim} */
 1696
 1697
 1698list_scens(_,[]).
 1699list_scens(N,[H|T]) :-
 1700   format('~q: ~q.~n',[N,H]),
 1701   N1 is N+1,
 1702   list_scens(N1,T).
 1703
 1704
 1705/* \end{verbatim}
 1706
 1707$expl2not(G,T0,T1)$ is true if ground $\neg G$ is explainable starting from
 1708scenario $T0$, with resulting explanation $T1$. No disjunctive answers are
 1709formed.
 1710\index{expl2}
 1711\begin{verbatim} */
 1712
 1713
 1714expl2not(G,T0,T1) :-
 1715   new_lit(`ex_not_`,G,[ths(T0,T,[],D),anc([],[]),ans([],[])],ExG),
 1716   ExG,
 1717   make_ground(D),
 1718   check_consis(D,T,T1).
 1719
 1720
 1721/* \end{verbatim}
 1722
 1723\subsection{Simplifying Explanations}
 1724\index{simplify\_obs}
 1725\begin{verbatim} */
 1726                                   
 1727
 1728simplify_expls([S],[S]).
 1729
 1730simplify_expls([H|T], S) :-
 1731   simplify_expls(T, TS),
 1732   mergeinto(H,TS,S).
 1733
 1734
 1735/* \end{verbatim}
 1736\index{mergeinto}
 1737\begin{verbatim} */
 1738
 1739
 1740mergeinto(L,[],[L]).
 1741
 1742mergeinto(L,[A|R],[A|R]) :-
 1743   instance_of(A,L),
 1744   !.
 1745
 1746mergeinto(L,[A|R],N) :-
 1747   instance_of(L,A),
 1748   !,
 1749   mergeinto(L,R,N).
 1750
 1751mergeinto(L,[A|R],[A|N]) :-
 1752   mergeinto(L,R,N).
 1753
 1754                         
 1755/* \end{verbatim}
 1756
 1757\index{instance\_of}
 1758\begin{verbatim} */
 1759
 1760
 1761instance_of(D,S) :-
 1762   remove_all(D,S,_).
 1763                           
 1764
 1765/* \end{verbatim}
 1766
 1767\subsection{File Handling}
 1768To consult a Theorist file, you should do a,
 1769\begin{verse}
 1770{\bf thconsult} \em filename.
 1771\end{verse}
 1772The following is the definition of {\em thconsult}. Basicly we just
 1773keep reading the file and executing the commands in it until we stop.
 1774\index{thconsult}
 1775\begin{verbatim} */
 1776
 1777thconsult(( File0 )):-
 1778   fix_absolute_file_name(File0,File),
 1779   current_input(OldFile),
 1780   open(File,read,Input),
 1781   set_input(Input),
 1782   th_read(T),
 1783   read_all(T),!,
 1784   set_input(OldFile).
 1785
 1786
 1787/* \end{verbatim}
 1788\index{read\_all}
 1789\begin{verbatim} */
 1790
 1791
 1792:- meta_predicate(read_all(*)). 1793read_all(end_of_file) :- !.
 1794
 1795read_all(T) :-
 1796   ((flagth(( asserting,on))),!; format('~n% ~p.~n',[T])),
 1797   (thmust(T) *-> true ; format('% Warning: ~p failed~n',[T])),
 1798   th_read(T2),
 1799   read_all(T2).
 1800
 1801th_read(T):- read_term(T,[module(snark_theorist),variable_names(Vs)/*,double_quotes(codes)*/]),b_setval('$variable_names',Vs).
 1802                 
 1803thmust(G):- call(G),!.
 1804thmust(G):- rtrace(G),!.
 1805
 1806/* \end{verbatim}
 1807
 1808{\em thtrans} is like the previous version, but the generated code is written
 1809to a file. This code is neither loaded or compiled.
 1810\index{thtrans}
 1811\begin{verbatim} */
 1812
 1813fix_absolute_file_name(I,O):- is_list(I),!,string_to_atom(I,A),absolute_file_name(A,O).
 1814fix_absolute_file_name(I,O):- absolute_file_name(I,O),!.
 1815fix_absolute_file_name(I,O):- I=O.
 1816
 1817
 1818thtrans(( File0 )):-
 1819   fix_absolute_file_name(File0,File),
 1820   string_codes(File, Fname),
 1821   append(Fname,`.pl`,Plfname),
 1822   name(Plfile, Plfname),
 1823   current_output(Oldoutput),
 1824   open(Plfile,write,Output),
 1825   set_output(Output),
 1826   thtrans2out(File),
 1827   close(Output),
 1828   set_output(Oldoutput),!.
 1829   
 1830
 1831thtrans2out(File0):-
 1832   fix_absolute_file_name(File0,File),
 1833   current_input(Oldinput),
 1834   open(File,read,Input),
 1835   set_input(Input),
 1836   format(':- dynamic contrapos_recorded/1.~n',[]),
 1837   format(':- style_check(- singleton).~n',[]),
 1838   format(':- style_check(- discontiguous).~n',[]),
 1839   (setth((asserting,off))),
 1840   th_read(T),
 1841   read_all(T),
 1842   set_input(Oldinput),
 1843   resetth(( asserting)),!.
 1844
 1845/* \end{verbatim}
 1846To compile a Theorist file, you should do a,
 1847\begin{verse}
 1848{\bf thconsult} \em filename.
 1849\end{verse}
 1850
 1851This translates the code to Prolog and then compiles the prolog code.
 1852
 1853{\em thcompile} translates the file to Prolog
 1854which is then compiled using the Prolog compiler.
 1855\index{thcompile}
 1856\begin{verbatim} */
 1857
 1858
 1859thcompile(( File )):-
 1860   (thtrans(( File))),
 1861%   no_style_check(all),
 1862   compile(File).  
 1863
 1864
 1865/* \end{verbatim}
 1866
 1867
 1868\subsection{Flag Setting} \label{flags}
 1869There are a number of Theorist options which can be set by flagth declarations.
 1870Flags, by default, are {\tt on}.
 1871To set the flagth $f$ to value $v$ you can issue the command
 1872\begin{verse}
 1873\bf set $f,v.$
 1874\end{verse}
 1875To find out the value of the flagth $f$ issue the command
 1876\begin{verse}
 1877\bf flagth $f,V.$
 1878\end{verse}
 1879You can reset the value of flagth $f$ to its old value by
 1880\begin{verse}
 1881\bf reset $f.$
 1882\end{verse}
 1883The list of all flags is given by the command
 1884\begin{verse}
 1885\bf flags.
 1886\end{verse}
 1887
 1888The following is the definition of these
 1889\index{set}
 1890\begin{verbatim} */
 1891
 1892
 1893setth((F,V)):-
 1894   prolog_decl((flagth((F,V1)):- !,V=V1)),!.
 1895
 1896
 1897/* \end{verbatim}
 1898\index{flagth}
 1899\begin{verbatim} */
 1900
 1901
 1902flagth((_,on)).
 1903
 1904
 1905/* \end{verbatim}
 1906\index{reset}
 1907\begin{verbatim} */
 1908
 1909
 1910resetth(F) :-
 1911   retract((flagth((F,_)) :- !,_=_)).
 1912
 1913
 1914/* \end{verbatim}
 1915\index{flags}
 1916\begin{verbatim} */
 1917
 1918
 1919flags :- list_flags([asserting,ancestor_search,loop_check,
 1920                     depth_bound,sound_unification,timing]).
 1921list_flags([]).
 1922list_flags([H|T]) :-
 1923   (flagth((H,V))),
 1924   format('flagth((~w,~w)).~n',[H,V]),
 1925   list_flags(T).
 1926                          
 1927
 1928/* \end{verbatim}
 1929\subsection{Compiler Directives}
 1930There are some compiler directives which need to be added to Theorist
 1931code so that the Prolog to assembly language compiler can work
 1932(these are translated into the appropriate Quintus compiler directives).
 1933
 1934So that the Quintus compiler can correctly compile the code,
 1935we should declare that all calls for which we can assert the goal
 1936or the negative are dynamic, this is done by the command
 1937\begin{verse}
 1938\bf dyn $n.$
 1939\end{verse}
 1940This need only be given in files,
 1941and should be given before the atomic symbol $n$ is ever used.
 1942
 1943The following gives the appropriate translation.
 1944Essentially we then must say that the appropriate Prolog code is dynamic.
 1945\index{explainable}
 1946\begin{verbatim} */
 1947
 1948
 1949:- op(1150,fx,(dyn)). 1950dyn(n(G)) :-
 1951   !,
 1952   (dyn(G)).
 1953dyn(G):-
 1954   G =.. [R|Args],
 1955   add_prefix(`ex_not_`,R,ExNR),
 1956   add_prefix(`ex_tru_`,R,ExR),
 1957   length(Args,NA),
 1958   ExL is NA + 3,
 1959   decl_dyn(ExNR/ExL),
 1960   decl_dyn(ExR/ExL),
 1961   add_prefix(`prv_not_`,R,PrNR),
 1962   add_prefix(`prv_tru_`,R,PrR),
 1963   PrL is NA + 2,
 1964   decl_dyn(PrNR/PrL),
 1965   decl_dyn(PrR/PrL).
 1966
 1967decl_dyn(F/A) :- (flagth((asserting, on))),!,dynamic(F/A).
 1968decl_dyn(FA):- format(':- dynamic ~q.~n',[FA]).
 1969
 1970
 1971:- op(1150,fx,explainable). 1972explainable G :- dyn G. 
 1973
 1974                       
 1975/* \end{verbatim}
 1976
 1977\subsection{Using the Compiled Rules}
 1978The use of conditional asserting (prolog\_cl) is twofold.
 1979The first is to write the condition to a file if that is desired.
 1980The second is to be a backtrackable assert otherwise.
 1981\index{prolog\_cl}
 1982\index{flagth,asserting}
 1983\begin{verbatim} */
 1984
 1985% if_dbg(_G):-true,!.
 1986if_dbg(G):-call(G).
 1987
 1988print_clause(C) :- portray_clause(C).
 1989/*
 1990print_clause(C) :- 
 1991   \+ \+ (    
 1992     tnumbervars(C,0,_),
 1993     writeq(C),
 1994     write('.'),
 1995     nl).
 1996*/
 1997%prolog_cl(({C}:-B)):- !, prolog_cl((C:-B)).
 1998%prolog_cl({C}):- !, prolog_cl(C).
 1999
 2000prolog_cl((C:-B)):- \+ \+ ( C = B),!.
 2001prolog_cl(C) :-    
 2002   flagth((asserting,off)),!,
 2003   print_clause(C),!.
 2004
 2005prolog_cl(C) :-
 2006   (clause_asserted(C)->! ; (assertz(C),call(if_dbg(print_clause((C)))))),!.
 2007prolog_cl(C) :-
 2008   if_dbg(print_clause(retract(C))),
 2009   break,retract(C),
 2010   fail.
 2011
 2012
 2013/* \end{verbatim}
 2014$prolog\_decl$ is like the above predicate, but is both
 2015written to the file and asserted.
 2016\index{prolog\_decl}
 2017\begin{verbatim} */
 2018                     
 2019
 2020prolog_decl(C) :-
 2021   flagth((asserting,off)),
 2022   print_clause(C),
 2023   fail.
 2024prolog_decl(C) :-
 2025   asserta(C).
 2026prolog_decl(C) :-
 2027   retract(C),
 2028   fail.          
 2029              
 2030
 2031/* \end{verbatim}
 2032\subsection{Saving Theorist}
 2033The command ``save'' automagically saves the state of the Theorist code
 2034as the command `theorist`. This is normally done straight after compiling this
 2035file.
 2036\index{save}
 2037\begin{verbatim} */
 2038
 2039
 2040save :-
 2041   call(call,quintus:save_program(th,
 2042   format('~nWelcome to THEORIST 1.1.1  (4 December 89 version)
 2043For help type ``h.''.
 2044Any Problems see David Poole (poole@cs.ubc.ca)~n',
 2045  []))).
 2046
 2047
 2048/* \end{verbatim}
 2049\section{Utility Functions}
 2050\subsection{List Predicates}
 2051$append(X,Y,Z)$ is the normal append function
 2052\index{append}
 2053\begin{verbatim} 
 2054append([],L,L).
 2055
 2056append([H|X],Y,[H|Z]) :-
 2057   append(X,Y,Z).
 2058\end{verbatim}
 2059
 2060\index{member}
 2061\begin{verbatim} */
 2062
 2063/*
 2064member(A,[A|_]).
 2065member(A,[_|R]) :-
 2066   member(A,R).
 2067*/
 2068
 2069/* \end{verbatim}
 2070
 2071$id\_member(X,L)$ is true if $X$ is identical to some member of list $L$.
 2072\index{id\_member}
 2073\begin{verbatim} */
 2074
 2075
 2076id_member(A,[B|_]) :-
 2077   A==B.
 2078id_member(A,[_|R]) :-
 2079   id_member(A,R).
 2080
 2081
 2082/* \end{verbatim}
 2083
 2084\index{same\_length}
 2085\begin{verbatim} */
 2086
 2087
 2088same_length([],[]).
 2089same_length([_|L1],[_|L2]) :-
 2090   same_length(L1,L2).
 2091
 2092
 2093/* \end{verbatim}
 2094
 2095\index{remove}
 2096\begin{verbatim} */
 2097
 2098
 2099remove(A,[A|B],B).
 2100remove(A,[H|T],[H|R]) :-
 2101   remove(A,T,R).
 2102
 2103
 2104/* \end{verbatim}
 2105
 2106\index{remove\_all}
 2107\begin{verbatim} */
 2108
 2109
 2110remove_all([],L,L).
 2111remove_all([H|T],L,L2) :-
 2112   remove(H,L,L1),
 2113   remove_all(T,L1,L2).
 2114
 2115
 2116/* \end{verbatim}
 2117
 2118\subsection{Looking at Terms}
 2119\index{variable\_free}
 2120\begin{verbatim} */
 2121
 2122variable_free(X) :- !, \+ ground(X).
 2123
 2124variable_free(X) :-
 2125   atomic(X),
 2126   !.
 2127variable_free(X) :-
 2128   var(X),
 2129   !,
 2130   fail.
 2131variable_free([H|T]) :-
 2132   !,
 2133   variable_free(H),
 2134   variable_free(T).
 2135variable_free(X) :-
 2136   X =.. Y,
 2137   variable_free(Y).
 2138
 2139
 2140/* \end{verbatim}
 2141
 2142\index{make\_ground}
 2143\begin{verbatim} */
 2144
 2145
 2146make_ground(X) :-
 2147   retract(groundseed(N)),
 2148   tnumbervars(X,N,NN),
 2149   asserta(groundseed(NN)).
 2150
 2151:- dynamic groundseed/1. 2152groundseed(26).
 2153
 2154
 2155
 2156/* \end{verbatim}
 2157
 2158\index{reverse}
 2159\begin{verbatim} */
 2160
 2161
 2162reverse([],T,T).
 2163reverse([H|T],A,B) :-
 2164   reverse(T,A,[H|B]).
 2165
 2166
 2167/* \end{verbatim}
 2168                                                     
 2169\subsection{Help Commands}
 2170\index{h}
 2171\begin{verbatim} */
 2172
 2173
 2174(h) :- format('This is Theorist 1.1 (all complaints to David Poole)
 2175For more details issue the command:
 2176   h H.
 2177where H is one of:~n',
 2178[]),
 2179   unix(system('ls /faculty/poole/theorist/help')).
 2180
 2181(h(( H))) :- !,
 2182   add_prefix(`more /faculty/poole/theorist/help/`,H,Cmd),
 2183   unix(system(Cmd)).
 2184                              
 2185
 2186
 2187/* \end{verbatim}
 2188
 2189\subsection{Runtime Considerations}
 2190What is given here is the core part of our current implementation of
 2191Theorist.
 2192This code has been used with Waterloo Unix Prolog, Quintus Prolog,
 2193C-prolog and Mac-Prolog.
 2194For those Prologs with compilers we can actually compile the resulting
 2195code from this translater as we could any other Prolog code;
 2196this make it very fast indeed.
 2197
 2198The resulting code when the Theorist code is of the form of definite clauses 
 2199(the only case where a comparison makes sense,
 2200as it is what the two systems have in common), runs at about a quarter
 2201the speed
 2202of the corresponding interpreted or compiled code of the underlying
 2203Prolog system. About half of this extra cost is
 2204for the extra arguments to unify,
 2205and the other factor is for one membership
 2206of an empty list for each procedure call.
 2207For each procedure call we do one extra Prolog call which immediately fails.
 2208For the definite clause case, the contrapositive of the clauses are never used.
 2209\section{Conclusion}
 2210This paper has described in detail how we can translate Theorist code into
 2211prolog so that we can use the advances in Prolog implementation Technology.
 2212
 2213As far as this compiler is concerned there are a few issues which
 2214arise:
 2215\begin{itemize}                      
 2216\item Is there a more efficient way to determine that a goal can succeed because
 2217it unifies with an ancestor \cite{poole:grace,loveland87}?
 2218\item Can we incorporate a cycle check that has a low overhead?
 2219A simple, but expensive, version is implemented in some versions of
 2220our compiler which checks for identical ancestors.
 2221\item Are there optimal ordering which we can put the compiled
 2222clauses in so that we get answer most quickly \cite{smith86}?
 2223At the moment the compiler just puts the elements of the bodies
 2224in an arbitrary ordering. The optimal ordering depends, of course,
 2225on the underlying control structure.
 2226\item Are there better ways to do the consistency checking when there are
 2227variables in the hypotheses?
 2228\end{itemize}
 2229
 2230
 2231We are currently working on many applications of default and abductive
 2232reasoning.
 2233Hopefully with compilers based on the ideas presented in this paper
 2234we will be able to take full advantage of
 2235advances in Prolog implementation technology while still allowing
 2236flexibility in specification of the problems to be solved.
 2237\section*{Acknowledgements}
 2238This work could not have been done without the ideas,
 2239criticism and feedback from Randy Goebel, Eric Neufeld,
 2240Paul Van Arragon, Scott Goodwin and Denis Gagn\'e.
 2241Thanks to Brenda Parsons and Amar Shan for valuable comments on
 2242a previous version of this paper.
 2243This research was supported under NSERC grant A6260.
 2244\begin{thebibliography}{McDer80}
 2245\bibitem[Brewka86]{brewka86}
 2246G.\ Brewka,
 2247``Tweety -- Still Flying: Some Remarks on Abnormal Birds, Applicable Rules
 2248and a Default Prover'',
 2249{\em Proc.\ AAAI-86}, pp.\ 8-12.
 2250
 2251\bibitem[Chang73]{chang}
 2252C-L.\ Chang and R.\ C-T.\ Lee,
 2253{\em Symbolic Logic and Mechanical Theorem Proving},
 2254Academic Press, 1973.
 2255
 2256\bibitem[Cox82]{cox82}
 2257P.\ T.\ Cox, {\em Dependency-directed backtracking for Prolog Programs}.
 2258
 2259\bibitem[Cox87]{cox87}
 2260P.\ T.\ Cox and T.\ Pietrzykowski, {\em General Diagnosis by Abductive
 2261Inference}, Technical report CS8701, School of Computer Science,
 2262Technical University of Nova Scotia, April 1987.
 2263
 2264\bibitem[Dincbas87]{dincbas}
 2265M.~Dincbas, H.~Simonis and P.~Van Hentenryck,
 2266{\em Solving Large Combinatorial Problems in Logic Programming\/},
 2267ECRC Technical Report, TR-LP-21, June 1987.
 2268
 2269\bibitem[Doyle79]{doyle79}
 2270J.\ Doyle,
 2271``A Truth Maintenance System'',
 2272{\em Artificial Intelligence},
 2273Vol.\ 12, pp 231-273.
 2274
 2275\bibitem[de Kleer86]{dekleer86}
 2276J.\ de Kleer,
 2277``An Assumption-based TMS'',
 2278{\em Artificial Intelligence, Vol.\ 28, No.\ 2}, pp.\ 127-162.
 2279
 2280\bibitem[Edmonson87]{edmonson}
 2281R.~Edmonson, ????
 2282
 2283\bibitem[Enderton72]{enderton}
 2284H.\ B.\ Enderton, {\em A Mathematical Introduction to Logic},
 2285Academic Press, Orlando.
 2286
 2287\bibitem[Genesereth87]{genesereth87}
 2288M.\ Genesereth and N.\ Nilsson,
 2289{\em Logical Foundations of Artificial Intelligence},
 2290Morgan-Kaufmann, Los Altos, California.
 2291
 2292\bibitem[Ginsberg87]{ginsberg87}
 2293M.~L.~Ginsberg, {\em Computing Circumscription\/},
 2294Stanford Logic Group Report Logic-87-8, June 1987.
 2295
 2296\bibitem[Goebel87]{goebel87}
 2297R.\ G.\ Goebel and S.\ D.\ Goodwin,
 2298``Applying theory formation to the planning problem''
 2299in F.\ M.\ Brown (Ed.),
 2300{\em Proceedings of the 1987 Workshop on The Frame Problem in Artificial
 2301Intelligence}, Morgan Kaufmann, pp.\ 207-232.
 2302
 2303\bibitem[Kowalski79]{kowalski}
 2304R.~Kowalski, ``Algorithm = Logic + Control'',
 2305{\em Comm.~A.C.M.} Vol 22, No 7, pp.~424-436.
 2306
 2307\bibitem[Lifschitz85]{lifschitz85}
 2308V.~Lifschitz, ``Computing Circumscription'',
 2309{\em Proc.~IJCAI85}, pp.~121-127.
 2310
 2311\bibitem[Lloyd87]{lloyd}
 2312J.~Lloyd, {\em Foundations of Logic Programming},
 2313Springer-Verlag, 2nd Edition.
 2314
 2315\bibitem[Loveland78]{loveland78}
 2316D.~W.~Loveland, {\em Automated Theorem Proving: a logical basis},
 2317North-Holland, Amsterdam.
 2318
 2319\bibitem[Loveland87]{loveland87}
 2320D.~W.~Loveland, ``Near-Horn Logic Programming'',
 2321{\em Proc. 6th International Logic Programming Conference}.
 2322
 2323\bibitem[McCarthy86]{mccarthy86}
 2324J.\ McCarthy, ``Applications of Circumscription to Formalising
 2325Common Sense Knowledge'', {\em Artificial Intelligence}, Vol.\ 28, No.\ 1,
 2326pp.\ 89-116.
 2327
 2328\bibitem[Moto-Oka84]{pie}
 2329T.~Moto-Oka, H.~Tanaka, H.~Aida, k.~Hirata and T.~Maruyama,
 2330``The Architecture of a Parallel Inference Engine --- PIE'',
 2331{\em Proc.\ Int.\ Conf.\ on Fifth Generation Computing Systems},
 2332pp.~479-488.
 2333
 2334\bibitem[Naish86]{naish86}
 2335L.~Naish, ``Negation and Quantifiers in NU-PROLOG'',
 2336{\em Proc.~3rd Int.\ Conf.\ on Logic Programming},
 2337Springer-Verlag, pp.~624-634.
 2338
 2339\bibitem[Neufeld87]{neufeld87}
 2340E.\ M.\ Neufeld and D.\ Poole,
 2341``Towards solving the multiple extension problem:
 2342combining defaults and probabilities'',
 2343{\em Proc.\ Third AAAI Workshop on Reasoning with Uncertainty},
 2344Seattle, pp.\ 305-312.
 2345
 2346\bibitem[Poole84]{poole:clausal}
 2347D.\ L.\ Poole,
 2348``Making Clausal theorem provers Non-clausal'',
 2349{\em Proc.\ CSCSI-84}. pp.~124-125.
 2350
 2351\bibitem[Poole86]{poole:grace}
 2352D.\ L.\ Poole,
 2353``Gracefully adding Negation to Prolog'',
 2354{\em Proc.~Fifth International Logic Programming Conference},
 2355London, pp.~635-641.
 2356
 2357\bibitem[Poole86]{poole:dd}
 2358D.\ L.\ Poole,
 2359``Default Reasoning and Diagnosis as Theory Formation'',
 2360Technical Report, CS-86-08, Department of Computer Science,
 2361University of Waterloo, March 1986.
 2362
 2363\bibitem[Poole87a]{poole:vars}
 2364D.\ L.\ Poole,
 2365``Variables in Hypotheses'', 
 2366{\em Proc.~IJCAI-87}, pp.\ 905-908.
 2367
 2368\bibitem[Poole87b]{poole:dc}
 2369D.\ L.\ Poole,
 2370{\em Defaults and Conjectures: Hypothetical Reasoning for Explanation and
 2371Prediction}, Research Report CS-87-54, Department of
 2372Computer Science, University of Waterloo, October 1987, 49 pages.
 2373
 2374\bibitem[Poole88]{poole:lf}
 2375D.\ L.\ Poole,
 2376{\it A Logical Framework for Default Reasoning},
 2377to appear {\em Artificial Intelligence}, Spring 1987.
 2378
 2379\bibitem[PGA87]{pga}
 2380D.\ L.\ Poole, R.\ G.\ Goebel and R.\ Aleliunas,
 2381``Theorist: A Logical Reasoning System for Defaults and Diagnosis'',
 2382in N. Cercone and G. McCalla (Eds.)
 2383{\it The Knowledge Frontier: Essays in the Representation of
 2384Knowledge},
 2385Springer Varlag, New York, 1987, pp.\ 331-352.
 2386
 2387\bibitem[Reiter80]{reiter80}
 2388R.\ Reiter,
 2389``A Logic for Default Reasoning'',
 2390{\em Artificial Intelligence},
 2391Vol.\ 13, pp 81-132.
 2392                      
 2393\bibitem[Smith86]{smith86}
 2394D.~Smith and M.~Genesereth,
 2395``Ordering Conjunctive Queries'',
 2396{\em Artificial Intelligence}.
 2397
 2398\bibitem[Van Hentenryck87]{vanh}
 2399P.\ Van Hentenryck,
 2400``A Framework for consistency techniques in Logic Programming''
 2401IJCAI-87, Milan, Italy.
 2402\end{thebibliography}
 2403\printindex
 2404\end{document}
 2405*/
 2406
 2407tnumbervars(Term, N, M):- numbervars(Term, N, M).
 2408/*
 2409tnumbervars(Term, N, Nplus1) :-
 2410  var(Term), !,
 2411  Term = var/N,
 2412  Nplus1 is N + 1.
 2413tnumbervars(Term, N, M) :-
 2414  Term =.. [_|Args],
 2415  numberargs(Args,N,M).
 2416
 2417numberargs([],N,N) :- !.
 2418numberargs([X|L], N, M) :-
 2419  numberargs(X, N, N1),
 2420  numberargs(L, N1, M).      
 2421*/
 2422
 2423
 2424:- include(snark_klsnl). 2425
 2426:- thconsult(all_ex). 2427
 2428:- fixup_exports.