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