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}
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}{,\\\>}
27\author{David Poole\\
28Department of Computer Science,\\
29University of British Columbia,\\
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.
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.
508For the compiler to work properly we need to be able to return
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
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}
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],
693   append(Args, NewArgs, AllArgs),
694   NewReln =.. [NewPred | AllArgs].
695
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
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) :-
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),
1774   set_input(Input),
1777   set_input(OldFile).
1778
1779
1780/* \end{verbatim}
1782\begin{verbatim} */
1783
1784
1787
1789   ((flagth(( asserting,on))),!; format('~n% ~p.~n',[T])),
1790   (thmust(T) *-> true ; format('% Warning: ~p failed~n',[T])),
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,
2240Tweety -- 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},
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,
2264A Truth Maintenance System'',
2265{\em Artificial Intelligence},
2266Vol.\ 12, pp 231-273.
2267
2268\bibitem[de Kleer86]{dekleer86}
2269J.\ de Kleer,
2270An 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},
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,
2291Applying 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,
2323The 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,
2334Towards 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,
2341Making Clausal theorem provers Non-clausal'',
2342{\em Proc.\ CSCSI-84}. pp.~124-125.
2343
2344\bibitem[Poole86]{poole:grace}
2345D.\ L.\ Poole,
2346Gracefully 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,
2352Default 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,
2358Variables 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,
2374Theorist: 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,
2382A Logic for Default Reasoning'',
2383{\em Artificial Intelligence},
2384Vol.\ 13, pp 81-132.
2385
2386\bibitem[Smith86]{smith86}
2387D.~Smith and M.~Genesereth,
2388Ordering Conjunctive Queries'',
2389{\em Artificial Intelligence}.
2390
2391\bibitem[Van Hentenryck87]{vanh}
2392P.\ Van Hentenryck,
2393A 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.