\documentclass{article}
\usepackage{graphicx}
\usepackage[colorlinks=true,urlcolor=black,linkcolor=blue,citecolor=blue]{hyperref}%
\usepackage{fancyhdr}
\usepackage[margin=35mm]{geometry}
\usepackage{amsmath}
\usepackage{stmaryrd}   % for the tval symbol
\usepackage{algpseudocode}
\usepackage{tikz}
\usetikzlibrary{trees}
\newcommand{\fn}[1]{\mathrm{#1}}
\newcommand{\append}{\mathbin{+\mkern-10mu+}}
\newcommand{\cons}{\mathbin{::}}
\newcommand{\tval}[1]{\llbracket #1 \rrbracket}
\newcommand{\liff}{\leftrightarrow}
% If you don't have the stmaryrd package, the following substitute will do.
%\newcommand{\tval}[1]{[\![ #1 ]\!]}

\usepackage{bussproofs}
\EnableBpAbbreviations

\pagestyle{fancy}
\fancyhf{}
\renewcommand{\headrulewidth}{0pt}

\lhead{\sf Logic and Mechanized Reasoning}
\rhead{\sf Fall 2021}

\begin{document}

\bigskip

\begin{center}
{\Large Assignment 8}

\medskip

due 6pm Thursday, October 28, 2021
\end{center}

\medskip

\thispagestyle{fancy}

\noindent For the first three problems, you are asked to provide formal proofs in
various proof systems. You can describe the first two using a tree format, or by simply
giving a numbered list of formulas/clauses/sequents and giving a justification for each one in terms of the earlier numbers.
You are also free to take a picture of a hand-drawn
proof, as long as it is easily readable.
(If you are really serious about typesetting proof trees, we recommend the BussProofs
package, \url{https://www.math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/index.html}.)

\medskip

\subsection*{Problem 1 (3 points)}

Consider the following two axioms:
\begin{enumerate}
  \item $A \to (B \to A)$
  \item $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$.
\end{enumerate}
These are really axiom \emph{schemas}, which means that you can replace $A$ and $B$
with any propositional formulas. The only rule of inference is modus ponens:
\begin{quote}
From $A \to B$ and $A$ derive $B$.
\end{quote}
Let $p$ be a propositional variable. Show how to derive $p \to p$ in this system. (It is surprisingly tricky, but you can do it in five lines.)

\subsection*{Problem 2 (3 points)}

Remember the (cut-free) sequent calculus described in Section 8.2.
Either construct a proof of the following sequent or use the methods described
in that section to find a counterexample:
\[
((p \lor q) \to r) \lor ((r \to p) \land (r \to q)).
\]

\subsection*{Problem 3 (3 points)}

Give a resolution refutation of the following list of clauses:
\begin{enumerate}
\item $p \lor q \lor \lnot r$
\item $\lnot p \lor \lnot q \lor r$
\item $q \lor r  \lor \lnot s$
\item $\lnot q \lor \lnot r \lor s$
\item $p \lor r \lor s$
\item $\lnot p \lor \lnot r \lor \lnot s$
\item $\lnot p \lor q \lor s$
\item $p \lor \lnot q \lor \lnot s$
\end{enumerate}
Please present your solution as a list of clauses extending the list of starting
clauses, so the first one you derive should be numbered 9. For each one,
specify the two clauses that serve as input to the resolution rule by indicating their numbers.

There is a solution with 11 additional clauses, for a total of 19.
If your list has more than 26 clauses altogether, please look for a shorter proof!

\subsection*{Problem 4 (3 points)}

In Section 8.3, we outline a method for extracting a resolution refutation of a set of clauses,
$\Gamma$, from a failed refutation proof.
The method relies on the following claim:
\begin{quote}
  If there are a resolution proof of a clause $C$ from $\Gamma$ such that
  $\tval{C}_{\tau[p \mapsto \top]} = \bot$
  and a resolution proof of a clause $D$ from $\Gamma$ such that
  $\tval{D}_{\tau[p \mapsto \bot]} = \bot$,
  then there is a resolution proof of a clause $E$ from $\Gamma$ such that
  $\tval{E}_\tau = \bot$.
\end{quote}
Here $\tau$ is a partial truth assignment and the notation $\tval{C}_\tau$ refers to the simplification of the
clause $C$ with respect to assignment $\tau$ that is described in Section 6.2.

Prove this claim.

\subsection*{Problem 5 (6 points)}

Fill in the proofs of the propositional formulas found in {\tt assignment8.lean}.

\end{document}