\documentstyle[makeidx]{article}
\makeindex
%\setlength{\oddsidemargin}{.5in}
%\setlength{\evensidemargin}{.5in}
%\setlength{\textwidth}{5.8in}
\begin{document}
%\setlength{\parindent}{0pt}
%\newcounter{bean}
%\begin{list}{\arabic{bean}.}{\usecounter{bean}\setlength{\leftmargin}{0pt}\setlength{\rightmargin}{0pt}\setlength{\listparindent}{20pt}\setlength{\parsep}{5pt}}
%\item[]

\begin{verbatim};;;; proof of completeness of ground resolution

;;;; Matt Wilding  April 1988 

;;;; This proof script executes on Matt Kaufmann's interactive enhancement 
;;;; to the Boyer-Moore system

;; This proof script is a proof of the completeness of ground resolution
;; using Bledsoe's excess literal technique.  The final theorem is:

;;	     (implies
;;	      (and
;;	       (unsatisfiable x)
;;	       (validclauses x))
;;	      (finishedproof x (getproof x)))

;; The proof script is in several sections:

;; 1) definitions required for understanding the theorem
;; 2) definition of getproof (a function that is conjectured to return a valid
;;      resolution proof that ends in box)
;; 3) proof of theorem

;; Section 1 is, strictly speaking, the only section needed to understand what has
;; been proven.  

\end{verbatim}
\noindent{\sc Event}:   Start with the initial {\bf nqthm} theory.

\addvspace{18pt} \begin{verbatim};; added by Matt Kaufmann just to make nqthm-1991 happy!





;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 1: definitions of terms in theorem

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{subset} \\  
\=\+{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{car}}\,({\it{x\/}}) $\in$ {\it{y\/}}$\;\;${\bf then }{\rm{subset}}\,({\rm{cdr}}\,({\it{x\/}}), {\it{y\/}})\index{subset} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{set-equal} \\  
{\rm{set-equal}}\,({\it{s1\/}}, {\it{s2\/}})\index{set-equal} $=$ ({\rm{subset}}\,({\it{s1\/}}, {\it{s2\/}})\index{subset} $\wedge$ {\rm{subset}}\,({\it{s2\/}}, {\it{s1\/}})\index{subset})
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{set-member} \\  
\=\+{\rm{set-member}}\,({\it{x\/}}, {\it{list\/}})\index{set-member} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{set-equal}}\,({\it{x\/}}, {\rm{car}}\,({\it{list\/}}))\index{set-equal}$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{set-member}}\,({\it{x\/}}, {\rm{cdr}}\,({\it{list\/}}))\index{set-member}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim};;  define what it means to be a valid set of clauses
;;  (ex.  (validclauses '((a b) ((not a) (not b)) ((not a) b) (a (not b)))) = t)

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{validliteral} \\  
\=\+{\rm{validliteral}}\,({\it{l\/}})\index{validliteral} \\ 
$=$$\;\;\;\;$(\=\+({\rm{litatom}}\,({\it{l\/}}) $\wedge$ ({\it{l\/}} $\not=$ {\bf{nil}})) \\ 
$\vee$$\;\;\;\;$(\=\+{\rm{listp}}\,({\it{l\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{l\/}}) $=$ {\tt{'}}{\tt{not}}) \\ 
$\wedge$$\;\;\;\;${\rm{litatom}}\,({\rm{cadr}}\,({\it{l\/}})) \\ 
$\wedge$$\;\;\;\;$({\rm{cadr}}\,({\it{l\/}}) $\not=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;$({\rm{cddr}}\,({\it{l\/}}) $=$ {\bf{nil}}))\-)\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{validclause} \\  
\=\+{\rm{validclause}}\,({\it{c\/}})\index{validclause} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{c\/}}) \\ 
{\bf then }\=\+{\rm{validclause}}\,({\rm{cdr}}\,({\it{c\/}}))\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validliteral}}\,({\rm{car}}\,({\it{c\/}}))\index{validliteral} \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\it{c\/}}) $\not\in$ {\rm{cdr}}\,({\it{c\/}}))\- \\ 
{\bf else }{\it{c\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{validclauses} \\  
\=\+{\rm{validclauses}}\,({\it{cs\/}})\index{validclauses} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}})$\;\;${\bf then }{\rm{validclause}}\,({\rm{car}}\,({\it{cs\/}}))\index{validclause} $\wedge$ {\rm{validclauses}}\,({\rm{cdr}}\,({\it{cs\/}}))\index{validclauses} \\ 
{\bf else }{\it{cs\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; unsatisfiablility of a set of clauses
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{unsatwith} \\  
\=\+{\rm{unsatwith}}\,({\it{clause\/}}, {\it{cs\/}}, {\it{values\/}})\index{unsatwith} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{clause\/}}) \\ 
{\bf then }\=\+{\bf if }\=\+({\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{car}}\,({\it{clause\/}})) $\in$ {\it{values\/}}) \\ 
$\vee$$\;\;\;\;$({\rm{cadar}}\,({\it{clause\/}}) $\in$ {\it{values\/}})\- \\ 
{\bf then }{\rm{unsatwith}}\,({\rm{cdr}}\,({\it{clause\/}}), {\it{cs\/}}, {\it{values\/}})\index{unsatwith} \\ 
{\bf else }\=\+{\rm{unsatwith}}\,({\rm{cdr}}\,({\it{clause\/}}), {\it{cs\/}}, {\it{values\/}})\index{unsatwith} \\ 
$\wedge$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}}) \\ 
{\bf then }{\rm{unsatwith}}\,(\=\+{\rm{car}}\,({\it{cs\/}}), \\ 
{\rm{cdr}}\,({\it{cs\/}}), \\ 
{\rm{cons}}\,({\rm{car}}\,({\it{clause\/}}), {\it{values\/}}))\-\index{unsatwith} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{unsatisfiable} \\  
\=\+{\rm{unsatisfiable}}\,({\it{cs\/}})\index{unsatisfiable} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}})$\;\;${\bf then }{\rm{unsatwith}}\,({\rm{car}}\,({\it{cs\/}}), {\rm{cdr}}\,({\it{cs\/}}), {\bf{nil}})\index{unsatwith} \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{takeout} \\  
\=\+{\rm{takeout}}\,({\it{list\/}}, {\it{x\/}})\index{takeout} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{car}}\,({\it{list\/}})$\;\;${\bf then }{\rm{takeout}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{x\/}})\index{takeout} \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{list\/}}), {\rm{takeout}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{x\/}})\index{takeout})$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; resolvent is valid resolvent of p1 and p2 resolving on something in p1list
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{resolvent-help} \\  
\=\+{\rm{resolvent-help}}\,({\it{resolvent\/}}, {\it{p1list\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{p1list\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{car}}\,({\it{p1list\/}})) $\in$ {\it{p2\/}} \\ 
{\bf then }\=\+{\rm{subset}}\,(\=\+\=\+{\rm{takeout}}\,({\it{p1\/}}, {\rm{car}}\,({\it{p1list\/}}))\index{takeout} \\ 
$\cup$$\;\;\;\;${\rm{takeout}}\,({\it{p2\/}}, {\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{car}}\,({\it{p1list\/}})))\index{takeout}\-, \\ 
{\it{resolvent\/}})\-\index{subset} \\ 
$\vee$$\;\;\;\;${\rm{resolvent-help}}\,({\it{resolvent\/}}, {\rm{cdr}}\,({\it{p1list\/}}), {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help}\- \\ 
{\bf elseif }{\rm{cadar}}\,({\it{p1list\/}}) $\in$ {\it{p2\/}} \\ 
{\bf then }\=\+{\rm{subset}}\,(\=\+\=\+{\rm{takeout}}\,({\it{p1\/}}, {\rm{car}}\,({\it{p1list\/}}))\index{takeout} \\ 
$\cup$$\;\;\;\;${\rm{takeout}}\,({\it{p2\/}}, {\rm{cadar}}\,({\it{p1list\/}}))\index{takeout}\-, \\ 
{\it{resolvent\/}})\-\index{subset} \\ 
$\vee$$\;\;\;\;${\rm{resolvent-help}}\,({\it{resolvent\/}}, {\rm{cdr}}\,({\it{p1list\/}}), {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help}\- \\ 
{\bf else }{\rm{resolvent-help}}\,({\it{resolvent\/}}, {\rm{cdr}}\,({\it{p1list\/}}), {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{resolvent}$\;\;$
{\rm{resolvent}}\,({\it{r\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent} $=$ {\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help}
\end{tabbing}

\begin{verbatim};; a valid resolution proof for a set of axioms is a set of triples where
;;each line of the proof has a resolvent and two (axiomatic or derived) parents
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{validproof} \\  
\=\+{\rm{validproof}}\,({\it{axioms\/}}, {\it{proof\/}})\index{validproof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{proof\/}}) \\ 
{\bf then }\=\+{\rm{set-member}}\,({\rm{cadar}}\,({\it{proof\/}}), {\it{axioms\/}})\index{set-member} \\ 
$\wedge$$\;\;\;\;${\rm{set-member}}\,({\rm{caddar}}\,({\it{proof\/}}), {\it{axioms\/}})\index{set-member} \\ 
$\wedge$$\;\;\;\;${\rm{resolvent}}\,({\rm{caar}}\,({\it{proof\/}}), {\rm{cadar}}\,({\it{proof\/}}), {\rm{caddar}}\,({\it{proof\/}}))\index{resolvent} \\ 
$\wedge$$\;\;\;\;${\rm{validproof}}\,({\rm{cons}}\,({\rm{caar}}\,({\it{proof\/}}), {\it{axioms\/}}), {\rm{cdr}}\,({\it{proof\/}}))\index{validproof}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; the empty clause is in a set of clauses
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{box-in-axioms} \\  
\=\+{\rm{box-in-axioms}}\,({\it{axioms\/}})\index{box-in-axioms} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{axioms\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{car}}\,({\it{axioms\/}}))$\;\;${\bf then }{\rm{box-in-axioms}}\,({\rm{cdr}}\,({\it{axioms\/}}))\index{box-in-axioms} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{f}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{last-element} \\  
\=\+{\rm{last-element}}\,({\it{list\/}})\index{last-element} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{listp}}\,({\rm{cdr}}\,({\it{list\/}}))$\;\;${\bf then }{\rm{last-element}}\,({\rm{cdr}}\,({\it{list\/}}))\index{last-element} \\ 
{\bf else }{\rm{car}}\,({\it{list\/}})$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{verbatim};; proof is a finished proof of axioms if there are no axioms, if 
;; there are no axioms (and therefore satisfiable), if axioms include box,
;; or if proof is valid and has as its last resolvent box.
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{finishedproof} \\  
\=\+{\rm{finishedproof}}\,({\it{axioms\/}}, {\it{proof\/}})\index{finishedproof} \\ 
$=$$\;\;\;\;$(\=\+($\neg$ {\rm{listp}}\,({\it{axioms\/}})) \\ 
$\vee$$\;\;\;\;${\rm{box-in-axioms}}\,({\it{axioms\/}})\index{box-in-axioms} \\ 
$\vee$$\;\;\;\;$({\rm{validproof}}\,({\it{axioms\/}}, {\it{proof\/}})\index{validproof} $\wedge$ ({\rm{car}}\,({\rm{last-element}}\,({\it{proof\/}})\index{last-element}) $\simeq\;${{\bf{nil}}}${}$)))\-\-
\end{tabbing}










\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 2:  getproof function developement

\end{verbatim}\begin{tabbing}{\sc Definition}:\index{length} \\  
\=\+{\rm{length}}\,({\it{list\/}})\index{length} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}})$\;\;${\bf then }$1\;+$ {\rm{length}}\,({\rm{cdr}}\,({\it{list\/}}))\index{length} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  list-means-length-more-0 \\ \index{list-means-length-more-0}
{\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\tt{0}} $<$ {\rm{length}}\,({\it{x\/}})\index{length})
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{takeout1} \\  
\=\+{\rm{takeout1}}\,({\it{list\/}}, {\it{x\/}})\index{takeout1} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{x\/}} $=$ {\rm{car}}\,({\it{list\/}})$\;\;${\bf then }{\rm{cdr}}\,({\it{list\/}}) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{list\/}}), {\rm{takeout1}}\,({\rm{cdr}}\,({\it{list\/}}), {\it{x\/}})\index{takeout1})$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{listofcars} \\  
\=\+{\rm{listofcars}}\,({\it{list\/}})\index{listofcars} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{list\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{caar}}\,({\it{list\/}}), {\rm{listofcars}}\,({\rm{cdr}}\,({\it{list\/}}))\index{listofcars}) \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim};; some really useful rewrite rules for sets
 
\end{verbatim}\begin{tabbing}{\sc Theorem}:  membership-on-subsets \\ \index{membership-on-subsets}
(({\it{e\/}} $\in$ {\it{a\/}}) $\wedge$ {\rm{subset}}\,({\it{a\/}}, {\it{b\/}})\index{subset}) $\rightarrow$ ({\it{e\/}} $\in$ {\it{b\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  equals-has-same-members \\ \index{equals-has-same-members}
{\rm{set-equal}}\,({\it{a\/}}, {\it{b\/}})\index{set-equal} $\rightarrow$ (({\it{e\/}} $\in$ {\it{a\/}}) $=$ ({\it{e\/}} $\in$ {\it{b\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-is-transitive \\ \index{subset-is-transitive}
({\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\wedge$ {\rm{subset}}\,({\it{y\/}}, {\it{z\/}})\index{subset}) $\rightarrow$ {\rm{subset}}\,({\it{x\/}}, {\it{z\/}})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-fact-1 \\ \index{subset-fact-1}
{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\rightarrow$ {\rm{subset}}\,({\it{x\/}}, {\rm{cons}}\,({\it{a\/}}, {\it{y\/}}))\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-equals-fact \\ \index{set-equals-fact}
{\rm{set-equal}}\,({\it{x\/}}, {\it{y\/}})\index{set-equal} $\rightarrow$ {\rm{set-equal}}\,({\rm{cons}}\,({\it{a\/}}, {\it{x\/}}), {\rm{cons}}\,({\it{a\/}}, {\it{y\/}}))\index{set-equal}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  subset-of-self \\ \index{subset-of-self}
{\rm{subset}}\,({\it{x\/}}, {\it{x\/}})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  set-equal-self \\ \index{set-equal-self}
{\rm{set-equal}}\,({\it{x\/}}, {\it{x\/}})\index{set-equal}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-is-setmember \\ \index{member-is-setmember}
({\it{a\/}} $\in$ {\it{x\/}}) $\rightarrow$ {\rm{set-member}}\,({\it{a\/}}, {\it{x\/}})\index{set-member}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  setmember-is-setmember-of-superset \\ \index{setmember-is-setmember-of-super!set}
({\rm{set-member}}\,({\it{a\/}}, {\it{x\/}})\index{set-member} $\wedge$ {\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset}) $\rightarrow$ {\rm{set-member}}\,({\it{a\/}}, {\it{y\/}})\index{set-member}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  takeout-fact1 \\ \index{takeout-fact1}
{\rm{subset}}\,({\rm{takeout}}\,({\it{s\/}}, {\it{x\/}})\index{takeout}, {\rm{takeout}}\,({\rm{cons}}\,({\it{a\/}}, {\it{s\/}}), {\it{x\/}})\index{takeout})\index{subset}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-of-union-fact-1 \\ \index{subset-of-union-fact-1}
{\rm{subset}}\,({\it{a\/}} $\cup$ {\it{b\/}}, {\it{c\/}})\index{subset} $=$ ({\rm{subset}}\,({\it{a\/}}, {\it{c\/}})\index{subset} $\wedge$ {\rm{subset}}\,({\it{b\/}}, {\it{c\/}})\index{subset})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  takeout-fact2 \\ \index{takeout-fact2}
({\it{a\/}} $\not\in$ {\it{x\/}}) $\rightarrow$ {\rm{set-equal}}\,({\rm{takeout}}\,({\it{x\/}}, {\it{a\/}})\index{takeout}, {\it{x\/}})\index{set-equal}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  stupid-lemma1 \\ \index{stupid-lemma1}
({\it{l\/}} $\in$ {\it{c\/}}) $\rightarrow$ ({\rm{subset}}\,({\rm{cons}}\,({\it{l\/}}, {\it{c\/}}), {\it{d\/}})\index{subset} $=$ {\rm{subset}}\,({\it{c\/}}, {\it{d\/}})\index{subset})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stupid-lemma2 \\ \index{stupid-lemma2}
({\it{l\/}} $\in$ {\it{d\/}}) $\rightarrow$ ({\rm{subset}}\,({\it{c\/}}, {\rm{cons}}\,({\it{l\/}}, {\it{d\/}}))\index{subset} $=$ {\rm{subset}}\,({\it{c\/}}, {\it{d\/}})\index{subset})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  stupid-lemma3 \\ \index{stupid-lemma3}
({\it{l\/}} $\in$ {\it{c\/}}) $\rightarrow$ ({\rm{set-member}}\,({\rm{cons}}\,({\it{l\/}}, {\it{c\/}}), {\it{d\/}})\index{set-member} $=$ {\rm{set-member}}\,({\it{c\/}}, {\it{d\/}})\index{set-member})
\end{tabbing}


\begin{verbatim};; some useful oddball facts about append other things
\end{verbatim}\begin{tabbing}{\sc Theorem}:  member-of-append-1 \\ \index{member-of-append-1}
({\it{a\/}} $\in$ {\it{x\/}}) $\rightarrow$ ({\it{a\/}} $\in$ {\rm{append}}\,({\it{x\/}}, {\it{y\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  is-last-element-means-member \\ \index{is-last-element-means-member}
({\rm{listp}}\,({\it{p\/}}) $\wedge$ ({\rm{car}}\,({\rm{last-element}}\,({\it{p\/}})\index{last-element}) $=$ {\it{x\/}})) $\rightarrow$ ({\it{x\/}} $\in$ {\rm{listofcars}}\,({\it{p\/}})\index{listofcars})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  membership-of-append \\ \index{membership-of-append}
({\it{a\/}} $\in$ {\it{x\/}}) $\rightarrow$ ({\it{a\/}} $\in$ {\rm{append}}\,({\it{y\/}}, {\it{x\/}}))
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  subset-of-append \\ \index{subset-of-append}
{\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\rightarrow$ {\rm{subset}}\,({\it{x\/}}, {\rm{append}}\,({\it{z\/}}, {\it{y\/}}))\index{subset}
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{first-non-unit} \\  
\=\+{\rm{first-non-unit}}\,({\it{clauses\/}})\index{first-non-unit} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{clauses\/}}) \\ 
{\bf then }\=\+{\bf if }{\tt{1}} $<$ {\rm{length}}\,({\rm{car}}\,({\it{clauses\/}}))\index{length}$\;\;${\bf then }{\rm{car}}\,({\it{clauses\/}}) \\ 
{\bf else }{\rm{first-non-unit}}\,({\rm{cdr}}\,({\it{clauses\/}}))\index{first-non-unit}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  first-non-unit-fact2 \\ \index{first-non-unit-fact2}
({\rm{length}}\,({\rm{first-non-unit}}\,({\it{x\/}})\index{first-non-unit})\index{length} $=$ {\tt{1}}) $=$ {\bf{f}}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{take-out-literal} \\  
\=\+{\rm{take-out-literal}}\,({\it{cs\/}}, {\it{c\/}})\index{take-out-literal} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{c\/}} $=$ {\rm{car}}\,({\it{cs\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{cdr}}\,({\it{c\/}}), {\rm{cdr}}\,({\it{cs\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{cs\/}}), {\rm{take-out-literal}}\,({\rm{cdr}}\,({\it{cs\/}}), {\it{c\/}})\index{take-out-literal})$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{take-out-clause} \\  
\=\+{\rm{take-out-clause}}\,({\it{cs\/}}, {\it{c\/}})\index{take-out-clause} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}}) \\ 
{\bf then }\=\+{\bf if }{\it{c\/}} $=$ {\rm{car}}\,({\it{cs\/}})$\;\;${\bf then }{\rm{cons}}\,({\rm{list}}\,({\rm{car}}\,({\it{c\/}})), {\rm{cdr}}\,({\it{cs\/}})) \\ 
{\bf else }{\rm{cons}}\,({\rm{car}}\,({\it{cs\/}}), {\rm{take-out-clause}}\,({\rm{cdr}}\,({\it{cs\/}}), {\it{c\/}})\index{take-out-clause})$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  subset-of-takeouts-fact \\ \index{subset-of-takeouts-fact}
\=\+(\=\+{\rm{validclauses}}\,({\it{x\/}})\index{validclauses} \\ 
$\wedge$$\;\;\;\;$({\it{a\/}} $\in$ {\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\rm{list}}\,({\rm{car}}\,({\it{a\/}})) $\in$ {\it{y\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{subset}}\,({\rm{takeout1}}\,({\it{x\/}}, {\it{a\/}})\index{takeout1}, {\it{y\/}})\index{subset})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{subset}}\,({\rm{take-out-clause}}\,({\it{x\/}}, {\it{a\/}})\index{take-out-clause}, {\it{y\/}})\index{subset}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  take-out-literal-communative-sort-of \\ \index{take-out-literal-communative-so!rt-of}
\=\+({\it{a\/}} $\in$ {\it{x\/}}) \\ 
$\rightarrow$$\;\;\;\;${\rm{set-equal}}\,({\rm{take-out-literal}}\,({\rm{cons}}\,({\it{y\/}}, {\it{x\/}}), {\it{a\/}})\index{take-out-literal}, {\rm{cons}}\,({\it{y\/}}, {\rm{take-out-literal}}\,({\it{x\/}}, {\it{a\/}})\index{take-out-literal}))\index{set-equal}\-
\end{tabbing}
	       

\begin{tabbing}{\sc Theorem}:  take-out-literal-preserves-validclauseness \\ \index{take-out-literal-preserves-vali!dclauseness}
\=\+(($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\wedge$ {\rm{validclauses}}\,({\it{cs\/}})\index{validclauses}) \\ 
$\rightarrow$$\;\;\;\;${\rm{validclauses}}\,({\rm{take-out-literal}}\,({\it{cs\/}}, {\it{x\/}})\index{take-out-literal})\index{validclauses}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  take-out-clause-preserves-validclauseness \\ \index{take-out-clause-preserves-valid!clauseness}
\=\+(($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\wedge$ {\rm{validclauses}}\,({\it{cs\/}})\index{validclauses}) \\ 
$\rightarrow$$\;\;\;\;${\rm{validclauses}}\,({\rm{take-out-clause}}\,({\it{cs\/}}, {\it{x\/}})\index{take-out-clause})\index{validclauses}\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{find-contradiction} \\  
\=\+{\rm{find-contradiction}}\,({\it{cs\/}})\index{find-contradiction} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{length}}\,({\rm{car}}\,({\it{cs\/}}))\index{length} $=$ {\tt{1}} \\ 
{\bf then }\=\+{\bf if }{\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{caar}}\,({\it{cs\/}}))) $\in$ {\rm{cdr}}\,({\it{cs\/}}) \\ 
{\bf then }{\rm{list}}\,({\bf{nil}}, {\rm{car}}\,({\it{cs\/}}), {\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{caar}}\,({\it{cs\/}})))) \\ 
{\bf elseif }{\rm{list}}\,({\rm{cadaar}}\,({\it{cs\/}})) $\in$ {\rm{cdr}}\,({\it{cs\/}}) \\ 
{\bf then }{\rm{list}}\,({\bf{nil}}, {\rm{car}}\,({\it{cs\/}}), {\rm{list}}\,({\rm{cadaar}}\,({\it{cs\/}}))) \\ 
{\bf else }{\rm{find-contradiction}}\,({\rm{cdr}}\,({\it{cs\/}}))\index{find-contradiction}$\;${\bf  endif}\- \\ 
{\bf else }{\rm{list}}\,({\bf{nil}}, {\bf{nil}}, {\bf{nil}})$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{number-of-lits} \\  
\=\+{\rm{number-of-lits}}\,({\it{cs\/}})\index{number-of-lits} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}})$\;\;${\bf then }{\rm{length}}\,({\rm{car}}\,({\it{cs\/}}))\index{length} $+$ {\rm{number-of-lits}}\,({\rm{cdr}}\,({\it{cs\/}}))\index{number-of-lits} \\ 
{\bf else }{\tt{0}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{excess-literal} \\  
{\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} $=$ ({\rm{number-of-lits}}\,({\it{cs\/}})\index{number-of-lits} $-$ {\rm{length}}\,({\it{cs\/}})\index{length})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  first-non-unit-fact \\ \index{first-non-unit-fact}
\=\+(({\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} $\not\simeq {\tt{0}}$) $\wedge$ ($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms})) \\ 
$\rightarrow$$\;\;\;\;$(({\tt{1}} $<$ {\rm{length}}\,({\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit})\index{length}) $=$ {\bf{t}})\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{adjust} \\  
\=\+{\rm{adjust}}\,({\it{proof\/}}, {\it{cs\/}}, {\it{l\/}})\index{adjust} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{proof\/}}) \\ 
{\bf then }\=\+{\bf if }{\rm{set-member}}\,({\rm{cadar}}\,({\it{proof\/}}), {\it{cs\/}})\index{set-member} \\ 
{\bf then }\=\+{\bf if }{\rm{set-member}}\,({\rm{caddar}}\,({\it{proof\/}}), {\it{cs\/}})\index{set-member} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{car}}\,({\it{proof\/}}), \\ 
{\rm{adjust}}\,({\rm{cdr}}\,({\it{proof\/}}), {\rm{cons}}\,({\rm{caar}}\,({\it{proof\/}}), {\it{cs\/}}), {\it{l\/}})\index{adjust})\- \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\rm{add-to-set}}\,({\it{l\/}}, {\rm{caar}}\,({\it{proof\/}})), \\ 
{\rm{cadar}}\,({\it{proof\/}}), \\ 
{\rm{add-to-set}}\,({\it{l\/}}, {\rm{caddar}}\,({\it{proof\/}})))\-, \\ 
{\rm{adjust}}\,(\=\+{\rm{cdr}}\,({\it{proof\/}}), \\ 
{\rm{cons}}\,({\rm{add-to-set}}\,({\it{l\/}}, {\rm{caar}}\,({\it{proof\/}})), {\it{cs\/}}), \\ 
{\it{l\/}})\-\index{adjust})\-$\;${\bf  endif}\- \\ 
{\bf elseif }{\rm{set-member}}\,({\rm{caddar}}\,({\it{proof\/}}), {\it{cs\/}})\index{set-member} \\ 
{\bf then }{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\rm{add-to-set}}\,({\it{l\/}}, {\rm{caar}}\,({\it{proof\/}})), \\ 
{\rm{add-to-set}}\,({\it{l\/}}, {\rm{cadar}}\,({\it{proof\/}})), \\ 
{\rm{caddar}}\,({\it{proof\/}}))\-, \\ 
{\rm{adjust}}\,({\rm{cdr}}\,({\it{proof\/}}), {\rm{cons}}\,({\rm{add-to-set}}\,({\it{l\/}}, {\rm{caar}}\,({\it{proof\/}})), {\it{cs\/}}), {\it{l\/}})\index{adjust})\- \\ 
{\bf else }{\rm{cons}}\,(\=\+{\rm{list}}\,(\=\+{\rm{add-to-set}}\,({\it{l\/}}, {\rm{caar}}\,({\it{proof\/}})), \\ 
{\rm{add-to-set}}\,({\it{l\/}}, {\rm{cadar}}\,({\it{proof\/}})), \\ 
{\rm{add-to-set}}\,({\it{l\/}}, {\rm{caddar}}\,({\it{proof\/}})))\-, \\ 
{\rm{adjust}}\,(\=\+{\rm{cdr}}\,({\it{proof\/}}), \\ 
{\rm{cons}}\,({\rm{add-to-set}}\,({\it{l\/}}, {\rm{caar}}\,({\it{proof\/}})), {\it{cs\/}}), \\ 
{\it{l\/}})\-\index{adjust})\-$\;${\bf  endif}\- \\ 
{\bf else }{\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  adjust-is-listp-when \\ \index{adjust-is-listp-when}
{\rm{listp}}\,({\it{p\/}}) $\rightarrow$ {\rm{listp}}\,({\rm{adjust}}\,({\it{p\/}}, {\it{x\/}}, {\it{l\/}})\index{adjust})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  when-first-non-unit-gives-clause \\ \index{when-first-non-unit-gives-clause}
\=\+(($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\wedge$ ({\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit} $\in$ {\it{cs\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  no-box-fact \\ \index{no-box-fact}
($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\rightarrow$ ({\rm{number-of-lits}}\,({\it{cs\/}})\index{number-of-lits} $\not<$ {\rm{length}}\,({\it{cs\/}})\index{length})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  excess-literal-in-terms-of-cdr \\ \index{excess-literal-in-terms-of-cdr}
\=\+({\rm{listp}}\,({\it{cs\/}}) $\wedge$ ($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms})) \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} \\ 
$=$$\;\;\;\;$(({\rm{length}}\,({\rm{car}}\,({\it{cs\/}}))\index{length} $+$ {\rm{excess-literal}}\,({\rm{cdr}}\,({\it{cs\/}}))\index{excess-literal}) $-\;1$))\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  when-take-out-literal-does-something \\ \index{when-take-out-literal-does-somet!hing}
\=\+(($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\wedge$ ({\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{excess-literal}}\,({\rm{take-out-literal}}\,({\it{cs\/}}, {\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit})\index{take-out-literal})\index{excess-literal} \\ 
$<$$\;\;\;\;${\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal})\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  not-box-when-clause-taken \\ \index{not-box-when-clause-taken}
\=\+(($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\wedge$ ({\tt{1}} $<$ {\rm{length}}\,({\it{x\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;$($\neg$ {\rm{box-in-axioms}}\,({\rm{take-out-clause}}\,({\it{cs\/}}, {\it{x\/}})\index{take-out-clause})\index{box-in-axioms})\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  no-box-zero-el-fact \\ \index{no-box-zero-el-fact}
\=\+({\rm{listp}}\,({\it{x\/}}) $\wedge$ ($\neg$ {\rm{box-in-axioms}}\,({\it{x\/}})\index{box-in-axioms}) $\wedge$ ({\rm{excess-literal}}\,({\it{x\/}})\index{excess-literal} $\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$({\rm{excess-literal}}\,({\rm{cdr}}\,({\it{x\/}}))\index{excess-literal} $\simeq {\tt{0}}$)\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  take-out-clause-fact \\ \index{take-out-clause-fact}
\=\+(($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\wedge$ ({\tt{1}} $<$ {\rm{length}}\,({\it{x\/}})\index{length}) $\wedge$ ({\it{x\/}} $\in$ {\it{cs\/}})) \\ 
$\rightarrow$$\;\;\;\;$(({\rm{excess-literal}}\,({\rm{take-out-clause}}\,({\it{cs\/}}, {\it{x\/}})\index{take-out-clause})\index{excess-literal} $<$ {\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal}) $=$ {\bf{t}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  when-take-out-clause-does-something \\ \index{when-take-out-clause-does-somet!hing}
\=\+(($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) $\wedge$ ({\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} $\not\simeq {\tt{0}}$)) \\ 
$\rightarrow$$\;\;\;\;$(\=\+(\=\+{\rm{excess-literal}}\,({\rm{take-out-clause}}\,({\it{cs\/}}, {\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit})\index{take-out-clause})\index{excess-literal} \\ 
$<$$\;\;\;\;${\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal})\- \\ 
$=$$\;\;\;\;${\bf{t}})\-\-
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{getproof} \\  
\=\+{\rm{getproof}}\,({\it{cs\/}})\index{getproof} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}$\;\;${\bf then }{\bf{nil}} \\ 
{\bf elseif }{\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} $\simeq {\tt{0}}$$\;\;${\bf then }{\rm{list}}\,({\rm{find-contradiction}}\,({\it{cs\/}})\index{find-contradiction}) \\ 
{\bf elseif }\=\+{\rm{car}}\,({\rm{last-element}}\,({\rm{adjust}}\,(\=\+{\rm{getproof}}\,({\rm{take-out-literal}}\,(\=\+{\it{cs\/}}, \\ 
{\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit})\-\index{take-out-literal})\index{getproof}, \\ 
{\it{cs\/}}, \\ 
{\rm{car}}\,({\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit}))\-\index{adjust})\index{last-element}) \\ 
$=$$\;\;\;\;${\bf{nil}}\- \\ 
{\bf then }{\rm{adjust}}\,(\=\+{\rm{getproof}}\,({\rm{take-out-literal}}\,({\it{cs\/}}, {\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit})\index{take-out-literal})\index{getproof}, \\ 
{\it{cs\/}}, \\ 
{\rm{car}}\,({\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit}))\-\index{adjust} \\ 
{\bf else }{\rm{append}}\,(\=\+{\rm{adjust}}\,(\=\+{\rm{getproof}}\,({\rm{take-out-literal}}\,(\=\+{\it{cs\/}}, \\ 
{\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit})\-\index{take-out-literal})\index{getproof}, \\ 
{\it{cs\/}}, \\ 
{\rm{car}}\,({\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit}))\-\index{adjust}, \\ 
{\rm{getproof}}\,({\rm{take-out-clause}}\,({\it{cs\/}}, {\rm{first-non-unit}}\,({\it{cs\/}})\index{first-non-unit})\index{take-out-clause})\index{getproof})\-$\;${\bf  endif}\-\-
\end{tabbing}








\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 3. Proof of the completeness theorem


;; the format of a resolution proof (implicit in validproof but useful to make explicit
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{proof-form} \\  
\=\+{\rm{proof-form}}\,({\it{p\/}})\index{proof-form} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{p\/}}) \\ 
{\bf then }\=\+{\rm{validclause}}\,({\rm{caar}}\,({\it{p\/}}))\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\rm{cadar}}\,({\it{p\/}}))\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\rm{caddar}}\,({\it{p\/}}))\index{validclause} \\ 
$\wedge$$\;\;\;\;$({\rm{cdddar}}\,({\it{p\/}}) $=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;${\rm{proof-form}}\,({\rm{cdr}}\,({\it{p\/}}))\index{proof-form}\- \\ 
{\bf else }{\it{p\/}} $=$ {\bf{nil}}$\;${\bf  endif}\-\-
\end{tabbing}



\begin{verbatim};; some useful facts about valid proofs
\end{verbatim}\begin{tabbing}{\sc Theorem}:  validproof-on-subset \\ \index{validproof-on-subset}
({\rm{subset}}\,({\it{x\/}}, {\it{y\/}})\index{subset} $\wedge$ {\rm{validproof}}\,({\it{x\/}}, {\it{p\/}})\index{validproof}) $\rightarrow$ {\rm{validproof}}\,({\it{y\/}}, {\it{p\/}})\index{validproof}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  validproof-clauses-commutative \\ \index{validproof-clauses-commutative}
{\rm{set-equal}}\,({\it{x\/}}, {\it{y\/}})\index{set-equal} $\rightarrow$ ({\rm{validproof}}\,({\it{x\/}}, {\it{p\/}})\index{validproof} $=$ {\rm{validproof}}\,({\it{y\/}}, {\it{p\/}})\index{validproof})
\end{tabbing}


\begin{verbatim};; A useful fact about unsatisfiable sets of clauses
\end{verbatim}\begin{tabbing}{\sc Theorem}:  assignment-interchangeable \\ \index{assignment-interchangeable}
({\rm{unsatwith}}\,({\it{c\/}}, {\it{cs\/}}, {\it{z\/}})\index{unsatwith} $\wedge$ {\rm{set-equal}}\,({\it{y\/}}, {\it{z\/}})\index{set-equal}) $\rightarrow$ {\rm{unsatwith}}\,({\it{c\/}}, {\it{cs\/}}, {\it{y\/}})\index{unsatwith}
\end{tabbing}


\begin{verbatim};; lemmas about preservation of unsatisfiablility of clauses with some of 
;; the literals removed

\end{verbatim}\begin{tabbing}{\sc Theorem}:  take-out-literal-helper \\ \index{take-out-literal-helper}
\=\+{\rm{unsatwith}}\,({\it{clause\/}}, {\it{cs\/}}, {\it{v\/}})\index{unsatwith} \\ 
$\rightarrow$$\;\;\;\;${\rm{unsatwith}}\,(\=\+{\rm{car}}\,({\rm{take-out-literal}}\,({\rm{cons}}\,({\it{clause\/}}, {\it{cs\/}}), {\it{x\/}})\index{take-out-literal}), \\ 
{\rm{cdr}}\,({\rm{take-out-literal}}\,({\rm{cons}}\,({\it{clause\/}}, {\it{cs\/}}), {\it{x\/}})\index{take-out-literal}), \\ 
{\it{v\/}})\-\index{unsatwith}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  without-literal-still-unsatisfiable \\ \index{without-literal-still-unsatisfi!able}
({\rm{unsatisfiable}}\,({\it{cs\/}})\index{unsatisfiable} $\wedge$ {\rm{listp}}\,({\it{cs\/}})) $\rightarrow$ {\rm{unsatisfiable}}\,({\rm{take-out-literal}}\,({\it{cs\/}}, {\it{x\/}})\index{take-out-literal})\index{unsatisfiable}
\end{tabbing}



\begin{tabbing}{\sc Theorem}:  unsat-stepper \\ \index{unsat-stepper}
({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{unsatwith}}\,({\it{x\/}}, {\it{cs\/}}, {\it{v\/}})\index{unsatwith}) $\rightarrow$ {\rm{unsatwith}}\,({\rm{list}}\,({\rm{car}}\,({\it{x\/}})), {\it{cs\/}}, {\it{v\/}})\index{unsatwith}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  take-out-clause-helper \\ \index{take-out-clause-helper}
\=\+({\rm{listp}}\,({\it{x\/}}) $\wedge$ {\rm{unsatwith}}\,({\it{clause\/}}, {\it{cs\/}}, {\it{v\/}})\index{unsatwith}) \\ 
$\rightarrow$$\;\;\;\;${\rm{unsatwith}}\,(\=\+{\rm{car}}\,({\rm{take-out-clause}}\,({\rm{cons}}\,({\it{clause\/}}, {\it{cs\/}}), {\it{x\/}})\index{take-out-clause}), \\ 
{\rm{cdr}}\,({\rm{take-out-clause}}\,({\rm{cons}}\,({\it{clause\/}}, {\it{cs\/}}), {\it{x\/}})\index{take-out-clause}), \\ 
{\it{v\/}})\-\index{unsatwith}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  when-unsatisfiable \\ \index{when-unsatisfiable}
{\rm{unsatwith}}\,({\it{clause\/}}, {\it{cs\/}}, {\it{z\/}})\index{unsatwith} $\rightarrow$ {\rm{unsatwith}}\,({\it{clause\/}}, {\it{cs\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{z\/}}))\index{unsatwith}
\end{tabbing}

\begin{tabbing}{\sc Definition}:\index{unsat-induct} \\  
\=\+{\rm{unsat-induct}}\,({\it{c\/}}, {\it{x\/}}, {\it{cs\/}}, {\it{v\/}})\index{unsat-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{cs\/}}) \\ 
{\bf then }\=\+{\bf if }({\it{x\/}} $=$ {\rm{cadr}}\,({\rm{car}}\,({\it{c\/}}))) $\vee$ ({\it{x\/}} $=$ {\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{car}}\,({\it{c\/}})))$\;\;${\bf then }{\bf{t}} \\ 
{\bf else }{\rm{unsat-induct}}\,({\rm{car}}\,({\it{cs\/}}), {\it{x\/}}, {\rm{cdr}}\,({\it{cs\/}}), {\rm{cons}}\,({\rm{car}}\,({\it{c\/}}), {\it{v\/}}))\index{unsat-induct}$\;${\bf  endif}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{verbatim};; useful facts about negations of literals
\end{verbatim}\begin{tabbing}{\sc Theorem}:  reversible-nots-1 \\ \index{reversible-nots-1}
\=\+(\=\+({\rm{length}}\,({\it{y\/}})\index{length} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;${\rm{litatom}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $\not=$ {\bf{nil}}) \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{y\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $=$ {\rm{cadar}}\,({\it{y\/}})))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{x\/}})) $=$ {\it{y\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  reversible-nots-2 \\ \index{reversible-nots-2}
\=\+(\=\+({\rm{length}}\,({\it{y\/}})\index{length} $=$ {\tt{1}}) \\ 
$\wedge$$\;\;\;\;${\rm{listp}}\,({\it{x\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{y\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;$({\it{x\/}} $=$ {\rm{list}}\,({\tt{'}}{\tt{not}}, {\rm{car}}\,({\it{y\/}}))))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{list}}\,({\rm{cadr}}\,({\it{x\/}})) $=$ {\it{y\/}})\-
\end{tabbing}



\begin{verbatim};; useful definition of set of clauses with all unit clauses
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{allunits} \\  
\=\+{\rm{allunits}}\,({\it{x\/}})\index{allunits} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{x\/}})$\;\;${\bf then }({\rm{length}}\,({\rm{car}}\,({\it{x\/}}))\index{length} $=$ {\tt{1}}) $\wedge$ {\rm{allunits}}\,({\rm{cdr}}\,({\it{x\/}}))\index{allunits} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  allunit-means \\ \index{allunit-means}
{\rm{allunits}}\,({\it{x\/}})\index{allunits} $\rightarrow$ ($\neg$ {\rm{listp}}\,({\rm{cdar}}\,({\it{x\/}})))
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  allunits-if \\ \index{allunits-if}
(($\neg$ {\rm{box-in-axioms}}\,({\it{x\/}})\index{box-in-axioms}) $\wedge$ ({\rm{excess-literal}}\,({\it{x\/}})\index{excess-literal} $\simeq {\tt{0}}$)) $\rightarrow$ {\rm{allunits}}\,({\it{x\/}})\index{allunits}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  unit-clause-fact \\ \index{unit-clause-fact}
({\rm{length}}\,({\it{x\/}})\index{length} $=$ {\tt{1}}) $\rightarrow$ ({\rm{takeout}}\,({\it{x\/}}, {\rm{car}}\,({\it{x\/}}))\index{takeout} $=$ {\bf{nil}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  restriction-list-commutative \\ \index{restriction-list-commutative}
{\rm{set-equal}}\,({\it{z1\/}}, {\it{z2\/}})\index{set-equal} $\rightarrow$ ({\rm{unsatwith}}\,({\it{x\/}}, {\it{y\/}}, {\it{z1\/}})\index{unsatwith} $=$ {\rm{unsatwith}}\,({\it{x\/}}, {\it{y\/}}, {\it{z2\/}})\index{unsatwith})
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  unsat-ignore-first-helper \\ \index{unsat-ignore-first-helper}
\=\+(\=\+({\rm{litatom}}\,({\it{x\/}}) $\rightarrow$ ({\rm{list}}\,({\rm{list}}\,({\tt{'}}{\tt{not}}, {\it{x\/}})) $\not\in$ {\rm{cons}}\,({\it{c\/}}, {\it{cs\/}}))) \\ 
$\wedge$$\;\;\;\;$({\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\rm{list}}\,({\rm{cadr}}\,({\it{x\/}})) $\not\in$ {\rm{cons}}\,({\it{c\/}}, {\it{cs\/}}))) \\ 
$\wedge$$\;\;\;\;${\rm{allunits}}\,({\rm{cons}}\,({\it{c\/}}, {\it{cs\/}}))\index{allunits} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\rm{list}}\,({\it{x\/}}))\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclauses}}\,({\rm{cons}}\,({\it{c\/}}, {\it{cs\/}}))\index{validclauses} \\ 
$\wedge$$\;\;\;\;${\rm{unsatwith}}\,({\it{c\/}}, {\it{cs\/}}, {\rm{cons}}\,({\it{x\/}}, {\it{v\/}}))\index{unsatwith})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{unsatwith}}\,({\it{c\/}}, {\it{cs\/}}, {\it{v\/}})\index{unsatwith}\-
\end{tabbing}

 
\begin{verbatim};; base case of main theorem - if all clauses unit then getproof finds a proof
\end{verbatim}\begin{tabbing}{\sc Theorem}:  no-excess-literal-proof \\ \index{no-excess-literal-proof}
\=\+(\=\+{\rm{validclauses}}\,({\it{cs\/}})\index{validclauses} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{box-in-axioms}}\,({\it{cs\/}})\index{box-in-axioms}) \\ 
$\wedge$$\;\;\;\;$({\rm{excess-literal}}\,({\it{cs\/}})\index{excess-literal} $\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{unsatisfiable}}\,({\it{cs\/}})\index{unsatisfiable})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{finishedproof}}\,({\it{cs\/}}, {\rm{list}}\,({\rm{find-contradiction}}\,({\it{cs\/}})\index{find-contradiction}))\index{finishedproof}\-
\end{tabbing}


\begin{verbatim};; useful definition of "almost" valid proof.  p is validproof of cs except that
;; some clauses in proof are missing literal l
\end{verbatim}\begin{tabbing}{\sc Definition}:\index{validproof-but-for-literal} \\  
\=\+{\rm{validproof-but-for-literal}}\,({\it{cs\/}}, {\it{p\/}}, {\it{l\/}})\index{validproof-but-for-literal} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{p\/}}) \\ 
{\bf then }\=\+(\=\+{\rm{set-member}}\,({\rm{cadar}}\,({\it{p\/}}), {\it{cs\/}})\index{set-member} \\ 
$\vee$$\;\;\;\;${\rm{set-member}}\,({\rm{add-to-set}}\,({\it{l\/}}, {\rm{cadar}}\,({\it{p\/}})), {\it{cs\/}})\index{set-member})\- \\ 
$\wedge$$\;\;\;\;$(\=\+{\rm{set-member}}\,({\rm{caddar}}\,({\it{p\/}}), {\it{cs\/}})\index{set-member} \\ 
$\vee$$\;\;\;\;${\rm{set-member}}\,({\rm{add-to-set}}\,({\it{l\/}}, {\rm{caddar}}\,({\it{p\/}})), {\it{cs\/}})\index{set-member})\- \\ 
$\wedge$$\;\;\;\;${\rm{resolvent}}\,({\rm{caar}}\,({\it{p\/}}), {\rm{cadar}}\,({\it{p\/}}), {\rm{caddar}}\,({\it{p\/}}))\index{resolvent} \\ 
$\wedge$$\;\;\;\;${\rm{validproof-but-for-literal}}\,({\rm{cons}}\,({\rm{caar}}\,({\it{p\/}}), {\it{cs\/}}), {\rm{cdr}}\,({\it{p\/}}), {\it{l\/}})\index{validproof-but-for-literal}\- \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}



\begin{verbatim};; some facts about validproof-but-for-literal
\end{verbatim}\begin{tabbing}{\sc Theorem}:  validproof-but-for-literal-clauses-commutative \\ \index{validproof-but-for-literal-clau!ses-commutative}
\=\+{\rm{set-equal}}\,({\it{x\/}}, {\it{y\/}})\index{set-equal} \\ 
$\rightarrow$$\;\;\;\;$(\=\+{\rm{validproof-but-for-literal}}\,({\it{x\/}}, {\it{p\/}}, {\it{l\/}})\index{validproof-but-for-literal} \\ 
$=$$\;\;\;\;${\rm{validproof-but-for-literal}}\,({\it{y\/}}, {\it{p\/}}, {\it{l\/}})\index{validproof-but-for-literal})\-\-
\end{tabbing}


\begin{tabbing}{\sc Definition}:\index{adding-literal-induct} \\  
\=\+{\rm{adding-literal-induct}}\,({\it{cs\/}}, {\it{p\/}})\index{adding-literal-induct} \\ 
$=$$\;\;\;\;$\=\+{\bf if }{\rm{listp}}\,({\it{p\/}})$\;\;${\bf then }{\rm{adding-literal-induct}}\,({\rm{cons}}\,({\rm{caar}}\,({\it{p\/}}), {\it{cs\/}}), {\rm{cdr}}\,({\it{p\/}}))\index{adding-literal-induct} \\ 
{\bf else }{\bf{t}}$\;${\bf  endif}\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  adding-literal-fact \\ \index{adding-literal-fact}
\=\+{\rm{validproof-but-for-literal}}\,({\rm{cons}}\,({\it{x\/}}, {\it{cs\/}}), {\it{p\/}}, {\it{l\/}})\index{validproof-but-for-literal} \\ 
$\rightarrow$$\;\;\;\;${\rm{validproof-but-for-literal}}\,({\rm{cons}}\,({\rm{add-to-set}}\,({\it{l\/}}, {\it{x\/}}), {\it{cs\/}}), {\it{p\/}}, {\it{l\/}})\index{validproof-but-for-literal}\-
\end{tabbing}


\begin{verbatim};; facts about adjusting clauses by adding literals and still getting valid resolvents
\end{verbatim}\begin{tabbing}{\sc Theorem}:  resolvent-with-extra-literal-fact1b \\ \index{resolvent-with-extra-literal-fa!ct1b}
\=\+(\=\+{\rm{validliteral}}\,({\it{l\/}})\index{validliteral} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not\in$ {\it{p2\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\in$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p2\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1list\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1list\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1list\/}}, {\it{p1\/}}, {\rm{cons}}\,({\it{l\/}}, {\it{p2\/}}))\index{resolvent-help}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  resolvent-with-extra-literal-fact1c \\ \index{resolvent-with-extra-literal-fa!ct1c}
\=\+(\=\+{\rm{validliteral}}\,({\it{l\/}})\index{validliteral} \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not\in$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not\in$ {\it{p2\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p2\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1list\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1list\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{resolvent-help}}\,({\rm{cons}}\,({\it{l\/}}, {\it{r\/}}), {\it{p1list\/}}, {\it{p1\/}}, {\rm{cons}}\,({\it{l\/}}, {\it{p2\/}}))\index{resolvent-help}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  resolvent-with-extra-literal-fact2a \\ \index{resolvent-with-extra-literal-fa!ct2a}
\=\+(\=\+({\it{l\/}} $\not\in$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not\in$ {\it{p1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{validliteral}}\,({\it{l\/}})\index{validliteral} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p2\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1list\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1list\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{resolvent-help}}\,({\rm{cons}}\,({\it{l\/}}, {\it{r\/}}), {\it{p1list\/}}, {\rm{cons}}\,({\it{l\/}}, {\it{p1\/}}), {\it{p2\/}})\index{resolvent-help}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  resolvent-with-extra-literal-fact2b \\ \index{resolvent-with-extra-literal-fa!ct2b}
\=\+(\=\+({\it{l\/}} $\in$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not\in$ {\it{p1\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{validliteral}}\,({\it{l\/}})\index{validliteral} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p2\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1list\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1list\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1list\/}}, {\rm{cons}}\,({\it{l\/}}, {\it{p1\/}}), {\it{p2\/}})\index{resolvent-help}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  resolvent-with-extra-literal-fact3a \\ \index{resolvent-with-extra-literal-fa!ct3a}
\=\+(\=\+({\it{l\/}} $\not\in$ {\it{r\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not\in$ {\it{p1\/}}) \\ 
$\wedge$$\;\;\;\;$({\it{l\/}} $\not\in$ {\it{p2\/}}) \\ 
$\wedge$$\;\;\;\;${\rm{validliteral}}\,({\it{l\/}})\index{validliteral} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p2\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{validclause}}\,({\it{p1list\/}})\index{validclause} \\ 
$\wedge$$\;\;\;\;${\rm{resolvent-help}}\,({\it{r\/}}, {\it{p1list\/}}, {\it{p1\/}}, {\it{p2\/}})\index{resolvent-help})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{resolvent-help}}\,({\rm{cons}}\,({\it{l\/}}, {\it{r\/}}), {\it{p1list\/}}, {\rm{cons}}\,({\it{l\/}}, {\it{p1\/}}), {\rm{cons}}\,({\it{l\/}}, {\it{p2\/}}))\index{resolvent-help}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  resolvent-fact \\ \index{resolvent-fact}
{\rm{resolvent-help}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{d\/}})\index{resolvent-help} $\rightarrow$ {\rm{resolvent-help}}\,({\rm{cons}}\,({\it{l\/}}, {\it{a\/}}), {\it{b\/}}, {\it{c\/}}, {\it{d\/}})\index{resolvent-help}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  extra-try-resolvent-fact \\ \index{extra-try-resolvent-fact}
{\rm{resolvent-help}}\,({\it{a\/}}, {\it{b\/}}, {\it{c\/}}, {\it{d\/}})\index{resolvent-help} $\rightarrow$ {\rm{resolvent-help}}\,({\it{a\/}}, {\rm{cons}}\,({\it{l\/}}, {\it{b\/}}), {\it{c\/}}, {\it{d\/}})\index{resolvent-help}
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  when-not-member-of-take-out-literal \\ \index{when-not-member-of-take-out-lite!ral}
\=\+(({\tt{1}} $<$ {\rm{length}}\,({\it{c\/}})\index{length}) $\wedge$ ({\it{a\/}} $\in$ {\rm{take-out-literal}}\,({\it{x\/}}, {\it{c\/}})\index{take-out-literal}) $\wedge$ ({\it{a\/}} $\not\in$ {\it{x\/}})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{cons}}\,({\rm{car}}\,({\it{c\/}}), {\it{a\/}}) $\in$ {\it{x\/}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  take-out-literal-is-validclause \\ \index{take-out-literal-is-validclause}
\=\+({\rm{validclauses}}\,({\it{x\/}})\index{validclauses} $\wedge$ ({\tt{1}} $<$ {\rm{length}}\,({\it{c\/}})\index{length})) \\ 
$\rightarrow$$\;\;\;\;${\rm{validclauses}}\,({\rm{take-out-literal}}\,({\it{x\/}}, {\it{c\/}})\index{take-out-literal})\index{validclauses}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-of-validclause-is-validlit \\ \index{member-of-validclause-is-validlit}
({\rm{validclause}}\,({\it{cs\/}})\index{validclause} $\wedge$ ({\it{l\/}} $\in$ {\it{cs\/}})) $\rightarrow$ {\rm{validliteral}}\,({\it{l\/}})\index{validliteral}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  when-literal-not-there \\ \index{when-literal-not-there}
({\rm{validclauses}}\,({\it{cs\/}})\index{validclauses} $\wedge$ ({\it{x\/}} $\not\in$ {\it{cs\/}})) $\rightarrow$ ({\rm{take-out-literal}}\,({\it{cs\/}}, {\it{x\/}})\index{take-out-literal} $=$ {\it{cs\/}})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  real-proof-implies-almost-proof \\ \index{real-proof-implies-almost-proof}
{\rm{validproof}}\,({\it{cs\/}}, {\it{p\/}})\index{validproof} $\rightarrow$ {\rm{validproof-but-for-literal}}\,({\it{cs\/}}, {\it{p\/}}, {\it{x\/}})\index{validproof-but-for-literal}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  when-not-in-bigger-clauses \\ \index{when-not-in-bigger-clauses}
\=\+(($\neg$ {\rm{set-member}}\,({\it{x\/}}, {\it{cs\/}})\index{set-member}) $\wedge$ {\rm{set-member}}\,({\it{x\/}}, {\rm{take-out-literal}}\,({\it{cs\/}}, {\it{p\/}})\index{take-out-literal})\index{set-member}) \\ 
$\rightarrow$$\;\;\;\;${\rm{set-equal}}\,({\rm{cdr}}\,({\it{p\/}}), {\it{x\/}})\index{set-equal}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  take-out-literal-produces-almost-proof \\ \index{take-out-literal-produces-almost!-proof}
\=\+(\=\+{\rm{proof-form}}\,({\it{p\/}})\index{proof-form} \\ 
$\wedge$$\;\;\;\;${\rm{validproof}}\,({\rm{take-out-literal}}\,({\it{cs\/}}, {\it{c\/}})\index{take-out-literal}, {\it{p\/}})\index{validproof} \\ 
$\wedge$$\;\;\;\;${\rm{validclauses}}\,({\it{cs\/}})\index{validclauses} \\ 
$\wedge$$\;\;\;\;$({\tt{1}} $<$ {\rm{length}}\,({\it{c\/}})\index{length}))\- \\ 
$\rightarrow$$\;\;\;\;${\rm{validproof-but-for-literal}}\,({\it{cs\/}}, {\it{p\/}}, {\rm{car}}\,({\it{c\/}}))\index{validproof-but-for-literal}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  member-of-validclauses-is-validclause \\ \index{member-of-validclauses-is-valid!clause}
({\rm{validclauses}}\,({\it{x\/}})\index{validclauses} $\wedge$ ({\it{a\/}} $\in$ {\it{x\/}})) $\rightarrow$ {\rm{validclause}}\,({\it{a\/}})\index{validclause}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  find-contradiction-returns-proof-form \\ \index{find-contradiction-returns-proo!f-form}
\=\+(\=\+($\neg$ {\rm{box-in-axioms}}\,({\it{x\/}})\index{box-in-axioms}) \\ 
$\wedge$$\;\;\;\;$({\rm{excess-literal}}\,({\it{x\/}})\index{excess-literal} $\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{unsatisfiable}}\,({\it{x\/}})\index{unsatisfiable} \\ 
$\wedge$$\;\;\;\;${\rm{validclauses}}\,({\it{x\/}})\index{validclauses})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{proof-form}}\,({\rm{list}}\,({\rm{find-contradiction}}\,({\it{x\/}})\index{find-contradiction}))\index{proof-form}\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  proofs-together-have-form-if-both-do \\ \index{proofs-together-have-form-if-bot!h-do}
({\rm{proof-form}}\,({\it{x\/}})\index{proof-form} $\wedge$ {\rm{proof-form}}\,({\it{y\/}})\index{proof-form}) $\rightarrow$ {\rm{proof-form}}\,({\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{proof-form}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  adjust-does-not-unform-proofs \\ \index{adjust-does-not-unform-proofs}
({\rm{proof-form}}\,({\it{x\/}})\index{proof-form} $\wedge$ {\rm{validliteral}}\,({\it{l\/}})\index{validliteral}) $\rightarrow$ {\rm{proof-form}}\,({\rm{adjust}}\,({\it{x\/}}, {\it{cs\/}}, {\it{l\/}})\index{adjust})\index{proof-form}
\end{tabbing}

\begin{verbatim};; getproof returns something that is of a resolution proof form
;; (later we show that this proof is "valid")
\end{verbatim}\begin{tabbing}{\sc Theorem}:  getproof-gives-proof-form \\ \index{getproof-gives-proof-form}
({\rm{unsatisfiable}}\,({\it{x\/}})\index{unsatisfiable} $\wedge$ {\rm{validclauses}}\,({\it{x\/}})\index{validclauses}) $\rightarrow$ {\rm{proof-form}}\,({\rm{getproof}}\,({\it{x\/}})\index{getproof})\index{proof-form}
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  allunits-means-no-excess-literal \\ \index{allunits-means-no-excess-litera!l}
{\rm{allunits}}\,({\it{x\/}})\index{allunits} $\rightarrow$ ({\rm{excess-literal}}\,({\it{x\/}})\index{excess-literal} $\simeq {\tt{0}}$)
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  find-contradiction-returns-box \\ \index{find-contradiction-returns-box}
\=\+(\=\+{\rm{unsatisfiable}}\,({\it{x\/}})\index{unsatisfiable} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{box-in-axioms}}\,({\it{x\/}})\index{box-in-axioms}) \\ 
$\wedge$$\;\;\;\;$({\rm{excess-literal}}\,({\it{x\/}})\index{excess-literal} $\simeq {\tt{0}}$) \\ 
$\wedge$$\;\;\;\;${\rm{validclauses}}\,({\it{x\/}})\index{validclauses})\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\rm{find-contradiction}}\,({\it{x\/}})\index{find-contradiction}) $=$ {\bf{nil}})\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  last-element-fact \\ \index{last-element-fact}
{\rm{listp}}\,({\it{x\/}}) $\rightarrow$ ({\rm{last-element}}\,({\rm{append}}\,({\it{y\/}}, {\it{x\/}}))\index{last-element} $=$ {\rm{last-element}}\,({\it{x\/}})\index{last-element})
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  getproof-is-list-when \\ \index{getproof-is-list-when}
($\neg$ {\rm{box-in-axioms}}\,({\it{x\/}})\index{box-in-axioms}) $\rightarrow$ {\rm{listp}}\,({\rm{getproof}}\,({\it{x\/}})\index{getproof})
\end{tabbing}

\begin{verbatim};; the last resolvent in a getproof-generated proof is box
\end{verbatim}\begin{tabbing}{\sc Theorem}:  getproof-returns-box \\ \index{getproof-returns-box}
\=\+({\rm{unsatisfiable}}\,({\it{x\/}})\index{unsatisfiable} $\wedge$ {\rm{validclauses}}\,({\it{x\/}})\index{validclauses} $\wedge$ ($\neg$ {\rm{box-in-axioms}}\,({\it{x\/}})\index{box-in-axioms})) \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\rm{last-element}}\,({\rm{getproof}}\,({\it{x\/}})\index{getproof})\index{last-element}) $=$ {\bf{nil}})\-
\end{tabbing}

\begin{verbatim};; adjusting a proof ending in box yields a proof ending in box or a proof
;; whose last resolvent has just the literal used to adjust the proof
\end{verbatim}\begin{tabbing}{\sc Theorem}:  adjusted-proof-gets \\ \index{adjusted-proof-gets}
\=\+({\rm{car}}\,({\rm{last-element}}\,({\it{p\/}})\index{last-element}) $=$ {\bf{nil}}) \\ 
$\rightarrow$$\;\;\;\;$(\=\+({\rm{car}}\,({\rm{last-element}}\,({\rm{adjust}}\,({\it{p\/}}, {\it{x\/}}, {\it{l\/}})\index{adjust})\index{last-element}) $=$ {\bf{nil}}) \\ 
$\vee$$\;\;\;\;$({\rm{car}}\,({\rm{last-element}}\,({\rm{adjust}}\,({\it{p\/}}, {\it{x\/}}, {\it{l\/}})\index{adjust})\index{last-element}) $=$ {\rm{list}}\,({\it{l\/}})))\-\-
\end{tabbing}


\begin{tabbing}{\sc Theorem}:  what-adjusted-proof-returns \\ \index{what-adjusted-proof-returns}
\=\+(\=\+{\rm{unsatisfiable}}\,({\it{x\/}})\index{unsatisfiable} \\ 
$\wedge$$\;\;\;\;${\rm{validclauses}}\,({\it{x\/}})\index{validclauses} \\ 
$\wedge$$\;\;\;\;$($\neg$ {\rm{box-in-axioms}}\,({\it{x\/}})\index{box-in-axioms}) \\ 
$\wedge$$\;\;\;\;$({\rm{car}}\,({\rm{last-element}}\,({\rm{adjust}}\,({\rm{getproof}}\,({\it{x\/}})\index{getproof}, {\it{y\/}}, {\it{l\/}})\index{adjust})\index{last-element}) $\not=$ {\bf{nil}}))\- \\ 
$\rightarrow$$\;\;\;\;$({\rm{car}}\,({\rm{last-element}}\,({\rm{adjust}}\,({\rm{getproof}}\,({\it{x\/}})\index{getproof}, {\it{y\/}}, {\it{l\/}})\index{adjust})\index{last-element}) $=$ {\rm{list}}\,({\it{l\/}}))\-
\end{tabbing}


\begin{verbatim};; adjusting an "almost" correct proof yields a correct proof
\end{verbatim}\begin{tabbing}{\sc Theorem}:  adjusting-makes-proofs-valid \\ \index{adjusting-makes-proofs-valid}
\=\+(\=\+{\rm{validliteral}}\,({\it{l\/}})\index{validliteral} \\ 
$\wedge$$\;\;\;\;${\rm{proof-form}}\,({\it{p\/}})\index{proof-form} \\ 
$\wedge$$\;\;\;\;${\rm{validclauses}}\,({\it{cs\/}})\index{validclauses} \\ 
$\wedge$$\;\;\;\;${\rm{validproof-but-for-literal}}\,({\it{cs\/}}, {\it{p\/}}, {\it{l\/}})\index{validproof-but-for-literal})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{validproof}}\,({\it{cs\/}}, {\rm{adjust}}\,({\it{p\/}}, {\it{cs\/}}, {\it{l\/}})\index{adjust})\index{validproof}\-
\end{tabbing}



\begin{tabbing}{\sc Theorem}:  validproof-of-append \\ \index{validproof-of-append}
\=\+(\=\+{\rm{proof-form}}\,({\it{x\/}})\index{proof-form} \\ 
$\wedge$$\;\;\;\;${\rm{proof-form}}\,({\it{y\/}})\index{proof-form} \\ 
$\wedge$$\;\;\;\;${\rm{validclauses}}\,({\it{cs\/}})\index{validclauses} \\ 
$\wedge$$\;\;\;\;${\rm{validproof}}\,({\it{cs\/}}, {\it{x\/}})\index{validproof} \\ 
$\wedge$$\;\;\;\;${\rm{validproof}}\,({\rm{append}}\,({\rm{listofcars}}\,({\it{x\/}})\index{listofcars}, {\it{cs\/}}), {\it{y\/}})\index{validproof})\- \\ 
$\rightarrow$$\;\;\;\;${\rm{validproof}}\,({\it{cs\/}}, {\rm{append}}\,({\it{x\/}}, {\it{y\/}}))\index{validproof}\-
\end{tabbing}

\begin{tabbing}{\sc Theorem}:  getproof-returns-validproof \\ \index{getproof-returns-validproof}
({\rm{unsatisfiable}}\,({\it{x\/}})\index{unsatisfiable} $\wedge$ {\rm{validclauses}}\,({\it{x\/}})\index{validclauses}) $\rightarrow$ {\rm{validproof}}\,({\it{x\/}}, {\rm{getproof}}\,({\it{x\/}})\index{getproof})\index{validproof}
\end{tabbing}




\begin{verbatim};;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; the completeness theorem

\end{verbatim}\begin{tabbing}{\sc Theorem}:  resolution-is-complete \\ \index{resolution-is-complete}
({\rm{unsatisfiable}}\,({\it{x\/}})\index{unsatisfiable} $\wedge$ {\rm{validclauses}}\,({\it{x\/}})\index{validclauses}) $\rightarrow$ {\rm{finishedproof}}\,({\it{x\/}}, {\rm{getproof}}\,({\it{x\/}})\index{getproof})\index{finishedproof}
\end{tabbing}

%\end{list}
\printindex
\end{document}
