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