\documentclass{article}
\usepackage{fullpage}
\usepackage{amsmath}
\usepackage{amssymb}
\newcounter{probcnt}
\newenvironment{problem}{\stepcounter{probcnt}{\bf Problem \arabic{probcnt}}.}{}
\newcounter{pracprobcnt}
\newenvironment{pracproblem}{\stepcounter{pracprobcnt}{\bf Practice Problem \arabic{pracprobcnt}}.}{}
\setlength{\parskip}{.4cm}
\setlength{\baselineskip}{15pt}
\setlength{\parindent}{0cm}
\newcommand{\meanl} {[\![}
\newcommand{\meanr} {]\!]}
\newcommand{\means}[1] {\meanl #1 \meanr}
\newcommand{\propsem}[2] {#1\means{#2}}
\newcommand{\logprf} {\vdash}
\newcommand{\logcnsq} {\models}
\author{}
\date{}
\begin{document}
\hrule
\begin{center}
{\LARGE \sc $\underline{\mbox{Homework 1}}$} \\
{\Large \sc CS 498 MV: Logic in Computer Science}\\
\ \\
\begin{tabular}{ll}
Assigned: September 6, 2018 & Due on: September 13, 2018
\end{tabular}
\end{center}
\hrule
{\bf Instructions:} Please do not turn in solutions to the practice
problems. Solutions to the homework problems should be turned in as a
PDF file on Gradescope. See instructions on Piazza.
{\bf Recommended Reading:} Lectures 1 through 3: propositional logic,
proof systems (Frege and Resolution), soundness and completeness.
$\underline{\mbox{\bf Practice Problems}}$
\begin{pracproblem}
The following sentence is taken from the specification of a telephone
system: ``If the directory database is opened, then the monitor is put
in a closed state, if the system is not in its initial state.'' Find
an equivalent easier to understand specification that involves
disjunctions and negations but no implications.
\end{pracproblem}
\begin{pracproblem}
Are the following system specifications consistent? Determine this by
encoding the specification in logic and using your favorite proof
system to determine if the constructed formula is satisfiable.
\vspace*{-0.5cm}
\begin{enumerate}
\item ``The system is in multiuser state if and only if it is
operating normally. If the system is operating normally, the kernel
is functioning. The kernel is not functioning or the system is in
interrupt mode. If the system is not in multiuser state, then it is
in interrupt mode. The system is not in interrupt mode.''
\item ``If the file system is not locked, then new messages will be
queued. If the file system is not locked, then the system is
functioning normally, and conversely. If new messages are not
queued, then they will be sent to the message buffer. If the file
system is not locked, the new messages will be sent to the message
buffer. New messages will not be sent to the message buffer.''
\end{enumerate}
\end{pracproblem}
\vspace*{-0.5cm}
$\underline{\mbox{\bf Homework Problems}}$
\begin{problem}
A set $S$ is said to be \emph{countable} if there is a function $f: S
\to {\mathbb N}$ that is 1-to-1. For a set $A$, $A^*$ is the set of
all finite strings over $A$. Prove that if $A$ is countable then $A^*$
is countable.
\end{problem}
\begin{problem}
Prove the soundness theorem for the Frege Proof system. That is, show
that if $\Gamma \logprf \varphi$ then $\Gamma \logcnsq
\varphi$. \emph{Hint:} Let $\psi_1, \psi_2, \ldots \psi_m$ be a proof of
$\varphi$ from $\Gamma$. Prove by induction on $i$ that, for every
$i$, $\Gamma \logcnsq \psi_i$
\end{problem}
\begin{problem}
For the Frege proof system, prove the Deduction Theorem (without
assuming the completeness theorem). That is, if $\Gamma \cup
\{\varphi\} \logprf \psi$ then $\Gamma \logprf \varphi \rightarrow
\psi$. {\em Hint:} Let $\psi_1, \psi_2, \ldots \psi_m$ be a proof of
$\psi$ from $\Gamma \cup \{\varphi\}$. Show by induction on $i$ that,
for every $i$, $\Gamma \logprf \varphi \rightarrow \psi_i$.
\end{problem}
\begin{problem}
The Davis-Putnam proof showing the completeness of resolution,
outlines an algorithm to determine satisfiability of a set of
clauses. Use the Davis-Putnam algorithm to determine if the following
sets of clauses are satisfiable. Outline all the steps of the
algorithm in each case.
\begin{enumerate}
\item $\Gamma = \{\{a,b,c\}, \{b,\neg c, \neg f\}, \{\neg b, e\}\}$
\item $\Gamma = \{\{a,b\}, \{a,\neg b\}, \{\neg a, c\}, \{\neg a, \neg
c\}\}$
\end{enumerate}
\end{problem}
\end{document}