\documentclass{article}
\input{../6825-preamble}
\usepackage{longtable}
\begin{document}
\psetnum{1b}
\date{2005/10/13}
\lstset{language=homework}
\lstset{frame=trbl}
\lstset{basicstyle=\footnotesize}

\newenvironment{proofsketch}{\trivlist\item[]\emph{Proof sketch}:}%
{\unskip\nobreak\hskip 1em plus 1fil\nobreak$\qed$
\parfillskip=0pt%
\endtrivlist}

\begin{pset}
  \begin{problem}
    We formalize the argument as follows:
    \begin{align}
      \forall x\;\; Man(x) \implies Mortal(x)\\
      \forall x\;\; Mortal(x) \implies Boring(x)\\
      \neg Boring(Hera)\\
      \intertext{And the conclusion}
      \exists x\;\; \neg Man(x)
    \end{align}

    \begin{proofsketch}
      We'll prove this by negating the desired conclusion and arriving
      at a contradiction by resolution. We'll begin by resolving (1)
      and (2) to show that all men are boring (S5), then resolve this
      with (3) to show that Hera is not a man (S6). When we resolve
      this with the negation of our conclusion (4), we reach a
      contradiction (S7).
    \end{proofsketch}
      
    \begin{proof}
      \-\\
      \begin{scriptsize}
        \begin{longtable}{lp{3.5in}p{2.5in}}
          \input{hera-proof.tex}
        \end{longtable}
      \end{scriptsize}
    \end{proof}
  \end{problem}

  \begin{problem}
    \begin{proofsketch}
      We'll prove that the surgeon is the child's mother by resolution
      refutation. We first show that since the surgeon (\texttt{CA} in
      the proof) can't operate on \texttt{CS}, she must either not be
      a surgeon or \texttt{CS}'s parent (S11). But we know \texttt{CA}
      is a surgeon (A8), so \texttt{CA} must be a parent of
      \texttt{CS} (S12). Applying the definition of a parent (A4), we
      find that \texttt{CA} must be either \texttt{CS}'s father or
      mother (S13). Since she is not the father (A9), she must be the
      mother (S14).
    \end{proofsketch}

    \begin{proof}
      \-\\
      \begin{scriptsize}
        \begin{longtable}{lp{3.5in}p{2.5in}}
          \input{doctor-proof.tex}
        \end{longtable}
      \end{scriptsize}      
    \end{proof}
  \end{problem}

  \begin{problem}
    \begin{proofsketch}
      First, the solution: to put \texttt{A} on \texttt{B}, we'll
      first move \texttt{C} to the table to clear \texttt{B}, then
      move \texttt{A} to \texttt{B}.

      First, we move \texttt{C} to the table. Steps S31 and S32 show
      that we can make this move because both \texttt{C} and the table
      are clear, and S33 shows that the result is that \texttt{B} is
      now clear. Now we need to establish that we can move \texttt{A}
      onto \texttt{B}. We need \texttt{B} to be clear, which we just
      showed. This tells us that if some block is clear, we can move
      it onto \texttt{B} (S34). In (S35), we resolve with our desired
      condition (A30); the resulting unification establishes that
      \texttt{A} is the block we want to move onto \texttt{B}. In
      order to move \texttt{A}, we'll need to show that \texttt{A} is
      clear and on some other block. (S36-S38) show that \texttt{A} is
      clear because it was clear before we moved \texttt{B} and wasn't
      affected by the move; (S39) and (S40) shows that \texttt{A} is
      still on the table after the move. This means that we can move
      \texttt{A} onto \texttt{B}, which gives us the desired result
      (S41).
    \end{proofsketch}
    
    \begin{proof}
      \-\\
      \begin{scriptsize}
        \begin{longtable}{lp{3.5in}p{2.5in}}
          \input{blocks-proof.tex}
        \end{longtable}
      \end{scriptsize}      
    \end{proof}
  \end{problem}

  \begin{problem}
    \begin{proofsketch}
      We'll prove that if \texttt{A1} and \texttt{A2} are on
      \texttt{W2} and \texttt{W3} respectively in \texttt{S1}, then
      \texttt{A1} is allowed to move to \texttt{W4}. In order to do
      so, we'll begin by showing that no athlete is currently on
      \texttt{W4}. (S61) and (S63) show that \texttt{A1} isn't on
      \texttt{W4} since it can only be on one station, and (S62) and
      (S64) do the same for \texttt{A2}.

      Now we'll reach a contradiction from the negated conclusion
      (A60): since we assume \texttt{A1} isn't allowed to move to
      \texttt{W4}, we'll show this must mean that \texttt{A1} or
      \texttt{A2} is on \texttt{W4} in \texttt{S1}, which we just
      showed wasn't the case. Resolving (A60) with the definition of
      \texttt{Allowed}, we obtain (S66) that there is some blocking
      athlete preventing \texttt{A1} from moving to \texttt{A4},
      because it is already on \texttt{W4} (S65). But according to
      (A26), \texttt{A1} and \texttt{A2} are the only athletes, so the
      blocking athlete is one of them (S67); therefore, \texttt{A1} or
      \texttt{A2} must be on \texttt{W4} (S68-S69). But this
      contradicts our earlier results of (S63-S64), proving the
      theorem.
    \end{proofsketch}
    \begin{proof}
      \-\\
      \begin{scriptsize}
        \begin{longtable}{lp{3.5in}p{2.5in}}
          \input{equip1-proof.tex}
        \end{longtable}
      \end{scriptsize}      
    \end{proof}    
  \end{problem}

  \begin{problem}
    \begin{proofsketch}
      We show that there exists a conflict because both \texttt{A1}
      and \texttt{A2} can be on \texttt{W4} in \texttt{S2}. We first
      establish that \texttt{A1} and \texttt{A2} are both on stations
      that connect to \texttt{W4}, so they can both move to
      \texttt{W4} if they are \texttt{Allowed} to(S62-S65). Then we must show
      that both are \texttt{Allowed} to move to \texttt{W4}. We show
      this in much the same way as Problem 4. First, neither \texttt{A1} nor
      \texttt{A2} is on \texttt{W4} (S66-S71) and (S72-S77)
      respectively --- details omitted. Then, we show that \texttt{A1}
      is allowed to move to \texttt{W4} because neither of the two
      athletes is blocking it (S78-S87), and similarly for \texttt{A2}
      (S88-S97). Hence, since two different athletes can be on the
      same station in \texttt{S2}, there is a conflict
      (S98-S101).
    \end{proofsketch}
    \newpage
    \begin{proof}
      \-\\
      \begin{scriptsize}
        \begin{longtable}{lp{3.5in}p{2.5in}}
          \input{equip2-proof.tex}
        \end{longtable}
      \end{scriptsize}
    \end{proof}    
  \end{problem}
\end{pset}

\end{document}