\documentclass[11pt]{article}
\usepackage{latexsym,amssymb,amsmath,theorem,proof,calc,alltt}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                  % 
%  NEW VERSION, March 2001         %
%                                  %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\input{mymacros}

\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{{\em LazyTAP} -- A Lazy Tableau Theorem Prover for FOL}

\author{Jan van Eijck \\
\small\em CWI and ILLC, Amsterdam, Uil-OTS, Utrecht}

\date{First Draft --- December 2000}

\begin{document}

\maketitle 

\begin{abstract} \noindent 
  First go at a Haskell implementation of tableau theorem 
  proving for FOL, using lazy lists of 
  instantiating substitutions for the free tableau variables
  instead of bracktracking. 
\end{abstract}

\paragraph{Keywords:} Tableau theorem proving, Instance Streams, leanTAP, 
Proof Search without Backtracking. 

\paragraph{MSC codes:} \ldots 


\section{Introduction} 

This paper works out a suggestion from Giese \cite{Giese:pswbui} to 
do tableau proof search by merging closing substitutions for tableau 
branches into a closing substitution for the whole tableau. 
The paper contains the complete Haskell \cite{Haskell98:rep} code of
a lazy tableau theorem prover for FOL. The boxed text constitutes the
Haskell program. Instead of doing proof search by backtracking and
iterative deepening, {\em LazyTAP}\/ generates 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.

Use of substitution instances to guide proof search in tableau theorem
proving is in the air: see Baumgartner \cite{Baumgartner:FDPLL} and 
Beckert \cite{Beckert:dfpswb} for background.

\section{Indices, Terms, Formulas} 

As variable identifiers we use indexed strings, i.e., pairs 
of strings and indices. Function terms have the form 
\verb^Struct Id [t1,...,tn]^. Function terms of the form 
\verb^Struct Id []^ are individual constants. 

\begin{code}
module LazyTAP where 

import List

type Name     = String
type Index    = Integer
type Id       = (Name,Index) 
data Term     = Var Id | Struct Id [Term] deriving (Eq,Show)

data Form =  Atom Id [Term]
           | Eq Term Term
           | Neg Form
           | Conj [Form]
           | Disj [Form] 
           | Forall Id Form 
           | Exists Id Form
     deriving (Eq,Show)
\end{code} 
  
Equality is in the language, but we don't handle it yet in the tableau
rules. An empty disjunction \verb^Disj []^ is always false, so this
formula plays the part of $\bot$. Similarly, \verb^Conj []^ does duty
as $\top$.

\section{Variables in Terms, Free Variables in Formulas} 

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} 

The free variables in a formula or a formula list. 

\begin{code}
fvarsInForm :: Form -> [Id] 
fvarsInForm (Atom a ts)     = varsInTerms ts
fvarsInForm (Neg form)      = fvarsInForm form
fvarsInForm (Conj forms)    = fvarsInForms forms
fvarsInForm (Disj forms)    = fvarsInForms forms
fvarsInForm (Forall v form) = filter (/= v) (fvarsInForm form) 
fvarsInForm (Exists v form) = filter (/= v) (fvarsInForm form) 

fvarsInForms :: [Form] -> [Id]
fvarsInForms = (nub . concat . map fvarsInForm)
\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 of a substitution. 

\begin{code}
dom :: Subst -> [Id]
dom = map fst
\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.  The following function ensures
that this list remains ordered and without duplicates as it is built.

\begin{code}
insrt :: Ord a => a -> [a] -> [a]
insrt i []                 = [i]
insrt i (j:js) | i < j     = (i:j:js)
                | i == j    = (j:js)
                | otherwise = (j:(insrt i js))
\end{code}
  
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{Negation Normal Forms, with Skolemization}

Negation normal formulas have negation signs only in front of atoms.
The function \verb^nnf^ calls an auxiliary function \verb^nnf'^ that
memoizes an identifier list (for the indices of outscoping universal
quantifiers) and an index (for use in the next skolem term to be
built).

\begin{code}
nnf :: Form -> Form 
nnf f = nnf' f [] 0
\end{code}
  
The function \verb^nnf'^ is called as \verb^nnf' f ixs sk^.  The
parameter \verb^ixs^ for the list of universal indices is updated in
the calls for universal formulas, while the parameter \verb^sk^, the 
index for the next skolem term, is incremented in the calls for
existential formulas.

\begin{code}
nnf' :: Form -> [Id] -> Index -> Form
nnf' (Atom n ts) ixs sk = (Atom n ts)
nnf' (Conj fs) ixs sk = Conj (map (\ f -> nnf' f ixs sk) fs) 
nnf' (Disj fs) ixs sk = Disj (map (\ f -> nnf' f ixs sk) fs) 
nnf' (Forall x f) ixs sk = Forall x (nnf' f (insrt x ixs) sk)
nnf' (Exists x f) ixs sk = nnf' (appF b f) ixs (sk+1)
      where b = [(x,(skolem ixs sk))]
nnf' (Neg (Atom n ts)) ixs sk = Neg (Atom n ts)
nnf' (Neg (Conj fs)) ixs sk = Disj (map (\ f -> nnf' (Neg f) ixs sk) fs) 
nnf' (Neg (Disj fs)) ixs sk = Conj (map (\ f -> nnf' (Neg f) ixs sk) fs) 
nnf' (Neg (Forall x f)) ixs sk = nnf' (appF b (Neg f)) ixs (sk+1) 
      where b = [(x,(skolem ixs sk))]
nnf' (Neg (Exists x f)) ixs sk = Forall x (nnf' (Neg f) (insrt x ixs) sk)
nnf' (Neg (Neg f)) ixs sk = nnf' f ixs sk 
\end{code} 

\section{Unification} 

Unification of atoms 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.
 
\begin{code}
unifyAtoms :: Form -> Form -> [Subst]
unifyAtoms (Atom a ts) (Atom b rs) = 
             unify (Struct a ts) (Struct b rs)
\end{code}
  
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}
unify :: Term -> Term -> [Subst]
unify (Var x)       (Var y)       =
      if x==y then [epsilon] else [[(x,Var y)]]
unify (Var x)       t2            = 
      [ [(x,t2)] | x `notElem` varsInTerm t2 ]
unify t1            (Var y)       = 
      [ [(y,t1)] | y `notElem` varsInTerm t1 ]
unify (Struct a ts) (Struct b rs) = 
      [ u | a==b, u <- listUnify ts rs ]
\end{code}

Unification of lists of terms: 
\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}
listUnify :: [Term] -> [Term] -> [Subst]
listUnify []     []     = [epsilon]
listUnify []     (r:rs) = []
listUnify (t:ts) []     = []
listUnify (t:ts) (r:rs) = 
   [ (compose sigma2 sigma1) | sigma1 <- unify t r,
                               sigma2 <- listUnify (appTs sigma1 ts) 
                                                   (appTs sigma1 rs) ]
\end{code}

\section{Merging of Substitutions} 

The merge 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^meet^ constructs a representation of $\theta_1 \sqcap
\theta_2$, the meet 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}
meet :: Subst -> Subst -> [Subst]
meet [] ys = [ys]
meet ((x,x'):xs) ys =
      [ subst | mgu   <- unify x' y', 
                subst <- meet (compose mgu xs) (compose mgu ys) ]
      where y' = appI ys x 
\end{code}

To see that the equation for \verb^meet ((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} 
Note that the function \verb^meet^ might have been called 
\verb^substitutionUnify^.
  
\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) = (meet x y) ++ 
    alt3 (mergePair x ys) (mergePair y xs) (merge xs ys) 

mergePair :: Subst -> [Subst] -> [Subst]
mergePair x [] = []
mergePair x (y:ys) = (meet 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 meets $\sqcap \{ \theta_1, \ldots, \theta_n \}$, where
$\theta_i$ is a substitution from the $i$-th stream. Since the meet
$\sqcap \emptyset$ is the identity substitution $\epsilon$, the
function call \verb^mergeLst []^ should return \verb^[epsilon]^.

\begin{code}
mergeLst :: [[Subst]] -> [Subst] 
mergeLst [] = [epsilon]
mergeLst [bs1] = bs1
mergeLst (bs1:bs2:streams) = mergeLst ((merge bs1 bs2):streams)
\end{code}

\section{Refutation} 

The function \verb^refute^ takes a list of formulas in negation normal
form and returns a stream of substitutions for the free variables
occurring in the formula list for which the list can be refuted. If
the formula list is unsatisfiable, the returned stream is non-empty,
and every substitution it contains yields a refutation of a tableau
development of the original list. For a satisfiable formula list, 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. In this respect, {\em LazyTAP}\/
  offers scope for further improvement.}

For finding the substitutions for all pairs of literals, we have to 
remember the literals pairs for which the substitutions were already computed. 
The function \verb^refute^ calls \verb^refuteMem^, a function 
that memoizes the literals pairs that already spawned a substitution
on the branch. These are kept in two lists, one for the positives, 
one for the negatives.  A third parameter is used for memoizing 
the next fresh universal index. 

\begin{code}
refute :: [Form] -> [Subst]
refute forms = refuteMem forms [] [] 0 
\end{code}
  
Function \verb^refuteMem^ takes a list of formulas (the current
branch) plus three further arguments \verb^pos^, \verb^neg^ and
\verb^i^.  Argument \verb^pos^ stores the list of positive literals
encountered so far along the branch, argument \verb^neg^ stores the
list of negative literals encountered so far along the branch. The
understanding is that all substitutions resulting from matching pairs
between \verb^pos^ and \verb^neg^ have already been spawned in the
stream.  The argument \verb^i^ stores the index for the next
available fresh universal parameter.

The function \verb^refuteMem^ returns a stream of substitutions, all 
of which represent a different way of closing the branch. 

\begin{code}
refuteMem :: [Form] -> [Form] -> [Form] -> Integer -> [Subst]
\end{code}

If there are no formulas left, there are no more ways of closing the branch, 
so in this case the stream of refuting substitutions dries up. 

\begin{code}
refuteMem [] _ _ _ = []
\end{code}

Conjunction: apply the $\alpha$ rule, so carry on with all the $\alpha_i$ 
added to the formula list. 

\begin{code}
refuteMem ((Conj conjuncts):forms) pos neg i = 
      refuteMem (conjuncts ++ forms) pos neg i  
\end{code}

Disjunction: apply the $\beta$ rule, carry on with a new stream for
each of the $\beta_i$ added to the formula list, and merge the
resulting substitution streams into a single stream again. Note that 
\verb^refuteMem (Disj []:_) _ _ _^ results in a call to 
\verb^mergeLst []^, which returns \verb^[epsilon]^. This closes 
the current branch without further ado (i.e., without constraining 
the substitutions for other branches). 

\begin{code}
refuteMem ((Disj disjuncts):forms) pos neg i = 
      mergeLst [ refuteMem (f:forms) pos neg i | f <- disjuncts ]
\end{code}

Universal quantification: apply the $\gamma$ rule, and carry on with 
both $\gamma_1$ and $\gamma$ added to the formula list to ensure fairness. 
To postpone the next application of the rule to the same formula as long 
as possible, the $\gamma$ formula is moved to the end of the list. 

\begin{code}
refuteMem ((Forall v form):forms) pos neg i  = 
   refuteMem (((appF [(v, new)] form):forms) 
                ++ [Forall v form]) pos neg (j+1) 
   where new = (Var ("X", j))
         j = find i (v:(fvarsInForms (form:forms)))
         find j ids | ("X",j) `elem` ids = find (j+1) ids
                    | otherwise          = j 
\end{code}

Positive atom: Spawn all possible substitutions resulting from unification
attempts against the negative literals collected so far. These
represent all the different ways of closing the branch, using this
literal against the negative literals encountered so far along the
branch. Carry on with the atom added to the list of positive literals.

\begin{code}
refuteMem (atom1@(Atom n ts):forms) pos neg i = 
   if atom1 `elem` pos 
   then 
     refuteMem forms pos neg i 
   else 
     [ b | atom2 <- neg, b <- unifyAtoms atom1 atom2 ] 
      ++
     refuteMem forms (atom1:pos) neg i 
\end{code}

Negated atom: Spawn all possible substitutions resulting from unification
attempts against the positive literals collected so far. These
represent all the different ways of closing the branch, using this
literal against the positive literals encountered so far along the
branch. Carry on with the atom added to the list of negative literals.

\begin{code}
refuteMem ((Neg atom1@(Atom n ts)):forms) pos neg i  = 
   if atom1 `elem` neg 
   then 
     refuteMem forms pos neg i 
   else  
     [ b | atom2 <- pos, b <- unifyAtoms atom1 atom2 ]
      ++ 
     refuteMem forms pos (atom1:neg) i 
\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 = (refute [(nnf (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 = (refute [nnf f]) == [] 
\end{code}

\section{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)
\end{code}

\paragraph{Propositional reasoning} \mbox{}

\begin{code}
pIMPLq = Disj [(Neg (p [])),(q [])]
qIMPLr = Disj [(Neg (q [])),(r [])]
pIMPLr = Disj [(Neg (p [])),(r [])]
taut = Disj [(Neg pIMPLq),(Neg qIMPLr),pIMPLr]
\end{code}

{\em LazyTAP}\/ gives: 
\begin{verbatim}
LazyTAP> thm taut
True
LazyTAP> :set +s
LazyTAP> thm taut
True
(476 reductions, 1136 cells)
LazyTAP> 
\end{verbatim}

\paragraph{An Aristotelian syllogism} \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 LazyTAP}\/ gives: 
\begin{verbatim}
LazyTAP> thm barbara
True
(1656 reductions, 3338 cells)
LazyTAP> 
\end{verbatim}

Lazy tableau theorem proving is not the way to go for finding finite
counterexamples. If a universal quantifier is present in a consistent
formula list, the tableau development for that list goes on forever,
for no substitution will close all branches, while the $\gamma$ rule keeps
getting applied.  An attempt to prove the negation of {\em Barbara},
e.g., gets into a loop:
\begin{verbatim}
LazyTAP> thm (Neg barbara)
{Interrupted!}

(661478 reductions, 1392416 cells, 5 garbage collections)
LazyTAP>
\end{verbatim}

\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. Note that this puzzle is not in the Horn fragment of FOL;
in fact, it cannot be solved by a Prolog program.

\begin{code} 
greenA = p [a]
greenC = p [c]
onAB = r [a,b]
onBC = r [b,c]
puzzle = Disj [Neg greenA, greenC, Neg onAB, Neg onBC,
                Exists xi (Exists yi (r [x,y]))]
\end{code}

{\em LazyTAP}\/ proves that this is a theorem: 

\begin{verbatim}
LazyTAP> thm puzzle
True
(783 reductions, 1604 cells)
LazyTAP> 
\end{verbatim}

An attempt to refute \verb^nnf (Neg puzzle)^ yields an infinite stream of
substitutions that all close the infinite tableau.  The tableau is
infinite because the $\gamma$ rule keeps getting applied. 
Here are the first two closing substitutions: 
\begin{verbatim} 
LazyTAP> take 2 (refute [nnf (Neg puzzle)])
[[(("X",0),Struct ("b",1) []),(("X",1),Struct ("c",1) [])],
[(("X",0),Struct ("a",1) []),(("X",1),Struct ("b",1) [])]]
\end{verbatim} 
All further members of the stream are identical to the above 
modulo renaming: 
\begin{verbatim}
LazyTAP> take 20 (refute [nnf (Neg puzzle)])
[[(("X",0),Struct ("b",1) []),(("X",1),Struct ("c",1) [])],
[(("X",0),Struct ("a",1) []),(("X",1),Struct ("b",1) [])],
[(("X",2),Struct ("b",1) []),(("X",3),Struct ("c",1) [])],
[(("X",2),Struct ("a",1) []),(("X",3),Struct ("b",1) [])],
[(("X",0),Struct ("b",1) []),(("X",4),Struct ("c",1) [])],
[(("X",0),Struct ("a",1) []),(("X",4),Struct ("b",1) [])],
[(("X",5),Struct ("b",1) []),(("X",6),Struct ("c",1) [])],
[(("X",5),Struct ("a",1) []),(("X",6),Struct ("b",1) [])],
[(("X",2),Struct ("b",1) []),(("X",7),Struct ("c",1) [])],
[(("X",2),Struct ("a",1) []),(("X",7),Struct ("b",1) [])],
[(("X",0),Struct ("b",1) []),(("X",8),Struct ("c",1) [])],
[(("X",0),Struct ("a",1) []),(("X",8),Struct ("b",1) [])],
[(("X",9),Struct ("b",1) []),(("X",10),Struct ("c",1) [])],
[(("X",9),Struct ("a",1) []),(("X",10),Struct ("b",1) [])],
[(("X",5),Struct ("b",1) []),(("X",11),Struct ("c",1) [])],
[(("X",5),Struct ("a",1) []),(("X",11),Struct ("b",1) [])],
[(("X",2),Struct ("b",1) []),(("X",12),Struct ("c",1) [])],
[(("X",2),Struct ("a",1) []),(("X",12),Struct ("b",1) [])],
[(("X",0),Struct ("b",1) []),(("X",13),Struct ("c",1) [])],
[(("X",0),Struct ("a",1) []),(("X",13),Struct ("b",1) [])]]
LazyTAP> 
\end{verbatim}

In this particular case, {\em LazyTAP}\/ is also able to prove that 
\verb^(Neg puzzle)^ is {\em not}\/ a theorem. 
\begin{verbatim}
LazyTAP> thm (Neg puzzle)
False
(65 reductions, 212 cells)
LazyTAP> 
\end{verbatim}
In this particular case the refutation attempt of the theorem 
\verb^Neg puzzle^ does not get into a loop for a trivial reason. 
As it happens, \verb^puzzle^, the formula that 
{\em LazyTAP}\/ attempts to refute, contains no universal quantifiers:
\begin{verbatim} 
LazyTAP> nnf puzzle
Disj [Neg (Atom ("P",0) [Struct ("a",1) []]),Atom ("P",0) [Struct ("c",1) []],
Neg (Atom ("R",0) [Struct ("a",1) [],Struct ("b",1) []]),Neg (Atom ("R",0) 
[Struct ("b",1) [],Struct ("c",1) []]),Atom ("R",0) [Struct ("sk",0) [],
Struct ("sk",1) []]]
LazyTAP> 
\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 LazyTAP}\/ is not very quick at baby arithmetic \ldots 

\begin{verbatim}
LazyTAP> thm arith1
True
(33448 reductions, 63828 cells)
LazyTAP> thm arith2
True
(16045689 reductions, 29788277 cells, 258 garbage collections)
LazyTAP> 
\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])])))
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]
\end{code}


We get: 

\begin{verbatim} 
LazyTAP> thm relprop1
True
(1581 reductions, 2904 cells)
LazyTAP> thm relprop2
True
(8604 reductions, 14112 cells)
LazyTAP> thm relprop3
True
(73088 reductions, 127304 cells)
LazyTAP> 
\end{verbatim} 

\section{Further Work} 

\begin{itemize} 
\item Add Rules for Equality Reasoning. 
\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}