\documentstyle[6.034-ps,marc,11pt]{article}
\pagestyle{empty}

\name{Marc Horowitz}
\recitation{Rulane, R10}
\handout{12}
\handoutdate{October 25, 1990}
\psnum{5}
\duedate{November 2, 1990}

\parskip=0.25in
\parindent=0.0in

\def\part #1{\vspace{0.05in}\par\noindent{\bf Part #1.}\vspace{0.05in}\par}
\def\lor{\vee}
\def\and{\wedge}
\def\not{\neg}
\def\impl{\Rightarrow}
\def\on{\mbox{on}}
\def\clear{\mbox{clear}}
\def\equal{\mbox{equal}}
\def\puton{\mbox{puton}}
\def\a{\mbox{a}}
\def\b{\mbox{b}}
\def\c{\mbox{c}}
\def\s{\mbox{s0}}
\def\t{\mbox{table}}
\def\proof#1{\null\vbox{\halign{\hbox to\hsize{\hfill$\ignorespaces##\hfilneg$\hfill}&\llap{(\ignorespaces##\hfilneg)}\cr#1}}\null}
\def\ul#1{\underline{#1}}
\def\twoline#1#2{\vcenter{\hbox{$#1$}\hbox{$#2$}}}
\def\nil{\mbox{Nil}}
\long\def\comment#1{}

\begin{document}
\maketitle

\part A
\noindent\(\begin{array}{@{}ll}%
1 &	\forall x\forall y\forall s[
	( \clear(x,s) \and \clear(y,s) \and \not\equal(x,y) )
	\impl
	\on(x,y,\puton(x,y,s))
	] \\
2 &	\forall x\forall y\forall z\forall s[
	\begin{array}[t]{@{}l}
	( \on(x,y,s) \and \clear(x,s) \and \clear(z,s) \and
	  \not\equal(y,z) \and \not\equal(x,z) ) \\
	\impl \\
	\clear(y,\puton(x,z,s)]
	\end{array} \\
3 &	\forall x\forall y\forall s\forall u[
	\clear(u,s) \and \not\equal(u,y)
	\impl
	\clear(u,\puton(x,y,s))
	] \\
4 &	\forall s[\clear(\t,s)] \\
5 &	\on(\b,\a,\s) \\
6 &	\on(\a,\t,\s) \\
7 &	\clear(\b,\s) \\
8 &	\clear(\c,\s) \\
9 &	\on(\c,\t,\s) \\
\\
11 &	\not\equal(\a,\t) \\
12 &	\not\equal(\b,\t) \\
13 &	\not\equal(\c,\t) \\
14 &	\not\equal(\a,\b) \\
15 &	\not\equal(\a,\c) \\
16 &	\not\equal(\b,\a) \\
17 &	\not\equal(\b,\c) \\
18 &	\not\equal(\c,\a) \\
19 &	\not\equal(\c,\b) \\
\\
10 &	\forall s[\not\clear(\a,s) \lor \not\clear(\c,s)]
\end{array}\)

\setlength{\unitlength}{0.75in}
\begin{picture}(4,3)(0,0)
\put(0,0){\line(0,1){1}}
\put(3.5,0){\line(0,1){1}}
\put(0,1){\line(1,0){3.5}}
\put(1.75,0.5){\makebox(0,0){Table}}
\put(0.5,1.0){\framebox(1,0.5){A}}
\put(2,1.0){\framebox(1,0.5){C}}
\put(0.75,1.51){\framebox(0.5,0.5){B}}
\end{picture}

\part B

In equation (2), substitute b for $x$, a for $y$, table for $z$, and
s0 for $s$.  In equation (10), substitute puton(b,table,s0) for $s$:

\proof{
\twoline{
 \not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t) \lor
}{
 \ul{\clear(\a,\puton(\b,\t,\s))}
}						& 2\cr
\ul{\not\clear(\a,\puton(\b,\t,\s))}
  \lor \not\clear(\c,\puton(\b,\t,\s))		& 10\cr
\twoline{
 \not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t) \lor
}{
 \not\clear(\c,\puton(\b,\t,\s))
}						& 20\cr
}

In equation (3), substitute b for $x$, table for $y$, s0 for $s$, and
c for $u$: 

\proof{
\not\clear(\c,\s) \lor
 \equal(\c,\t) \lor
 \ul{\clear(\c,\puton(\b,\t,\s))}		& 3\cr
\twoline{
 \not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t) \lor
}{
 \ul{\not\clear(\c,\puton(\b,\t,\s))}
}						& 20\cr
\twoline{
 \not\clear(\c,\s) \lor
 \equal(\c,\t) \lor
 \not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
}{
 \equal(\a,\t) \lor
 \equal(\b,\t)
}						& 21\cr
}

\proof{
\ul{\clear(\c,\s)}				& 8\cr
\twoline{
 \ul{\not\clear(\c,\s)} \lor
 \equal(\c,\t) \lor
 \not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
}{
 \equal(\a,\t) \lor
 \equal(\b,\t)
}						& 21\cr
\twoline{
 \equal(\c,\t) \lor
 \not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
}{
 \equal(\b,\t)
}						& 22\cr
}

\proof{
\ul{\not\equal(\c,\t)}				& 13\cr
\twoline{
 \ul{\equal(\c,\t)} \lor
 \not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
}{
 \equal(\b,\t)
}						& 22\cr
\not\on(\b,\a,\s) \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)					& 23\cr
}

\proof{
\ul{\on(\b,\a,\s)}				& 5\cr
\ul{\not\on(\b,\a,\s)} \lor
 \not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)					& 23\cr
\not\clear(\b,\s) \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)					& 24\cr
}

\proof{
\ul{\clear(\b,\s)}				& 7\cr
\ul{\not\clear(\b,\s)} \lor
 \not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)					& 24\cr
\not\clear(\t,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)					& 25\cr
}

\proof{
\ul{\clear(\t,\s)}				& 4\cr
\ul{\not\clear(\t,\s)} \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)					& 25\cr
\equal(\a,\t) \lor
 \equal(\b,\t)					& 26\cr
}

\proof{
\ul{\not\equal(\a,\t)}				& 11\cr
\ul{\equal(\a,\t)} \lor
 \equal(\b,\t)					& 26\cr
\equal(\b,\t)					& 27\cr
}

\proof{
\ul{\not\equal(\b,\t)}				& 12\cr
\equal(\b,\t)					& 27\cr
\nil						& 28\cr
}

\part C
\begin{verbatim}
 CYCLE=137, 60 clauses waiting to resolve ...
(CONTRADICTION 528 13)

 RESOLVE called with:
   (10 (S) ((NOT CLEAR A S) (NOT CLEAR C S))) 
   (2 (X Y Z S)
    ((NOT ON X Y S) (NOT CLEAR X S) (NOT CLEAR Z S) (EQUAL Y Z)
     (EQUAL X Z) (CLEAR Y (PUTON X Z S)))) 
 Resolvents are:
(20 (Y4 Y3 Y1)
 ((NOT CLEAR C (PUTON Y1 Y3 Y4)) (NOT ON Y1 A Y4) (NOT CLEAR Y1 Y4)
  (NOT CLEAR Y3 Y4) (EQUAL A Y3) (EQUAL Y1 Y3)))

 RESOLVE called with:
   (20 (Y4 Y3 Y1)
    ((NOT CLEAR C (PUTON Y1 Y3 Y4)) (NOT ON Y1 A Y4) (NOT CLEAR Y1 Y4)
     (NOT CLEAR Y3 Y4) (EQUAL A Y3) (EQUAL Y1 Y3))) 
   (5 NIL ((ON B A S0))) 
 Resolvents are:
(34 (X2)
 ((NOT CLEAR C (PUTON B X2 S0)) (NOT CLEAR B S0) (NOT CLEAR X2 S0)
  (EQUAL A X2) (EQUAL B X2)))

 RESOLVE called with:
   (34 (X2)
    ((NOT CLEAR C (PUTON B X2 S0)) (NOT CLEAR B S0) (NOT CLEAR X2 S0)
     (EQUAL A X2) (EQUAL B X2))) 
   (4 (S) ((CLEAR TABLE S))) 
 Resolvents are:
(53 NIL
 ((NOT CLEAR C (PUTON B TABLE S0)) (NOT CLEAR B S0) (EQUAL A TABLE)
  (EQUAL B TABLE)))

 RESOLVE called with:
   (53 NIL
    ((NOT CLEAR C (PUTON B TABLE S0)) (NOT CLEAR B S0) (EQUAL A TABLE)
     (EQUAL B TABLE))) 
   (3 (X Y S U) ((NOT CLEAR U S) (EQUAL U Y) (CLEAR U (PUTON X Y S)))) 
 Resolvents are:
(64 NIL
 ((NOT CLEAR B S0) (EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0)
  (EQUAL C TABLE)))

 RESOLVE called with:
   (64 NIL
    ((NOT CLEAR B S0) (EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0)
     (EQUAL C TABLE))) 
   (7 NIL ((CLEAR B S0))) 
 Resolvents are:
(516 NIL
 ((EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0) (EQUAL C TABLE)))

 RESOLVE called with:
   (516 NIL
    ((EQUAL A TABLE) (EQUAL B TABLE) (NOT CLEAR C S0) (EQUAL C TABLE))) 
   (8 NIL ((CLEAR C S0))) 
 Resolvents are:
(521 NIL ((EQUAL A TABLE) (EQUAL B TABLE) (EQUAL C TABLE)))

 RESOLVE called with:
   (521 NIL ((EQUAL A TABLE) (EQUAL B TABLE) (EQUAL C TABLE))) 
   (11 NIL ((NOT EQUAL A TABLE))) 
 Resolvents are:
(525 NIL ((EQUAL B TABLE) (EQUAL C TABLE)))

 RESOLVE called with:
   (525 NIL ((EQUAL B TABLE) (EQUAL C TABLE))) 
   (12 NIL ((NOT EQUAL B TABLE))) 
 Resolvents are:
(528 NIL ((EQUAL C TABLE)))

 RESOLVE called with:
   (528 NIL ((EQUAL C TABLE))) 
   (13 NIL ((NOT EQUAL C TABLE))) 
 Resolvents are:
(CONTRADICTION 528 13)
\end{verbatim}

\proof{
\ul{\not\clear(\a,\puton(y1,y3,y4))} \lor
 \not\clear(\c,\puton(y1,y3,y4))	& 10\cr
\twoline{
 \not\on(y1,\a,y4) \lor
 \not\clear(y1,y4) \lor
 \not\clear(y3,y4) \lor
 \equal(\a,y3) \lor
 \equal(y1,y3) \lor
}{
 \ul{\clear(\a,\puton(y1,y3,y4))}
}					& 2\cr
\twoline{
 \not\clear(\c,\puton(y1,y3,y4)) \lor
 \not\on(y1,\a,y4) \lor
 \not\clear(y1,y4) \lor
 \not\clear(y3,y4) \lor
 \equal(\a,y3) \lor
}{
 \equal(y1,y3)
}					& 20\cr
}

\proof{
\twoline{
 \not\clear(\c,\puton(\b,x2,\s)) \lor
 \ul{\not\on(\b,\a,\s)} \lor
 \not\clear(\b,\s) \lor
 \not\clear(x2,\s) \lor
 \equal(\a,x2) \lor
}{
 \equal(\b,x2)
}					& 20\cr
\ul{\on(\b,\a,\s)}			& 5\cr
\not\clear(\c,\puton(\b,x2,\s)) \lor
 \not\clear(\b,\s) \lor
 \not\clear(x2,\s) \lor
 \equal(\a,x2) \lor
 \equal(\b,x2)				& 34\cr
}

\proof{
\twoline{
 \not\clear(\c,\puton(\b,\t,\s)) \lor
 \not\clear(\b,\s) \lor
 \ul{\not\clear(\t,\s)} \lor
 \equal(\a,\t) \lor
}{
 \equal(\b,\t)
}					& 34\cr
\ul{\clear(\t,\s)}			& 4\cr
\not\clear(\c,\puton(\b,\t,\s)) \lor
 \not\clear(\b,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)				& 53\cr
}

\proof{
\ul{\not\clear(\c,\puton(\b,\t,\s))} \lor
 \not\clear(\b,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)				& 53\cr
\not\clear(\c,\s) \lor
 \equal(\c,\t) \lor
 \ul{\clear(\c,\puton(\b,\t,\s))}	& 3\cr
\not\clear(\b,\s) \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)
 \not\clear(\c,\s) \lor
 \equal(\c,\t)				& 64\cr
}

\proof{
\ul{\not\clear(\b,\s)} \lor
 \equal(\a,\t) \lor
 \equal(\b,\t)
 \not\clear(\c,\s) \lor
 \equal(\c,\t)				& 64\cr
\ul{\clear(\b,\s)}			& 7\cr
\equal(\a,\t) \lor
 \equal(\b,\t)
 \not\clear(\c,\s) \lor
 \equal(\c,\t)				& 516\cr
}

\proof{
\equal(\a,\t) \lor
 \equal(\b,\t)
 \ul{\not\clear(\c,\s)} \lor
 \equal(\c,\t)				& 516\cr
\ul{\clear(\c,\s)}			& 8\cr
\equal(\a,\t) \lor
 \equal(\b,\t)
 \equal(\c,\t)				& 521\cr
}

\proof{
\ul{\equal(\a,\t)} \lor
 \equal(\b,\t)
 \equal(\c,\t)				& 521\cr
\ul{\not\equal(\a,\t)}			& 11\cr
\equal(\b,\t)
 \equal(\c,\t)				& 525\cr
}

\proof{
\ul{\equal(\b,\t)}
 \equal(\c,\t)				& 525\cr
\ul{\not\equal(\b,\t)}			& 12\cr
\equal(\c,\t)				& 528\cr
}

\proof{
\ul{\equal(\c,\t)}			& 528\cr
\ul{\not\equal(\c,\t)}			& 13\cr
\nil					& \omit\cr
}

Both my proof and the program's proof combine the same rules to arrive
at the contradiction.  The proofs are very similar in intent, they
vary only where the order of steps is not significant to the meaning
of the proof.

\part {D,E}
You said punt, so I punted.

\part F
Since the proof is an exponential process, it is important to have a
good heuristic to limit the search.  Simply calling the
greater-numbered clause ``better'' is mostly a random heuristic.  The
better the estimating the function, the closer the search will be to
something like an ideal A* search.  (If \verb+CLAUSE-IS-BETTER+ was
always right, the search would be very short.)  The given
\verb+CLAUSE-IS-BETTER+ function is closer to a depth-first search.

\end{document}
