Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
\documentclass[11pt]{article} \usepackage{latexsym,amssymb,amsmath,theorem,proof,calc,alltt} %\usepackage{parsetree} %\usepackage{tree-dvips} \usepackage{pst-tree} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % % % VERSION FEB 2001 % % % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \input{mymacros} \newcommand{\close}[1]{\begin{array}{c}{#1} \\ {\times} \end{array}} \newcommand{\clsubs}[2]{\begin{array}{c}{#1} \\ {#2} \end{array}} \newcommand{\stack}[1]{\begin{array}{c}{#1} \end{array}} \newcommand{\barr}{\begin{array}{c}} \newcommand{\earr}{\end{array}} \newcommand{\ttop}{\mbox{\boldmath $\top\!\!\!\!\top$}} \newcommand{\bT}{\mbox{\boldmath $T$}} \newcommand{\cB}{\mbox{$\cal B$}} \newcommand{\href}[1]{} \newcommand{\Nat}{\mathbb{N}} \newcommand{\Exists}{\boldsymbol{\exists\!\!\!\exists}} \newcommand{\Neg}{\boldsymbol{\neg\!\!\!\neg}} \newcommand{\SC}{\ \boldsymbol{;}\ } \newsavebox{\fminibox} \newlength{\fminilength} \newenvironment{fminipage}[1][\linewidth] {\setlength{\fminilength}{#1-2\fboxsep-2\fboxrule-1em}% \bigskip\begin{lrbox}{\fminibox}\quad\begin{minipage}{\fminilength}\bigskip} {\smallskip\end{minipage}\end{lrbox}\noindent\fbox{\usebox{\fminibox}}\bigskip} \newcommand{\bc}{\begin{fminipage}} \newcommand{\ec}{\end{fminipage}} \newenvironment{code}{\begin{fminipage}\begin{alltt}}% {\end{alltt}\end{fminipage}} \newenvironment{pcode}{\begin{fminipage}\begin{alltt}}% {\end{alltt}\end{fminipage} } \renewcommand{\impl}{\Rightarrow} \newtheorem{exercise}[theorem]{Exercise} \newcommand{\produces}{\longrightarrow} \newcommand{\yields}{\Rightarrow} \setlength{\textheight}{22cm} \setlength{\textwidth}{16cm} \setlength{\topmargin}{0cm} \setlength{\oddsidemargin}{0cm} \setlength{\evensidemargin}{0cm} \setlength{\parindent}{0 ex} \setlength{\parskip}{1.5 ex} \title{Free Hyper Tableaux with Constraints} \author{Jan van Eijck \\ \small\em CWI and ILLC, Amsterdam, Uil-OTS, Utrecht} \date{Draft --- February 2001} \begin{document} \maketitle \begin{abstract} \noindent Hyper tableau reasoning is a form of clausal form tableau reasoning where all negative literals in a clause are resolved away in a single inference step. Free hyper tableaux are a generalization of hyper tableaux, where free universal tableau variables are permitted. Substitutions that close tableau branches serve as constraints on closure of other tableau branches. The paper first introduces free hyper tableaux with constraints, and next presents the full code of {\em FHT\_TAP}, a lazy free hyper tableau theorem prover for FOL. {\em FHT\_TAP} uses lazy lists of instantiating substitutions for the free tableau variables instead of backtracking, with the search for closing substitutions guided by finite lists of constraining substitutions on each tableau branch. \end{abstract} \paragraph{Keywords:} Tableau theorem proving for FOL, hyper tableaux, instance checking, leanTAP, constraint guided proof search, proof search without backtracking. \paragraph{MSC codes:} 03B10, 03F03, 68N17, 68T15 \section{Hyper Tableaux with Constraints} Hyper tableau reasoning was introduced in \cite{BauFurNie:ht}. Like (positive) hyperresolution (see, e.g., \cite{ChaLee:slamtp}), it resolves away all negative literals of a clause in a single inference step, but it combines this with the notion of a tableau style search for counterexamples. Hyper tableau reasoning, in the improved version proposed in \cite{Baumgartner:httng}, allows local universally quantified variables. Free hyper tableau reasoning, to be introduced below, allows global universally quantified variables. The calculus/theorem prover described in this paper combines the following ideas: \begin{itemize} \item The idea from \cite{BauFurNie:ht} to use a single hyper tableau rule on tableau branches that matches all negative literals of a clause against positive literals from a tableau branch. \item The idea to enrich tableau branches with finite lists of constraints on branch closure, in the form of (representations of) substitutions that constrain the potential closing substitutions for the whole tableau. This effectively generalizes (rigid) hyper tableaux to free hyper tableaux. \item The idea from \cite{Baumgartner:httng} to enrich tableau branches with history lists that keep track of the clause instances used in the construction of the branch. New instances are only allowed if they are a proper generalization of all the instances used so far. \item A suggestion from \cite{Giese:pswbui} to do tableau proof search by merging closing substitutions for tableau branches into a closing substitution for the whole tableau. \item A new way to define models from open constrained hypertableaux. \end{itemize} The paper contains the complete Haskell \cite{Haskell98:rep} code of a lazy free hyper tableau theorem prover for FOL. The boxed text constitutes the Haskell program. Instead of doing proof search by backtracking and iterative deepening, {\em FHT\_TAP}\/ generates (finite or infinite) streams of most general closing substitutions for the branches and tries to merge them in a fair way into a closing substitution for the whole tableau. These streams are processed lazily using the lazy execution mechanism of Haskell. Baumgartner \cite{Baumgartner:FDPLL} and Beckert \cite{Beckert:dfpswb} use substitution instances to guide proof search in tableau theorem proving. The present paper replaces this by the use of constraining substitutions. As far as I know, the idea to use lists of substitution representations as constraints on model generation is new. \section{Tableaux and Model Generation} Let $\Sigma$ be a first order signature, and $F_{\text{\bf sko}}$ an infinite set of skolem functions, with $F_{\text{\bf sko}} \cap F_\Sigma = \emptyset$. We call the extended signature $\Sigma^*$, and the extended language $\Ln_{\Sigma^*}$. A $\Ln_{\Sigma^*}$ literal is an $\Ln_{\Sigma^*}$ atom or its negation, and an $\Ln_{\Sigma^*}$ clause is a multiset of $\Ln_{\Sigma^*}$ literals, written as $A_1 \lor \cdots \lor A_m \lor \neg B_1 \lor \cdots \lor \neg B_n$ ($m,n \geq 0$). Let us call all-positive clauses (clauses consisting of a non-empty list of positive literals only) {\em facts}, mixed clauses (clauses with a non-empty set of positive literals and a non-empty set of negative literals) {\em rules}\/ and all-negative clauses {\em checks}. In a Prolog context, all-negative clauses are called goals, but that tag is not appropriate here, for in the calculus we propose here they serve not as goals, but as generators of checks for closure. We occasionally write a rule $A_1 \lor \cdots \lor A_m \lor \neg B_1 \lor \cdots \lor \neg B_n$ as $B_1 \land \cdots \land B_n \Rightarrow A_1 \lor \cdots \lor A_m$. We occasionally write checks (!) as $\neg (B_1 \land \cdots \land B_n)$. The blank check $\neg ()$ is written as $\bot$. A hypertableau over $\Sigma$ is a finitely branching tree with nodes labeled with (sets of) $\Ln_{\Sigma^*}$ facts, or with substitutions. A branch in a tableau $\bT$ is a maximal path in $\bT$. We will the substitutions that label a branch node {\em constraints}\/ on the branch, and we occasionally identify a branch $B$ with the set of its formulas and constraints. A hypertableau for a set $\Phi$ of $\Ln_{\Sigma^*}$ formulas in clause form is constructed as follows. The top node of a tableau is labeled with the set of facts in the clause set $\Phi$. Next, the {\bf Split}\/ rule is applied a finite number of times, until every fact has been split on every branch. Next, there is a (possibly infinite) sequence of applications of {\bf Extend}\/ and of {\bf Constrain}. The variables of a tableau branch are the variables that occur in a literal along the branch. The constraints of a branch (if any) are the substitutions that close the branch. A set of branches in a tableau is {\em connected}\/ if each pair in the set has a variable in common. A tableau {\em bundle}\/ is a maximal set of connected branches. The variables of a bundle is the union of the variables of its branches. Note that bundling a tableau partitions the set of branches of the tableau, and that if a tableau consists of bundles $\cB_1, \ldots, \cB_k$, then $\text{vars}(\cB_i) \cap \text{vars}(\cB_j) = \emptyset$, for $1 \leq i \neq j \leq k$. \begin{center} $ \pstree{\Tr{\cdot}}{ \Tfan \lput{:U}{\rput[r]{N}(0,-.2){{\cal B}_1}} \Tfan \lput{:U}{\rput[r]{N}(0,-.2){{\cal B}_2}} \Tfan \Tfan \Tfan \lput{:U}{\rput[r]{N}(0,-.2){{\cal B}_k}}} $ \end{center} \paragraph{Initialization} Initialization of a tableau starts from the list of all-positive clauses $A_1 \lor \cdots \lor A_n$. If there are no such clauses in a clause set, the set cannot be refuted since in this case we can always build a model for it from just negative facts. Otherwise, put all the all-positive clauses at the start node of the tableau. \paragraph{Split} This rule is applicable to all-positive clauses: \[ \frac{A_1 \lor \cdots \lor A_n} { A_1 \mid \ \ \ \ \cdots \ \ \ \ \mid A_n }. \] This is sound because it is just an application of the $\beta$ tableau rule (the rule for disjunction). \paragraph{Extend} Rule clauses (mixed clauses) are used in the extension rule of FHT reasoning, in the following manner. \[ \frac{A_1 \lor \cdots \lor A_n \lor \neg B_1 \lor \cdots \lor \neg B_m, C_1, \ldots, C_m} { \sigma A_1 \mid \ \ \ \ \cdots \ \ \ \ \mid \sigma A_n }, \] where $n,m \geq 1$, the $C_i$ are positive literals from the current branch (possibly under renaming), and $\sigma$ is a substitution such that $\sigma B_i = \sigma C_i \ \ (1 \leq i \leq m)$. We use prefix notation for substitution composition rather than the more customary postfix notation since our functional implementation below has to conform to prefix notation. The extension rule extends the branch with an instance of a literal from the list $A_1, \ldots , A_n$. To avoid superfluous rule applications, a {\em history list}\/ is kept of all the instances of every clause that were applied to a branch. If the rule is applied with substitution $\sigma$, a condition on the rule application is that $\sigma A_1 \lor \cdots \lor \sigma A_n \lor \neg \sigma B_1 \lor \cdots \lor \neg \sigma B_m$ is not an instance of any of the instances of $A_1 \lor \cdots \lor A_n \lor \neg B_1 \lor \cdots \lor \neg B_m$ that were applied to the branch before. If this condition is met, the rule is applied, and the instance $\sigma A_1 \lor \cdots \lor \sigma A_n \lor \neg \sigma B_1 \lor \cdots \lor \neg \sigma B_m$ is added to the history list. Soundness of the rule is immediate, for the rule is a combination of instantiation of the clause $A_1 \lor \cdots \lor A_n \lor \neg B_1 \lor \cdots \lor \neg B_m$ to $\sigma A_1 \lor \cdots \lor \sigma A_n \lor \neg \sigma B_1 \lor \cdots \lor \neg \sigma B_m$, instantiation of the literals $C_1, \ldots, C_m$ to $\sigma C_1, \ldots, \sigma C_m$, and propositional hyper resolution. Also, the history condition on the rule is fair, for application of proper instances of previously applied clause instances is spurious. \paragraph{Constrain} All-negative clauses (checks) are applied in the constrain of FHT reasoning, in the following manner: \[ \frac{\neg B_1 \lor \cdots \lor \neg B_m, C_1, \ldots, C_m } {\theta}, \] where the $C_i$ are as before, there is a $\sigma$ is such that $\sigma B_i = \sigma C_i \ \ (1 \leq i \leq m)$, and $\theta$ is the restriction of $\sigma$ to the variables of the branch. The substitution $\theta$ is called a closing substitution of the branch, or a branch constraint. Note that a branch may have several closing substitutions; in fact, it may have infinitely many. The closing substitution $\theta$ is added to the set of branch constraints. Soundness of the rule follows again from the fact that the rule is a combination of instantiation of $\neg B_1 \lor \cdots \lor \neg B_m, C_1, \ldots, C_m$, and propositional hyper resolution. \paragraph{Merge Check for Closure} To check a tableau consisting of $n$ branches for closure, apply the following {\em merge check for closure}. It is assumed that the $\sigma_i$ are closing substitutions of the different branches. \[ \frac{\sigma_1, \ \ \ \ \cdots\ \ \ \ , \sigma_n} { \sigma_1 \sqcup \cdots \sqcup \sigma_n }. \] Here $\sigma \sqcup \theta$, the join of $\sigma$ and $\theta$, is the most general substitution $\rho$ such that $\sigma \sqsubseteq \rho$, $\theta \sqsubseteq \rho$, where $\sigma \sqsubseteq \rho$ if $\sigma$ is more general than $\rho$. So $\epsilon$, the substitution that is more general than any, is the bottom of the semilattice given by $\sqsubseteq$. It is convenient to use $\ttop$ for the inconsistent substitution. $\ttop$ tops the semilattice of substitutions, for $\sigma \sqsubseteq \ttop$ for any $\sigma$. Two substitutions $\sigma,\tau$ {\em meet}, or {\em do not merge}, if $\sigma \sqcup \tau = \ttop$. In the merge check it is assumed, of course, that $\sigma_1 \sqcup \cdots \sqcup \sigma_n \neq \ttop$. If $\sigma \sqsubseteq \rho$, and $\rho \neq \ttop$, we call $\rho$ an instance of $\sigma$. The idea of the merge check is that if $\sigma, \theta$ each close a branch and can be merged, then $\sigma \sqcup \theta$ closes both branches, and so on, until the whole tableau is closed. The soundness of the merge check follows from the fact that if a substitution closes a branch then each instance of that substitution will also close the branch. \paragraph{Open and Closed Tableaux} A bundle in a tableau is {\em open}\/ if \begin{itemize} \item either some branch in the bundle carries no constraint, \item all branches in the bundle carry constraints, but there is no way to pick constraints from individual branches and merge them into a single constraint (in the sense of: pick a $\sigma_i$ on each $B_i$ such that $\sigma_1 \sqcup \cdots \sqcup \sigma_n \neq \ttop$). \end{itemize} A hypertableau is {\em open}\/ if it has an open bundle, otherwise it is {\em closed}. Note that a closed tableau has a substitution that closes all the branches. For if a bundle $\cal B$ is closed, $\cal B$ is closed by a single substitution $\sigma$. Since different bundles have no variables in common, their most general closing substitutions can always be merged. An assignment $\alpha$ in a model $\M$ meets a constraint $\theta$ if there is a $v \in \dom(\theta)$ with $\alpha(v) \neq \ldb \theta v \rdb^\M_\alpha$, where $\ldb \cdot \rdb^\M_\alpha$ gives the term interpretation in the model with respect to $\alpha$. The idea of the constraints is to {\em forbid}\/ certain variable interpretations! Note that the constraint $\epsilon$ can never be met. An assignment $\alpha$ satisfies a tableau $T$ in a model $\M$ if there is a branch $B$ of $T$ such that $\alpha$ meets all constraints on $B$, and $\M \models_\alpha L$ for all positive literals $L$ on $B$. A tableau $T$ is satisfiable if for some model $\M$ it is the case that all assignments $\alpha$ for $\M$ satisfy $T$ in $\M$. \begin{lemma} If $\Phi$ is a satisfiable set of clauses, then any tableau for $\Phi$ is satisfiable. \end{lemma} \begin{proof} Let $T$ be a tableau for $\Phi$. Then there is a sequence of tableaux $T_1, \ldots, T_n = T$, such that $T_1$ consists of a single node with the facts of $\Phi$, and $T_{i+1}$ is constructed from $T_i$ by an application of {\bf Split}, {\bf Extend} or {\bf Constrain}. To prove by induction on $n$ that $T$ is satisfiable, we have to check that satisfiability is preserved by each of these steps. {\bf Split} and {\bf Extend} are obvious. For {\bf Constrain}, assume that $\M \models_\alpha T_i$, and $T_{i+1}$ is the result of applying {\bf Constrain} to $T_i$. Assume the branch is $B$, the check formula is $\neg (B_1 \land \cdots \land B_k)$, the branch literals used in the rule are $C_1, \ldots, C_k$, the matching substitution is $\sigma$, and the restriction of $\sigma$ to the variables in $B$ is $\theta$. In case $\alpha$ satisfies a branch different from $B$ then the application of {\bf Constrain} will not affect this, so there is nothing to prove. Suppose, therefore, that $\alpha$ satisfies only $B$. We have to show that $\alpha$ meets the constraint $\theta$. Assume for a contradiction that this is not the case. Then we have for all variables in $\dom(\theta)$ that $\alpha(v) = \ldb \theta v \rdb^\M_\alpha$. \end{proof} Any tableau constructed for a satisfiable set of clauses $\Phi$ \begin{theorem}[Soundness] If there is a hypertableau refutation for a clause set $\Phi$, then $\Phi$ is unsatisfiable. \end{theorem} \begin{proof} \end{proof} A substitution $\theta$ is {\em compatible}\/ with a branch $B$ if $\theta$ meets all constraints $\sigma$ on $B$. A substitution $\theta$ is {\em compatible}\/ with a bundle $\cB$ if $\theta$ is compatible with at least one branch $B$ of $\cB$. The following lemma is crucial for model generation. \begin{lemma}[Compatibility Lemma] If a tableau bundle ${\cal B}$ is open, then every ground substitution $\theta$ for $\text{vars}({\cal B})$ is compatible with ${\cal B}$. \end{lemma} \begin{proof} Assume ${\cal B}$ consists of branches $B_1, \ldots, B_n$. We have to show that every ground substitution is compatible with at least one $B_i$. Suppose $\theta$ is a ground substitution for $\text{vars}({\cal B})$ that is not compatible with any $B \in {\cal B}$. Then for each of the $B_i$ there is a $\sigma_i$ such that $\sigma_i \sqcup \theta \neq \ttop$. Since $\theta$ is ground, $\sigma_i \sqcup \theta = \theta$, i.e., $\sigma_i \sqsubseteq \theta$. It follows that $\sigma_1 \sqcup \cdots \sqcup \sigma_n \sqsubseteq \theta$, and contradiction with the assumption that ${\cal B}$ is open. \end{proof} \commentout{ An instance of a bundle $\cB$ is the result of applying a substitution $\sigma$ that is compatible with $\cB$ to all positive literals of $\cB$. } Now consider term models built from the (infinite) Herbrand universe consisting of all ground terms of $\Ln_{\Sigma^*}$. Such a model is completely specified by a set of ground positive literals. In general, these sets of ground literals will be infinite. \begin{lemma}[Satisfiability Lemma] Every open tableau is satisfiable. \end{lemma} \begin{proof} Note that in the Herbrand universe, ground substitutions play the role of assignments. To satisfy a tableau $T$ in a Herbrand model, all we have to do is look at all the ground instances of the tableau. To generate a model from an open hypertableau, proceed as follows. Pick an open bundle $\cal B$. \begin{itemize} \item If there is an unconstrained $B \in {\cal B}$, the set of all ground instances of the positive literals along $B$ constitutes a model for the tableau. It is clear that the model satisfies the tableau. \item If all branches in ${\cal B}$ are constrained, then generate ground instances from ground substitutions, as follows. For every ground substitution $\theta$ with $\dom(\theta) = \text{vars}({\cal B})$, collect the ground instances of the positive literals along a path that is compatible with $\theta$; according the compatibility lemma, there must be at least one such path. The union of the sets of ground positive literals collected from the various branches constitutes a model for the tableau. Again, it is clear that the model satisfies the tableau. \end{itemize} \end{proof} \section{Example Derivations: Informal Discussion} Let us first agree on some conventions for tableau representation. To represent an application of extension in the tableau, we just have to write the rule instance $\sigma B_1 \land \cdots \land \sigma B_n \Rightarrow \sigma A_1 \lor \cdots \lor \sigma A_m$, and the branch extensions with the list of daughters $\sigma A_1$ ... $\sigma A_m$, as follows: \begin{center} $ \pstree{\Tr{\sigma B_1 \land \cdots \land \sigma B_n \Rightarrow \sigma A_1 \lor \cdots \lor \sigma A_m}}{ \Tr{\sigma A_1} \Tfan[linestyle=dotted,fansize=3] \Tr{\sigma A_m}} $ \end{center} In case there is just one consequent, we suppress the branching, and let the detachment of the new literal $\sigma A$ be understood from context: \begin{center} $ \Tr{\sigma B_1 \land \cdots \land \sigma B_n \Rightarrow \sigma A} $ \end{center} We represent applications of the constraint rule as: \begin{center} $ \Toval{\clsubs{\neg (\sigma B_1 \land \cdots \land \sigma B_n)}{\sigma'}} $ \end{center} where $\sigma'$ is the restriction of $\sigma$ to the variables on the current branch. $P,Q,R, \ldots$ are used for predicates, $x, y, z, u, \ldots$ for variables, $a,b,c, \ldots$ for individual constants (skolem constants), $f, \ldots$ for skolem functions. \paragraph{Syllogistic Reasoning} To prove the syllogism {\em Barbara}\/ by hypertableau reasoning, one must refute its negation, which has the following clause form. The constant $c$ is the skolem constant for the existential quantifier in the negation of $\forall x (Px \Rightarrow Rx)$. \[ P x \Rightarrow Q x, Q y \Rightarrow R y, P c, \neg R c. \] The hypertableau for this example looks as follows: \begin{center} $\pstree[nodesepB=3pt]{\Tr{Pc}} {\pstree{\Tr{Pc \Rightarrow Qc}} {\pstree{\Tr{Qc \Rightarrow Rc}} {\Toval{\clsubs{\neg Rc}{\epsilon}}}}} $ \end{center} This tableau closes, with substitution $\epsilon$. \paragraph{Reasoning about Relations} To prove that every transitive and irreflexive relation is asymmetric, we refute the clause form of its negation: \[ Rxy \land Ryz \Rightarrow Rxz, \neg Ruu, Rab, ba, \] where the $Rab, Rba$ provide the witnesses of asymmetry. \begin{center} $\pstree[nodesepB=3pt]{\Tr{Rab,Rba}} {\pstree{\Tr{Rab \land Rba \Rightarrow Raa}} {\Toval{\clsubs{\neg Raa}{\epsilon}}}}$ \end{center} To apply the check, we substitute $a$ for $u$, but the restriction of of the substitution to the tableau variables is $\epsilon$, so $\epsilon$ is the closing substitution of the tableau. \paragraph{Generation of Multiple Closing Substitutions} If we try to refute \[ O x y, \neg O a b, \neg O b c, \] we generate the following two instances of $O x y$, \begin{center} \def\dedge{\ncline[linestyle=dotted]} $ \pstree{\Tr{Oxy}}{ \pstree{\Toval{\clsubs{\neg Oab}{[x \mapsto a, y \mapsto b]}}}{ \Toval{\clsubs{\neg Obc}{[x \mapsto b, y \mapsto c]}}}} $ \end{center} In this case, the order in which we generate the closing substitutions does not matter. If the branch would be part of a larger tree, then both closing substitutions $[x \mapsto a, y \mapsto b], [x \mapsto b, y \mapsto c]$ are candidates for closing the whole tree. If the branch is part of an open tableau, then both substitutions act as constraints on branch satisfaction. \paragraph{Incompatibility of Closing Substitutions} Consider \[ Px \lor Qx, \neg Pa, \neg Qb. \] Here is a hypertableau for this clause set: \begin{center} $\pstree{\Tr{Px \lor Qx}}{ \pstree{\Tr{Px}}{\Toval{\clsubs{\neg Pa}{[x \mapsto a]}}} \pstree{\Tr{Qx}}{\Toval{\clsubs{\neg Pb}{[x \mapsto b]}}}}$ \end{center} This tree is not closed, for the two substitutions $[x \mapsto a]$ $[x \mapsto b]$ do not merge. \paragraph{Closure by Merge} Consider \[ Sxy \lor Syx, \neg Sab, \neg Sba. \] A hypertableau for this clause set: \begin{center} $\pstree{\Tr{Sxy \lor Syx}}{ \pstree{\Tr{Sxy}}{\Toval{\clsubs{\neg Sab}{[x \mapsto a, y \mapsto b]}}} \pstree{\Tr{Syx}}{\Toval{\clsubs{\neg Sba}{[x \mapsto b, y \mapsto b]}}}}$ \end{center} The closing substititutions are compatible (in fact, identical), so the tableau closes. \paragraph{An AI Puzzle} If $a$ is green, $a$ is on top of $b$, $b$ is on top of $c$, and $c$ is not green, then there is a green object on top of an object that is not green. For a hypertableau refutation, refute the clause form of its negation: \[ G a, \neg G c, O a b, O b c, G x \land O x y \Rightarrow Gy. \] \begin{center} $\pstree{\Tr{Ga, Oab, Obc}} {\pstree{\Tr{Ga \land Oab \Rightarrow Gb}} {\pstree{\Tr{Gb \land Obc \Rightarrow Gc}} {\Toval{\clsubs{\neg Gc}{\epsilon}}}}} $ \end{center} A more interesting variant results if we swap positive and negative literals in the example, as follows: \[ \neg Ga , Gc , \neg Oab, \neg Obc , Gx \Rightarrow Gy \lor Oyx. \] This is not in the Horn fragment of FOL, so definitely beyond Prolog. Here is a tableau for it. Note that when the rule $Gx \Rightarrow Gy \lor Oyx$ is used for the second time, its variables are first renamed. \begin{center} $\pstree{\Tr{Gc}} {\pstree{\Tr{Gc \Rightarrow Gy \lor Oyc}}{ \pstree{\Tr{Gy}}{ \pstree{\Toval{\clsubs{\neg Ga}{[y \mapsto a]}}}{ \pstree{\Tr{Gy \Rightarrow Gy' \lor Oyy'}}{ \pstree{\Tr{Gy'}}{\Toval{\clsubs{\neg Ga}{[ y' \mapsto a]}}} \pstree{\Tr{Oyy'}}{ \pstree{\Toval{\clsubs{\neg Oab}{[y' \mapsto a, y \mapsto b]}}}{ \Toval{\clsubs{\neg Obc}{[y' \mapsto b, y \mapsto c]}}} } } } } \pstree{\Tr{Oyc}}{ \Toval{\clsubs{\neg Obc}{[y \mapsto b]}}}}} $ \end{center} This tableau closes, for the substitution $[y' \mapsto a, y \mapsto b]$ closes every branch. This closing substitution is found by an attempt to merge closing substitutions of the individual branches. Other possibilities fail. In particular, the substitution $[y' \mapsto b, y \mapsto c]$ closes the middle branch all right, but it clashes with both substitutions that close the lefthand branch, either on the $y$ or on the $y'$ value, and with the substitution that closes the rightmost branch on the $y$ value. \paragraph{Infinitary Tableau Development} There are relations that are transitive, irreflexive and serial. The attempt to refute this combination of properties should lead to an open hypertableau. In fact, the model for this clause set is infinite. \[ Rxy \land Ryz \Rightarrow Rxy, Ru fu. \] The following infinitary tree is generated: \begin{center} $\def\dedge{\ncline[linestyle=dotted]} \pstree[nodesepB=3pt]{\Tr{Ru fu,Rx'_3fx'_3}} {\pstree{\Tr{Ru fu \land Rfu ffu \Rightarrow Ru ffu}} {\pstree{\Tr{Ru fu \land Rfu fffu \Rightarrow Ru fffu}}{ \pstree{\Tr{Ru ffu \land Rffu ffffu \Rightarrow Ru fffu}}{ \Tfan[linestyle=dotted]}}}} $ \end{center} Note that new instances of the rule $Rxy \land Ryz \Rightarrow Rxy$ keep getting generated. The tableau will not close, and tableau development will not be stopped by the check on instantiations, for new instances of the rule will keep turning up. \paragraph{No All-Positive Clause Present} Every clause set that contains no all-positive clauses is satisfiable in a model with a single object satisfying no atomic predicates. Example: a model for transitivity and irreflexivity. \[ Rxy \land Ryz \Rightarrow Rxy, \neg Ru u. \] No hypertableau rule is applicable to such a clause set. \paragraph{Open Tableau; No Further Rules Applicable} \[ Rxy \Rightarrow Rxz \lor Rzy, Ruu. \] \begin{center} $\pstree{\Tr{Ruu}}{ \pstree{\Tr{Ruu \Rightarrow Ruz \lor R zu}}{ \pstree{\Tr{Ruz}}{ \pstree{\Tr{Ruz \Rightarrow Ruz' \lor Rz'z}}{ \Tr{Ruz'} \Tr{Rz'z}}} \pstree{\Tr{Rzu}}{ \pstree{\Tr{Rzu \Rightarrow Rzz'' \lor Rz''u}}{ \Tr{Rzz''} \Tr{Rz''u}}}}} $ \end{center} No further branch extensions are generated, as on all branches the next instance of $Rxy \Rightarrow Rxz \lor Rzy$ is a variant of an instance that has already been used on the branch. Note that renaming of variables is necessary in the second and the third application of the rule $Rxy \Rightarrow Rxz \lor Rzy$. \paragraph{Model Generation Example} \[ Rxy \lor Sxy , \neg Rz a, \neg S u b. \] \begin{center} $\pstree{\Tr{Rxy \lor Sxy}}{ \pstree{\Tr{Rx y}}{ \Toval{\clsubs{\neg Rx a}{[ y := a, z := x]}}} \pstree{\Tr{Sx y}}{ \Toval{\clsubs{\neg Sx b}{[y := b, u := x]}}}} $ \end{center} The tableau does not close, for the two substitutions disagree on the value for $y$. There are no further rule applications, so we have an open tableau. A model for the clause set is not generated by a single branch in this case, as the two branches share variables. To generate a model from the tableau, proceed as follows. Take all ground instances of $Rxy$ except for those that map $y$ to $a$, and all ground instances of $Sxy$ except for those that map $y$ to $b$. The example illustrates a case where an appropriate model cannot be distilled from a single branch. A model for the lefthand branch, e.g., would not contain any $S$ facts, and would therefore fail to satisfy $\forall xy(Rxy \lor Sxy)$, since the model has to avoid all instances of $Rxa$. \commentout{ \section{Indices, Terms, Formulas} \begin{code} module FHT_TAP where import List import Trace type Name = String type Index = Integer type Id = (Name,Index) data Term = Var Id | Struct Id [Term] deriving (Eq,Show) \end{code} %\begin{code} %instance Show (a -> b) where % showsPrec p _ = showString "<>" %\end{code} We define an ordering on terms. \begin{code} instance Ord Term where compare (Var x) (Var y) = compare x y compare (Var x) _ = LT compare _ (Var y) = GT compare (Struct a ts) (Struct b rs) | a == b = compare ts rs | a < b = LT | a > b = GT \end{code} Check whether a term is a variable. \begin{code} isVar :: Term -> Bool isVar (Var _) = True isVar _ = False \end{code} Formulas according to $F ::= \text{At} \mid \neg F \mid \land_i F_i \mid \lor_i F_i \mid \forall v F \mid \exists v F$. \begin{code} data Form = Atom Id [Term] | Eq Term Term | Neg Form | Conj [Form] | Disj [Form] | Forall Id Form | Exists Id Form deriving (Eq,Ord,Show) \end{code} Note that \verb^Disj []^ serves as $\bot$, \verb^Conj []^ as $\top$. \section{Variables in Terms} \verb^varsInTerm^ and \verb^varsInTerms^ give the variables that occur in a term or a term list. Variable lists should not contain duplicates; the function \verb^nub^ cleans up the variable lists. \begin{code} varsInTerm :: Term -> [Id] varsInTerm (Var i) = [i] varsInTerm (Struct i ts) = varsInTerms ts varsInTerms :: [Term] -> [Id] varsInTerms = nub . concat . map varsInTerm \end{code} \section{Substitutions} Representations of substitutions are lists of bindings, and bindings are identifier/term pairs. \begin{code} type Subst = [(Id,Term)] \end{code} The identity substitution $\epsilon$. \begin{code} epsilon :: Subst epsilon = [] \end{code} Domain and range of a substitution. \begin{code} dom :: Subst -> [Id] dom = map fst rng :: Subst -> [Term] rng = map snd \end{code} The restriction of a substitution to a list of variables: \begin{code} restriction :: [Id] -> Subst -> Subst restriction ids sigma = filter (\ x -> (fst x) `elem` ids) sigma \end{code} Check whether a substitution is a renaming. \begin{code} isRenaming :: Subst -> Bool isRenaming sigma = all isVar rngSigma && (nub rngSigma) == rngSigma where rngSigma = rng sigma \end{code} Application of a substitution to an identifier. \begin{code} appI :: Subst -> Id -> Term appI [] y = (Var y) appI ((x,x'):xs) y | x == y = x' | otherwise = appI xs y \end{code} Application of a substitution to a term or a term list. \begin{code} appT :: Subst -> Term -> Term appT b (Var y) = appI b y appT b (Struct n ts) = Struct n (appTs b ts) appTs :: Subst -> [Term] -> [Term] appTs b = map (appT b) \end{code} Application of a substitution to a formula or a formula list. \begin{code} appF :: Subst -> Form -> Form appF b (Atom a ts) = Atom a (appTs b ts) appF b (Neg form) = Neg (appF b form) appF b (Conj forms) = Conj (appFs b forms) appF b (Disj forms) = Disj (appFs b forms) appF b (Forall v form) = Forall v (appF b' form) where b' = filter (\ (x,x') -> x /= v) b appF b (Exists v form) = Exists v (appF b' form) where b' = filter (\ (x,x') -> x /= v) b appFs :: Subst -> [Form] -> [Form] appFs b = map (appF b) \end{code} \section{Composition of Substitution Representations} Recall the definition of $\circ$, the syntactic operation of composition of substitution representations: \begin{quote} Let $\theta = [t_1/v_1, \ldots, t_n/v_n]$ and $\rho = [r_1/w_1, \ldots, r_m/w_m]$ be substitution representations. Then $\theta \circ \rho$ is the result of removing from the sequence \[ [\theta(r_1)/w_1, \ldots, \theta(r_m)/w_m, t_1/v_1, \ldots, t_n/v_n] \] the bindings $\theta(r_i)/w_i$ for which $\theta(r_i) = w_i$, and the bindings $t_j/v_j$ for which $v_j \in \{ w_1, \ldots, w_m \}$. \end{quote} Composition of substitutions: {\tt compose xs ys} implements application of substitution {\tt xs} after substitution {\tt ys}.\footnote{To remain close to the prefix notation for functions of the implementation language, we will write substitutions as prefix operators, and read composition of substitutions $\sigma \rho$ as `$\sigma$ after $\rho$'.} \begin{code} compose :: Subst -> Subst -> Subst compose xs ys = (filter (\ (y,y') -> y' /= (Var y)) [ (y,(appT xs y')) | (y,y') <- ys ]) ++ (filter (\ (x,x') -> x `notElem` (dom ys)) xs) \end{code} \section{Generating Skolem Terms} The skolem term for an existential $\exists v F$ will depend on all universal quantifiers that have scope over $\exists v F$. To keep track of those, maintain a list of identifiers for the variables of the outscoping universal quantifiers. A skolem term is constructed from an identifier list and an index as follows. The identifiers represent all the universal parameters that the skolem term depends on. \begin{code} skolem :: [Id] -> Index -> Term skolem is i = Struct ("sk",i) [ (Var x) | x <- is ] \end{code} \section{From Standard Form to Quantifier Free Form} The function \verb^insrt^ inserts items into an ordered list while ensuring that the list remains ordered and without duplicates. \begin{code} insrt :: Ord a => a -> [a] -> [a] insrt i = nub . (insert i) \end{code} Rather than first putting a formula in prenex normal form and then skolemize it, the function \verb^qff^ directly skolemizes. This has the advantage that the skolem functions do not get cluttered with unnecessary arguments. Consider example $\forall x \exists y Rxy \land \forall x' \exists y' Sx'y'$. Direct skolemization yields $\forall x Rxf(x) \land \forall x' Sx'f'(x')$, which can be written without quantifiers on the assumptions that all free variables are universal: $Rxf(x) \land Sx'f'(x')$. If one first puts the formula in prenex form, one may get $\forall x \exists y\forall x' \exists y' (Rxy \land Sx'y')$, which leads to a spurious argument in one of the skolem functions: $Rxf(x) \land Sx'f'(x,x')$. The quantifier free form function \verb^qff^ computes by a call to \verb^qff'^, an auxiliary function that has a list argument for the current list of wide scope quantifier indices and a Boolean argument to indicate the current polarity, and that passes parameters for variable and skolem indices. \begin{code} qff :: Form -> Form qff f = fst (qff' f [] True 0 0) where fst (a,_,_) = a \end{code} Arguments of \verb^qff'^: the first argument is the current formula to be put in quantifier free form, the second the list of identifiers for universal quantifiers that have scope over the current formula, the third the polarity of the current context (\verb^True^ for positive, \verb^False^ for negative), and the fourth and fifth the next available index for a universal variable, and the next available index for a skolem constant, respectively. \begin{code} qff' :: Form -> [Id] -> Bool -> Index -> Index -> (Form,Index,Index) qff' (Atom n ts) ixs pol i k = ((Atom n ts),i,k) qff' (Conj fs) ixs pol i k = ((Conj fs'),j,l) where (fs',j,l) = qffs fs ixs pol i k qff' (Disj fs) ixs pol i k = ((Disj fs'),j,l) where (fs',j,l) = qffs fs ixs pol i k qff' (Forall x f) ixs True i k = qff' (appF b f) ixs' True (i+1) k where b = [(x,Var new)] new = ('X':(show i), 0) ixs' = insrt new ixs qff' (Forall x f) ixs False i k = qff' (appF b f) ixs False i (k+1) where b = [(x,(skolem ixs k))] qff' (Exists x f) ixs True i k = qff' (appF b f) ixs True i (k+1) where b = [(x,(skolem ixs k))] qff' (Exists x f) ixs False i k = qff' (appF b f) ixs' False (i+1) k where b = [(x,Var new)] new = ('X':(show i), 0) ixs' = insrt new ixs qff' (Neg f) ixs pol i k = ((Neg f'),j,l) where (f',j,l) = qff' f ixs (not pol) i k \end{code} \verb^qffs^ puts lists of formulas in quantifier free form. Same arguments as \verb^qff'^. \begin{code} qffs :: [Form] -> [Id] -> Bool -> Index -> Index -> ([Form],Index,Index) qffs [] _ _ i k = ([],i,k) qffs (f:fs) ixs pol i k = ((f':fs'),j,l) where (f', i1, k1) = qff' f ixs pol i k (fs',j , l) = qffs fs ixs pol i1 k1 \end{code} \section{Clauses and Substitution on Clauses} A clause consists of a list of positive literals followed by a list of negative literals. \begin{code} data Plit = T Id [Term] deriving (Eq,Ord,Show) data Nlit = F Id [Term] deriving (Eq,Ord,Show) type Cl = ([Plit],[Nlit]) \end{code} Conversion of positive and negative literals to terms: \begin{code} p2t :: Plit -> Term p2t (T a ts) = (Struct a ts) n2t :: Nlit -> Term n2t (F a ts) = (Struct a ts) \end{code} Application of a substitution to a (positive or negative) literal, a list of (positive or negative) literals. \begin{code} appPlit :: Subst -> Plit -> Plit appPlit b (T a ts) = T a (appTs b ts) appNlit :: Subst -> Nlit -> Nlit appNlit b (F a ts) = F a (appTs b ts) appPlits :: Subst -> [Plit] -> [Plit] appPlits b = map (appPlit b) appNlits :: Subst -> [Nlit] -> [Nlit] appNlits b = map (appNlit b) \end{code} Application of a substitution to a clause or a clause list. \begin{code} appCl :: Subst -> Cl -> Cl appCl b (pos,neg) = (appPlits b pos, appNlits b neg) appCls :: Subst -> [Cl] -> [Cl] appCls b = map (appCl b) \end{code} Variables in a positive or negative literal, and in a clause: \begin{code} varsInPlit :: Plit -> [Id] varsInPlit p = varsInTerm (p2t p) varsInNlit :: Nlit -> [Id] varsInNlit n = varsInTerm (n2t n) varsInClause :: Cl -> [Id] varsInClause (pos,neg) = nub (concat (map varsInPlit pos ++ map varsInNlit neg)) varsInClauses :: [Cl] -> [Id] varsInClauses = nub . concat . map varsInClause \end{code} \section{From Quantifier Free Form to Clausal Form} Function \verb^fuseLists^ will be used to keep the literals in the clauses ordered. \begin{code} fuseLists :: Ord a => [a] -> [a] -> [a] fuseLists [] ys = ys fuseLists xs [] = xs fuseLists (x:xs) (y:ys) | x < y = x:(fuseLists xs (y:ys)) | x == y = x:(fuseLists xs ys) | x > y = y:(fuseLists (x:xs) ys) \end{code} Disjunction distribution. Note that the empty disjunction gets represented as the clause \verb^([],[])^. \begin{code} disjList :: [Cl] -> [Cl] disjList [] = [([],[])] disjList [(pos,neg)]= [(pos,neg)] disjList ((pos,neg):cls) = map (disj (pos,neg)) (disjList cls) where disj (pos,neg) (pos',neg') = ((fuseLists pos pos'),(fuseLists neg neg')) \end{code} To put a quantifier free formula in clausal form, one just has to deal with the boolean connectives: \begin{code} cf :: Form -> [Cl] cf (Atom n ts) = [([T n ts],[])] cf (Conj fs) = concat (map cf fs) cf (Disj fs) = disjList (concat (map cf fs)) cf (Neg (Atom n ts)) = [([],[F n ts])] cf (Neg (Conj fs)) = disjList (concat (map (\ f -> cf (Neg f)) fs)) cf (Neg (Disj fs)) = concat (map (\ f -> cf (Neg f)) fs) cf (Neg (Neg f)) = cf f \end{code} To put a formula in clausal form, first put it in quantifier free form, next clausify the result: \begin{code} clause :: Form -> [Cl] clause = cf . qff \end{code} \section{Abbreviations for Examples} Some variable indices: \begin{code} xi = ("x", 0) yi = ("y", 0) zi = ("z", 0) \end{code} Some variable terms: \begin{code} x = Var xi y = Var yi z = Var zi \end{code} Some further terms: \begin{code} a = Struct ("a",1) [] b = Struct ("b",1) [] c = Struct ("c",1) [] zero = Struct ("z",1) [] s = Struct ("s",1) one = s[zero] two = s[one] three = s[two] four = s[three] five = s[four] \end{code} Some predicates: \begin{code} p = Atom ("P",0) q = Atom ("Q",0) r = Atom ("R",0) tP = T ("P",0) fP = F ("P",0) \end{code} \section{Local Renaming of Variables} Rename an identifier in a list by appending a \verb^'^ to its name. \begin{code} renId :: [Id] -> Id -> Id renId ids (n,i) | elem (n,i) ids = (n ++ "'",i) | otherwise = (n,i) \end{code} Local renaming in terms and term lists. \begin{code} renTerm :: [Id] -> Term -> Term renTerm ids (Var x) = Var (renId ids x) renTerm ids (Struct a ts) = Struct a (renTerms ids ts) renTerms :: [Id] -> [Term] -> [Term] renTerms ids = map (renTerm ids) \end{code} Local renaming in (positive and negative) literals, lists of literals, clause, clause lists and substitutions. \begin{code} renPlit :: [Id] -> Plit -> Plit renPlit ids (T a ts) = T a (renTerms ids ts) renNlit :: [Id] -> Nlit -> Nlit renNlit ids (F a ts) = F a (renTerms ids ts) renCl :: [Id] -> Cl -> Cl renCl ids (pos,neg) = (map (renPlit ids) pos, map (renNlit ids) neg) renCls :: [Id] -> [Cl] -> [Cl] renCls ids = map (renCl ids) renSubst :: [Id] -> Subst -> Subst renSubst ids = map (\ (x,x') -> (renId ids x,renTerm ids x')) \end{code} \section{Unification} Unification of terms. Three cases: \begin{itemize} \item Unification of two variables $x$ and $y$ gives the empty substitution if the variables are identical, and otherwise a substitution that binds one variable to the other. \item Unification of $x$ to a non-variable term $t$ fails if $x$ occurs in $t$, otherwise it yields the binding $[t/x]$. \item Unification of $f \bar{t}$ and $g \bar{r}$ fails if the two variable names are different, otherwise it yields the return of the attempt to do term list unification on $\bar{t}$ and $\bar{r}$. \end{itemize} If unification succeeds, a unit list containing a representation of a most general unifying substitution is returned. Return of the empty list indicates unification failure. \begin{code} unifyTs :: Term -> Term -> [Subst] unifyTs (Var x) (Var y) = if x==y then [epsilon] else [[(x,Var y)]] unifyTs (Var x) t2 = [ [(x,t2)] | x `notElem` varsInTerm t2 ] unifyTs t1 (Var y) = [ [(y,t1)] | y `notElem` varsInTerm t1 ] unifyTs (Struct a ts) (Struct b rs) = [ u | a==b, u <- unifyTlists ts rs ] \end{code} Unification of term lists: \begin{itemize} \item Unification of two empty term lists gives the identity substitution. \item Unification of two term lists of different length fails. \item Unification of two term lists $t_1, \ldots, t_n$ and $r_1, \ldots, r_n$ is the result of trying to compute a substitution $\sigma = \sigma_n \circ \cdots \circ \sigma_1$, where \begin{itemize} \item $\sigma_1$ is a most general unifier of $t_1$ and $r_1$, \item $\sigma_2$ is a most general unifier of $\sigma_1(t_2)$ and $\sigma_1(r_2)$, \item $\sigma_3$ is a most general unifier of $\sigma_2\sigma_1(t_3)$ and $\sigma_2\sigma_1(r_3)$, \item and so on. \end{itemize} \end{itemize} \begin{code} unifyTlists :: [Term] -> [Term] -> [Subst] unifyTlists [] [] = [epsilon] unifyTlists [] (r:rs) = [] unifyTlists (t:ts) [] = [] unifyTlists (t:ts) (r:rs) = [ (compose sigma2 sigma1) | sigma1 <- unifyTs t r, sigma2 <- unifyTlists (appTs sigma1 ts) (appTs sigma1 rs) ] \end{code} Unification of literals reduces to unification of (structured) terms. Successful unification returns a unit list containing a most general substitution. Unification failure is indicated by return of the empty list. Unification of positive against positive literal, negative against negative literal, negative against positive literal: \begin{code} unifyP :: Plit -> Plit -> [Subst] unifyP p1 p2 = unifyTs (p2t p1) (p2t p2) unifyN :: Nlit -> Nlit -> [Subst] unifyN n1 n2 = unifyTs (n2t n1) (n2t n2) unifyM :: Nlit -> Plit -> [Subst] unifyM n p = unifyTs (n2t n) (p2t p) \end{code} Extend \verb^unifyM^ to unification of a negative literal against a list of positive literals. If there is no match, unification fails. \begin{code} unifyLitList :: Nlit -> [Plit] -> [Subst] unifyLitList n [] = [] unifyLitList n (p:ps) = unifyM n p ++ unifyLitList n ps \end{code} If we assume that the variables in the (positive) literals that occur in a branch are universally quantified, then we can make {\em renamed copies}\/ of these literals as the need arises. The following function renames a literal that contains occurrences of a given list of variables. We get the list of variables that were `used up' from a match against a literal in the tableau, and we make fresh copies of the positive literals that contain variables from this list. \begin{code} rn :: [Id] -> [Plit] -> [Plit] rn ids [] = [] rn ids (p:ps) | any (\ i -> elem i ids) (varsInPlit p) = p:p':(rn ids ps) | otherwise = p:(rn ids ps) where p' = renPlit ids p \end{code} The function \verb^unif_rn^ tries to match a list of negative literals against a list of positive literals, on the assumption that all negative literals must be unified with a positive literal from the list, and that variables used in a match are renamed (refreshed) in the list of positives (note the call to \verb^rn^). \begin{code} unif_rn :: [Nlit] -> [Plit] -> [Subst] unif_rn [] ps = [epsilon] unif_rn (n:ns) ps = [(compose theta rho) | rho <- unifyLitList n ps, theta <- unif_rn (appNlits rho ns) (appPlits rho ps) ] -- (appPlits rho -- ps) ] -- (rn ((dom rho) ++ (varsInTerms (rng rho))) ps)) ] \end{code} Some examples: \begin{verbatim} FHT_TAP> unif_rn [fP[a]] [tP[x]] [[(("x",0),Struct ("a",1) [])]] FHT_TAP> unif_rn [fP[x]] [tP[a],tP[b]] [[(("x",0),Struct ("a",1) [])],[(("x",0),Struct ("b",1) [])]] FHT_TAP> unif_rn [fP[s[y]],fP[y]] [tP[x]] [[(("x",0),Struct ("s",1) [Var ("x'",0)]),(("y",0),Var ("x'",0))]] FHT_TAP> unif_rn [fP[y],fP[s[y]]] [tP[x]] [[(("y",0),Var ("x",0)),(("x'",0),Struct ("s",1) [Var ("y",0)])]] FHT_TAP> unif_rn [fP[x,s[x]]] [tP[y,z]] [[(("x",0),Var ("y",0)),(("z",0),Struct ("s",1) [Var ("y",0)])]] \end{verbatim} \section{Joining of Substitutions, Unification of Clauses} The join of two substitutions $\theta_1$, $\theta_2$, if it exists, is the most general substitution $\rho$ such that there is a $\sigma$ with $\sigma \circ \theta_1 = \rho$ and $\sigma \circ \theta_2 = \rho$. The most general substitution $\sigma$ that unifies $\theta_1 = [t_1/v_1, \ldots, t_n/v_n ]$ and $\theta_2 = [r_1/w_1, \ldots, r_m/w_m]$ can be constructed by finding a most general unifier $\sigma_1$ for $t_1$ and $\theta_2 (v_1)$, next, a most general unifier $\sigma_2$ for $\sigma_1 (t_2)$ and $\sigma_1\theta_2 (v_2)$, and so on, until we get $\sigma = \sigma_n \cdots \sigma_1$, provided all unifications succeed. The function \verb^unifySubst^ constructs a representation of $\theta_1 \sqcup \theta_2$, the join of $\theta_1$ and $\theta_2$, from the representations of $\theta_1$ and $\theta_2$, by computing $\sigma_n \circ \cdots \circ \sigma_1 \circ \theta_2$, in the manner explained above. Return of \verb^[]^ indicates failure. \begin{code} unifySubst :: Subst -> Subst -> [Subst] unifySubst [] ys = [ys] unifySubst ((x,x'):xs) ys = [ subst | mgu <- unifyTs x' y', subst <- unifySubst (compose mgu xs) (compose mgu ys) ] where y' = appI ys x \end{code} To see that the equation for \verb^unifySubst ((x,x'):xs) ys^ is correct, note that there are two cases to consider: \begin{enumerate} \item \verb^x `notElem` (dom ys)^. In this case, \verb^y' == appI ys x == (Var x)^. Therefore, \verb^mgu^ will be the substitution \verb^[(x,x')]^, and \verb^compose mgu ys^ will contain the binding \verb^(x,x')^, while \verb^compose mgu xs^ will not contain a binding for \verb^x^. \item \verb^x `elem` (dom ys)^, say with binding \verb^(x,y')^. In this case, \verb^appI ys x^ will be \verb^y'^, and \verb^compose mgu ys^ will replace the binding \verb^(x,y')^ by the binding of \verb^x^ to the MGU of \verb^x'^ and \verb^y'^, while \verb^compose mgu xs^ will not contain a binding for \verb^x^. \end{enumerate} Unification of two clauses, by trying to find a most general substitution that makes them equal: \begin{code} unifyCl :: Cl -> Cl -> [Subst] unifyCl (ps1,ns1) (ps2,ns2) = [ theta | sigma <- unifyTlists pts1 pts2, tau <- unifyTlists nts1 nts2, theta <- unifySubst sigma tau ] where pts1 = map p2t ps1 pts2 = map p2t ps2 nts1 = map n2t ns1 nts2 = map n2t ns2 \end{code} \section{Varianthood, Instances, Subsumption} Use \verb^unifySubst^ to give a definition of varianthood for substitutions: \begin{code} variants :: Subst -> Subst -> Bool variants sigma tau = any isRenaming (unifySubst sigma tau) \end{code} Check whether a clause is an instance of another clause. $\phi$ is an instance of $\psi$ if there is a substitution $\sigma$ with $\sigma \phi = \sigma\psi$ with the property that $\sigma$, restricted to the variables of $\phi$, is a renaming. \begin{code} isInstance :: Cl -> Cl -> Bool isInstance phi psi = any isRenaming [(restriction (varsInClause phi) sigma) | sigma <- unifyCl phi psi ] \end{code} A substitution $\sigma$ is subsumed by a substitution $\tau$ if there is a substitution $\theta$ with $\theta \circ \sigma = \theta \circ \tau$ and $\theta$, restricted to the variables occurring in the range of $\tau$, is a renaming. \begin{code} isSubsumed :: Subst -> Subst -> Bool isSubsumed sigma tau = any isRenaming [(restriction ids theta) | theta <- unifySubst sigma tau ] where ids = varsInTerms (rng tau) \end{code} \section{Merging Substitution Streams} For a fair merge of two streams of substitutions, proceed as follows. If one of them is empty, return the empty list. Otherwise, first try to unify the two heads, and next alternate through the following three procedures: \begin{itemize} \item merge the head of the first stream with the tail of the second, \item merge the head of the second stream with the tail of the first, \item merge the two tails. \end{itemize} \begin{code} merge :: [Subst] -> [Subst] -> [Subst] merge xs [] = [] merge [] ys = [] merge (x:xs) (y:ys) = (unifySubst x y) ++ alt3 (mergePair x ys) (mergePair y xs) (merge xs ys) mergePair :: Subst -> [Subst] -> [Subst] mergePair x [] = [] mergePair x (y:ys) = (unifySubst x y) ++ (mergePair x ys) \end{code} Alternation through three or two streams is defined by the following functions: \begin{code} alt3 :: [a] -> [a] -> [a] -> [a] alt3 xs ys [] = alt2 xs ys alt3 xs [] zs = alt2 xs zs alt3 [] ys zs = alt2 ys zs alt3 (x:xs) (y:ys) (z:zs) = x:y:z:(alt3 xs ys zs) alt2 :: [a] -> [a] -> [a] alt2 xs [] = xs alt2 [] ys = ys alt2 (x:xs) (y:ys) = x:y:(alt2 xs ys) \end{code} The function \verb^mergeLst^ merges a finite list of streams $s_1, \ldots, s_n$ of substitutions into a single stream by looking for all possible finite joins $\sqcup \{ \theta_1, \ldots, \theta_n \}$, where $\theta_i$ is a substitution from the $i$-th stream. Since the join $\sqcup \emptyset$ is the identity substitution $\epsilon$, the function call \verb^mergeLst []^ should return \verb^[epsilon]^. \begin{code} mergeLst :: [[Subst]] -> [Subst] mergeLst [] = [epsilon] mergeLst [s] = s mergeLst (s1:s2:streams) = mergeLst ((merge s1 s2):streams) \end{code} \section{Global Variable Renaming} Renaming of index $0$ to $i$ in identifiers, terms and term lists. We assume that we start out from the identifiers in the clause table, where $0$ is the only index that occurs. Global renaming of clauses from the clause table is used to avoid variable clashes. \begin{code} renameId :: Index -> Id -> Id renameId i (x,0) = (x,i) renameId i (x,j) = (x,j) renameTerm :: Index -> Term -> Term renameTerm i (Var x) = (Var (renameId i x)) renameTerm i (Struct a ts) = Struct a (renameTerms i ts) renameTerms :: Index -> [Term] -> [Term] renameTerms i = map (renameTerm i) \end{code} Renaming index $0$ to $i$ in positive literals, negative literals, clauses, clause lists and substitutions. \begin{code} renamePlit :: Index -> Plit -> Plit renamePlit i (T a ts) = T a (renameTerms i ts) renameNlit :: Index -> Nlit -> Nlit renameNlit i (F a ts) = F a (renameTerms i ts) renameCl :: Index -> Cl -> Cl renameCl i (pos,neg) = (map (renamePlit i) pos, map (renameNlit i) neg) renameCls :: Index -> [Cl] -> [Cl] renameCls i = map (renameCl i) renameSubst :: Index -> Subst -> Subst renameSubst i = map (\ (x,x') -> (renameId i x,renameTerm i x')) \end{code} \section{Branches and Histories} We represent a branch as a triple consisting of a list of `pending' positive literals (the literals that still have to be dealt with by means of a clause application), a branch history, and a list of all positive literals of the branch. The branch history is a table that for each clause lists the instances of the clause that were used for extending the branch. If a rule application results in an instance of a clause that is already in the history list for the branch, the application is redundant. The effect of this check is that extensions with a clause instance is allowed only in those cases where the instance is a proper generalization of all instances used so far. \begin{code} type History = Int -> [Cl] type Branch = ([Plit],History,[Plit]) \end{code} The initial history maps every integer to the empty clause instances list. \begin{code} initHistory :: History initHistory = \ i -> [] \end{code} We will need a sorted list of all the positive literals that occur in a list of clauses. \begin{code} positives :: [Cl] -> [Plit] positives = sort . nub . concat . (map fst) \end{code} A clause table for a list of clauses $C = [C_1, \ldots, C_n]$ gives for every negative literal $L$ that occurs in $C$ the clause that results from removal of $L$ from $C$. Every time a branch is extended with a positive literal $P$, we use the clause table to look up the applicable clauses for $P$: the clauses $C$ containing a negative literal $N$ that unifies with $P$. A clause table is a list of triples. The first element of the triple gives the number of the clause in the clause list, the second item the negative literal $L$ that is used for matching, and the third item what is left of the clause if the negative literal $L$ is removed from it. \begin{code} type Table = [(Int, Nlit, Cl)] \end{code} The function \verb^makeTable^ constructs a clause table for a clause list. \begin{code} makeTable :: [Cl] -> Table makeTable cls = [(i, n, (fst (cls!!i), snd (cls!!i))) | i <- [0 .. ((length cls)-1)], n <- snd (cls!!i) ] \end{code} \section{Initialization} Initialize the tableau with the all-positive clauses $P_1 \lor \cdots \lor P_n$ in the clause set. \begin{code} allPos :: Cl -> Bool allPos (_,[]) = True allPos (_,_) = False \end{code} Initialisation starts with the empty branch: no pending calls, an empty history, no positive literals, and no constraints on possible closing substitutions, indicated by a constraint list \verb^[epsilon]^. If there are all-positive clauses, then collect their literals as pending literals for calling the clause table and as positive literals of the branch. \begin{code} initialize :: [Cl] -> [Branch] initialize cls = initialize' cls ([],initHistory,[]) initialize' :: [Cl] -> Branch -> [Branch] initialize' cls (pending,h,lits) = if (find allPos cls) == Nothing then [(pending,h,lits)] else concat [ initialize' cls' (insrt p pending,h,insrt p lits) | p <- pos ] where Just (pos,[]) = find allPos cls cls' = filter (/= (pos,[])) cls \end{code} \section{Matching} The \verb^match^ function is used to match positive literals that have a call in the database with the appropriate database entry. To avoid spurious bindings, the clause table entries are first renamed. If a matching clause in the clause table is found, an attempt is made to unify its negative literals with positive literals in the branch, using the \verb^unif_rn^ function. If this attempt succeeds, the resulting clause instance is checked against the branch history to ensure that it is not a spurious application. The \verb^match^ function returns a list of triples consisting of the position $i$ of the matching clause in the clause list, the substitution $\sigma$ that effects the match, and the clause instance that results from applying $\sigma$ to the clause at position $i$ in the clause list. \begin{code} type Match = (Int,Subst,Cl) \end{code} The arguments of \verb^match^ are: the clause table, the branch history, the pending positive literal, the list of branch literals and a renaming index. \begin{code} match :: Table -> History -> Plit -> [Plit] -> Index -> [Match] \end{code} The function \verb^match^ computes the list of matching clauses for the positive literal, and makes a call to \verb^matchItems^. \begin{code} match table h p lits k = matchItems items h lits k where items = nub [ (i,cl) | (i,n,cl) <- table, unifyM n p /= [] ] \end{code} The function \verb^renameMatches^ applies global renaming to a list of matches. \begin{code} renameMatches :: Index -> [Match] -> [Match] renameMatches k [] = [] renameMatches k ((i,unif,cls):matches) = (i, renameSubst k unif, renameCl k cls) : renameMatches (k+1) matches \end{code} The function \verb^matchItems^ generates unifying substitutions and new clause instances. The variables with index $0$ (from the clause table) are renamed to avoid variable clashes between the matches. It is checked in the branch history that each clause instance is really new. \begin{code} matchItems :: [(Int,Cl)] -> History -> [Plit] -> Index -> [Match] matchItems items h lits k = renameMatches k matches where matches = [(i,unifier,newInstance) | (i,(pos,neg)) <- items, unifier <- unif_rn neg lits, newInstance <- [appCl unifier (pos,neg)], not (any (isInstance newInstance) (h i)) ] \end{code} \begin{verbatim} matchItems items h lits k = [(i,unifier,newInstance) | (i,(pos,neg)) <- items, (posk,negk) <- [renameCl k (pos,neg)], unifier <- unif_rn negk lits, newInstance <- [appCl unifier (posk,negk)], not (any (isInstance newInstance) (h i)) ] \end{verbatim} \section{Show Functions for Tracing} For tracing, it is useful to be able to show the positive literals and the constraining substitutions of an open branch. \begin{code} showLit :: Plit -> String showLit (T n ts) = show n ++ show ts ++ "\n" showLits :: [Plit] -> String showLits [] = "\n" showLits (p:ps) = showLit p ++ showLitsRest ps where showLitsRest [] = "\n" showLitsRest (p:ps) = showLit p ++ showLitsRest ps \end{code} \begin{code} showSub :: Subst -> String showSub [] = "{}\n" showSub (x:xs) = "{" ++ show x ++ showSubRest xs where showSubRest [] = "}\n" showSubRest (x:xs) = show x ++ showSubRest xs \end{code} \begin{code} showSubs :: [Subst] -> String showSubs [] = "nothing\n" showSubs (s:ss) = showSub s ++ showSubsRest ss where showSubsRest [] = "\n" showSubsRest (s:ss) = showSub s ++ showSubsRest ss ++ "\n" \end{code} \section{History Updating, Literal Distribution} The application of the clause at position $i$ under substitution $\sigma$ to a tableau branch gives rise to an update of the branch history. \begin{code} update :: History -> (Int,Cl) -> History update h (i,cl) k | i == k = insert cl (h i) | otherwise = h k \end{code} History updating with a list of instances. \begin{code} updateHIST :: History -> [(Int,Cl)] -> History updateHIST = foldl update \end{code} Another auxiliary function we need is \verb^distrib^, to distribute a list of positive clauses (a list of lists of positive literals). E.g., \verb^distrib [[tP[a],tP[b]],[tQ[a],tQ[b]]]^ should yield \verb^[[tP[a],tQ[a]],[tP[a],tQ[b]][tP[b],tQ[a]][tP[b],tQ[b]]]^. The idea is to convert a conjunction of disjunctions into an equivalent disjunction of conjunctions. Cf.\ the code for \verb^disjList^ above. We define \verb^distrib^ as a general list function. \begin{code} distrib :: [[a]] -> [[a]] distrib [] = [] distrib [xs]= [ [x] | x <- xs ] distrib (xs:yss) = [ (x:ys) | x <- xs, ys <- distrib yss ] \end{code} Examples: \begin{verbatim} FHT_TAP> distrib [[1,2],[3,4],[5,6]] [[1,3,5],[1,3,6],[1,4,5],[1,4,6],[2,3,5],[2,3,6],[2,4,5],[2,4,6]] FHT_TAP> distrib [[1,2],[3,4],[5,6,7]] [[1,3,5],[1,3,6],[1,3,7],[1,4,5],[1,4,6],[1,4,7],[2,3,5],[2,3,6], [2,3,7],[2,4,5],[2,4,6],[2,4,7]] FHT_TAP> distrib [[tP[a],tP[b]],[tP[x],tP[y]]] [[T ("P",0) [Struct ("a",1) []],T ("P",0) [Var ("x",0)]], [T ("P",0) [Struct ("a",1) []],T ("P",0) [Var ("y",0)]], [T ("P",0) [Struct ("b",1) []],T ("P",0) [Var ("x",0)]], [T ("P",0) [Struct ("b",1) []],T ("P",0) [Var ("y",0)]]] \end{verbatim} \section{Refutation} The function \verb^refute^ takes a clause table, a tableau branch, and a renaming index, and returns a stream of substitutions that refute the branch for the clause table. If the branch is unsatisfiable for the clause table, the returned stream is non-empty, and every substitution in it yields a refutation of a tableau development of the branch, for the clause table. For a branch that is satisfiable for the given clause table, the function may loop or return the empty list. We can't do better than that.\footnote{In fact, no-one can devise a program that decides FOL theoremhood, as Church and Turing discovered in the 1930s. Still, it is worthwhile to try and avoid refutation loops for particular formulas as much as possible.} Refutation is an attempt to close the current branch by means of processing of pending calls. If there are no calls left to be processed, the branch remains open. \begin{code} refute :: Table -> Branch -> Index -> [Subst] refute table ([],h,lits) k = [] \end{code} If a call (positive literal) is pending, look up its matches in the database table, and call \verb^refute'^. The matches in the database table are renamed starting from the index $k$ of \verb^refute^, so this index has to be incremented with the number of matches found. \begin{code} refute table ((p:pending), h, lits) k = refute' table matches (pending, h, lits) (k+l) where matches = match table h p lits k l = toInteger (length matches) \end{code} The function \verb^peekRefute^ is a wrapper for \verb^refute'^ that shows the substitutions. \begin{verbatim} peekRefute :: Table -> [Match] -> Branch -> Index -> [Subst] peekRefute table m (pending,h,lits) index = trace (showSubs constraints) (refute' table m (pending,h,lits) index) \end{verbatim} The function \verb^refute'^ carries out the work of \verb^refute^ for a given list of matches of a positive literal. \begin{code} refute' :: Table -> [Match] -> Branch -> Index -> [Subst] \end{code} Use the all negative matches to generate closing substitutions, and the other matches to extend the tableau branch. \begin{code} refute' table matches (pending,h,lits) k = if poslist == [] then [ rho | (j, rho, ([],neg)) <- matches ] ++ refute table (pending,h,lits) k else [ rho | (j, rho, ([],neg)) <- matches ] ++ mergeLst [ refute table (pending ++ newpos,newhist,newlits) k | newpos <- distrib poslist, newlits <- [fuseLists newpos lits] ] where instances = [(j,inst) | (j,rho,inst) <- matches ] newhist = updateHIST h instances poslist = [ pos | (j, rho, (pos,neg)) <- matches, pos /= [] ] \end{code} Notice that it is important for fairness that the new pending positive literals are appended to the list of pending literals. Replacement of \verb^pending ++ newpos^ by \verb^fuseLists newpos pending^ will result in an incomplete proof procedure. Wrap up the \verb^refute^ function in a function \verb^refuteIt^ that takes a list of clauses and returns a list of closing substitutions for the clause list. Set the renaming level to $1$, for the clause table uses index $0$ and the branches are initialized with positive literals with level-$0$ variables. \begin{code} refuteIt :: [Cl] -> [Subst] refuteIt cls = mergeLst [ refute table branch 1 | branch <- branches ] where branches = initialize cls table = makeTable cls \end{code} \section{Theorem Proving and Satisfiability Checking} A FOL theorem is a formula $F$ such that $\neg F$ can be refuted. Successful refutation is indicated by a non-empty substitution list returned by \verb^refute^. Note that \verb^thm^ may loop for non-theorems. \begin{code} thm :: Form -> Bool thm f = (refuteIt (clause (Neg f))) /= [] \end{code} A formula for which the refutation attempt fails is satisfiable. Failure of refutation is indicated by the empty substitution list returned by \verb^refute^. Note that \verb^sat^ may loop for satisfiable formulas. \begin{code} sat :: Form -> Bool sat f = (refuteIt (clause f)) == [] \end{code} \section{Examples} \paragraph{Propositional reasoning} \mbox{} \begin{code} true = Conj [] false = Disj [] pIMPLq = Disj [(Neg (p [])),(q [])] qIMPLr = Disj [(Neg (q [])),(r [])] pIMPLr = Disj [(Neg (p [])),(r [])] taut = Disj [Neg pIMPLq, Neg qIMPLr, pIMPLr] taut' = Disj [Neg pIMPLq, Neg (p []), q []] \end{code} {\em FHT\_TAP}\/ gives: \begin{verbatim} FHT_TAP> thm taut True \end{verbatim} \paragraph{Aristotelian Syllogisms} \mbox{} \begin{code} allPQ = Forall xi (Disj [(Neg (p [x])),(q [x])]) allQR = Forall xi (Disj [(Neg (q [x])),(r [x])]) allPR = Forall xi (Disj [(Neg (p [x])),(r [x])]) barbara = Disj [(Neg allPQ),(Neg allQR),allPR] \end{code} {\em FHT\_TAP}\/ gives: \begin{verbatim} FHT_TAP> thm barbara True \end{verbatim} {\em FHT\_TAP}\/ decides this syllogism. An attempt to prove the negation of {\em Barbara}\/ yields the following: \begin{verbatim} FHT_TAP> thm (Neg barbara) False \end{verbatim} In fact, the initialisation phase already makes clear that \verb^Neg barbara^ cannot be a theorem: \begin{verbatim} FHT_TAP> initialize (clause barbara) [([],<>,[],[[]])] FHT_TAP> \end{verbatim} Here is another example of a syllogism: \begin{code} someQ = Exists xi (q [x]) syllog2 = Disj [Neg allPQ, Neg (p[a]), someQ] \end{code} {\em FHT\_TAP}\/ gives: \begin{verbatim} FHT_TAP> thm syllog2 True \end{verbatim} The following example has a slight twist: \begin{code} allP = Forall xi (p[x]) allPQ' = Forall xi (Disj [Neg (p [x]), Neg (p [s[x]]), q [x]]) twist = Disj [Neg allP, Neg allPQ',someQ] \end{code} Here is the clause list for the example: \begin{verbatim} FHT_TAP> clause (Neg twist) [([T ("P",0) [Var ("X0",0)]],[]), ([T ("Q",0) [Var ("X1",0)]], [F ("P",0) [Var ("X1",0)],F ("P",0) [Struct ("s",1) [Var ("X1",0)]]]), ([],[F ("Q",0) [Var ("X2",0)]])] \end{verbatim} The table for \verb^Neg twist^ shows that the positive clause \verb^T ("P",0) [Var ("X0",0)]^ has two different matches: \begin{verbatim} FHT_TAP> makeTable (clause (Neg twist)) [(1,F ("P",0) [Var ("X1",0)], ([T ("Q",0) [Var ("X1",0)]], [F ("P",0) [Var ("X1",0)], F ("P",0) [Struct ("s",1) [Var ("X1",0)]]])), (1,F ("P",0) [Struct ("s",1) [Var ("X1",0)]], ([T ("Q",0) [Var ("X1",0)]], [F ("P",0) [Var ("X1",0)], F ("P",0) [Struct ("s",1) [Var ("X1",0)]]])), (2,F ("Q",0) [Var ("X2",0)], ([],[F ("Q",0) [Var ("X2",0)]]))] FHT_TAP> \end{verbatim} \begin{verbatim} FHT_TAP> thm twist True \end{verbatim} \paragraph{The AI puzzle again} \begin{code} greenA = p [a] greenC = p [c] greenX = p [x] greenY = p [y] onAB = r [a,b] onBC = r [b,c] onXY = r [x,y] puzzle = Disj [Neg greenA, greenC, Neg onAB, Neg onBC, Exists xi (Exists yi (Conj [greenX,(Neg greenY),onXY]))] puzzle' = Disj [Neg greenA, greenC, Neg onAB, Neg onBC, Exists xi (Exists yi (onXY))] \end{code} {\em FHT\_TAP}\/ proves that this is a theorem: \begin{verbatim} FHT_TAP> thm puzzle True \end{verbatim} {\em FHT\_TAP}\/ is also able to prove that \verb^Neg puzzle^ is {\em not}\/ a theorem. \begin{verbatim} FHT_TAP> thm (Neg puzzle) False \end{verbatim} \paragraph{Baby Arithmetic} Some properties of the natural numbers with $s$ and $\leq$. Zero is a natural number. If $x$ is a natural number, then $s(x)$ is a natural number as well. \begin{code} nat1 = p [zero] nat2 = Forall xi (Disj [Neg (p [x]), (p [s[x]])]) \end{code} $\forall x \in \Nat (x \leq 0)$, $\forall x \forall y (x \leq y \rightarrow s(x) \leq s(y))$. \begin{code} leq1 = Forall xi (Disj [Neg (p [x]), (r [zero,x])]) leq2 = Forall xi (Forall yi (Disj [Neg (r [x,y]),(r [s[x],s[y]])])) \end{code} Two baby theorems: \begin{code} arith1 = Disj [(Neg nat1),(Neg nat2), p[five]] arith2 = Disj [(Neg nat1),(Neg nat2),(Neg leq1),(Neg leq2),(r [two,five])] \end{code} {\em FHT\_TAP}\/ has no difficulty with baby arithmetic: \begin{verbatim} FHT_TAP> thm arith1 True FHT_TAP> thm arith2 True FHT_TAP> thm (Neg arith1) False FHT_TAP> thm (Neg arith2) False FHT_TAP> \end{verbatim} \paragraph{Reasoning about Relations} Some properties of relations in FOL: \begin{code} refl = Forall xi (r [x,x]) irrefl = Forall xi (Neg (r [x,x])) trans = Forall xi (Forall yi (Forall zi (Disj [Neg (r [x,y]),Neg (r [y,z]),r [x,z]]))) ctrans = Forall xi (Forall yi (Forall zi (Disj [r [x,y], r [y,z],Neg (r [x,z])]))) symm = Forall xi (Forall yi (Disj [Neg (r [x,y]), r [y,x]])) asymm = Forall xi (Forall yi (Disj [Neg (r [x,y]), Neg (r [y,x])])) serial = Forall xi (Exists yi (r [x,y])) \end{code} Every asymmetric relation is irreflexive: \begin{code} relprop1 = Disj [(Neg asymm),irrefl] \end{code} Every transitive and irreflexive relation is asymmetric: \begin{code} relprop2 = Disj [(Neg trans),(Neg irrefl),asymm] \end{code} Every transitive, symmetric and serial relation is reflexive: \begin{code} relprop3 = Disj [(Neg trans),(Neg symm),(Neg serial),refl] pos = [T ("R",0) [Var ("X5",0),Struct ("sk",0) [Var ("X5",0)]], T ("R",0) [Struct ("sk",0) [Var ("X5",0)],Var ("X5",0)]] neg = [F ("R",0) [Var ("X0",0),Var ("X1",0)], F ("R",0) [Var ("X1",0),Var ("X2",0)]] pos' = [T ("R",0) [Var ("X5",0),Struct ("sk",0) [Var ("X5",0)]], T ("R",0) [Struct ("sk",0) [Var ("X5",0)],Var ("X5",0)]] neg' = [F ("R",0) [Var ("X2",0),Var ("X5",0)], F ("R",0) [Var ("X1",0),Var ("X2",0)]] \end{code} We get: \begin{verbatim} FHT_TAP> thm relprop1 True (1236 reductions, 2885 cells) FHT_TAP> thm relprop2 True (11367 reductions, 23975 cells) FHT_TAP> thm relprop3 True (24249 reductions, 48876 cells) FHT_TAP> thm (Neg relprop1) False (153 reductions, 630 cells) FHT_TAP> thm (Neg relprop2) False (619 reductions, 2076 cells) FHT_TAP> thm (Neg relprop3) False (667 reductions, 2186 cells) FHT_TAP> \end{verbatim} % BUG: thm relprop3 loops Some examples that are satisfiable. Note that \verb^relprop7^ only has infinite models. \begin{code} relprop4 = Conj [ctrans,refl] relprop5 = Conj [trans,irrefl] relprop6 = Conj [trans,irrefl,serial] relprop7 = Conj [trans,irrefl,serial,asymm] relprop8 = Conj [trans,refl] \end{code} % BUG ??: sat relprop6 loops % BUG ??: sat relprop7 loops \begin{code} c7 = clause relprop7 tbl = makeTable c7 \end{code} Balder's example: \begin{code} balder = Conj [allP,Disj [Neg (p[a]),Neg (p[b])]] \end{code} We get: \begin{verbatim} FHT_TAP> sat balder False FHT_TAP> refuteIt (clause balder) [[(("X0",1),Struct ("a",1) []),(("X0",0),Struct ("b",1) [])], [(("X0",1),Struct ("b",1) []),(("X0",0),Struct ("a",1) [])]] FHT_TAP> \end{verbatim} A variant on Balder's example: \begin{code} balder' = Conj [allP,Disj [Neg (p[a]),Neg (p[b]),Neg (p[c])]] \end{code} This gives: \begin{verbatim} FHT_TAP> refuteIt (clause balder') [[(("X0",1),Struct ("a",1) []), (("X0",0),Struct ("b",1) []), (("X0'",0),Struct ("c",1) [])], [(("X0",1),Struct ("b",1) []), (("X0",0),Struct ("a",1) []), (("X0'",0),Struct ("c",1) [])], [(("X0",1),Struct ("c",1) []), (("X0",0),Struct ("a",1) []), (("X0'",0),Struct ("b",1) [])]] FHT_TAP> \end{verbatim} \section{Further Work} \begin{itemize} \item Write out the completeness proof for Free Hyper Tableau reasoning. \item Prove results about subclasses of FOL that are decided by Free Hyper Tableau reasoning. \item Add Rules for the handling of equality. \item Implement a Lazy (Disjunctive) Prolog. \item Implement a Lazy Dynamo \cite{EijHegNua:trap}. \end{itemize} \paragraph{Acknowledgement} Many thanks to the {\em Dynamo}\/ team for inspiration. } \bibliographystyle{acm} %\bibliography{/home/jve/texmacros/mybibentries} \bibliography{/ufs/jve/texmacros/mybibentries} \end{document}