\documentclass[fontsize=9pt]{scrartcl}
\usepackage{t1enc}
\usepackage[latin2]{inputenc}
\usepackage[a4paper,noheadfoot,left=13mm,right=13mm,top=13mm,bottom=13mm]{geometry}
\usepackage{enumitem}
\usepackage{url}
\usepackage{graphicx}
%\pagestyle{empty}
\newcommand{\alert}{}
\newcommand{\red}{}
\newcommand{\green}{}
\newcommand{\pause}{}
\usepackage{amsmath}
\usepackage{alltt}
\usepackage{hyperref}


\begin{document}

\setlength{\parindent}{0cm} 
\setlength{\parskip}{0.5ex} 

%% \setlength{\abovedisplayskip}{2pt}
%% \setlength{\abovedisplayshortskip}{0pt}
%% \setlength{\belowdisplayskip}{2pt}
%% \setlength{\belowdisplayshortskip}{0pt}

\begin{center}
\textbf{\Large
              AIT Semantic and Declarative Technologies Course\\[1ex]
              Optional Practice L3-2:  Propositional Resolution \\[1ex]}
              (3 optional points per puzzle solved)
              
\end{center}

\bigskip

\textbf{\Large Inspector Craig puzzles}

\medskip


Below is a set of problems from Raymond Smullyan's ``What is the name of
this book''. The chapter is entitled ``From the cases of Inspector
Craig''. Each puzzle involves some suspects of a crime, named A, B,
etc. Some of them are guilty, some innocent. There are some statements given.


\begin{description}
\item Example

An enormous amount of loot had been stolen from a store. The criminal (or criminals) took the heist away in a
car. Three well-known criminals A, B, C were brought to Scotland Yard for questioning. The following facts were
ascertained:

\begin{enumerate}[label=(\arabic*)]
\item No one other than A, B, C was involved in the robbery.
\item C never works without A (and possibly others) as an accomplice.
\item B does not know how to drive.
\end{enumerate}

Is A innocent or guilty?

Your tasks:
\begin{enumerate}[label=(\roman*)]
\item Try to solve the puzzle as a recreational task :-).

\item Transform each statement into a propositional formula involving the
letters A, B, etc. as atomic propositions. Proposition $X$ stands for ``X
is guilty''.
\begin{enumerate}
\item A is guilty or B is guilty or C is guilty:  $A \vee B \vee C$
\item If C is guilty then A is guilty:  $C \rightarrow A$
\item It cannot be the case that only B is guilty: $B \rightarrow (A \vee C)$
\end{enumerate}

\item Transform each  propositional formula into conjunctive normal form
(CNF), then show the clauses in simplified form:
\begin{enumerate}
\item $A \vee B \vee C$ (already in CNF), clauses:                       \texttt{+A +B +C.}
\item $C \rightarrow A$, CNF: $\neg C \vee A$, clauses:                  \texttt{-C +A.   }
\item $B \rightarrow (A \vee C)$, CNF: $\neg B \vee A \vee C$, clauses:  \texttt{-B +A +C.}
\end{enumerate}
(Note that in general a single statement can give rise to multiple clauses.)

\item Collect the clauses, give each a reference number and perform a
resolution proof:
\begin{alltt}
(1)             +A +B +C.
(2)             -C +A.   
(3)             -B +A +C.
(4)             +A +C.        (1)/2 rw (3)/1   \textrm{\parbox[top]{3em}{read} clause (1) literal 2 resolved with}
                                               \textrm{\parbox[top]{3em}{    } clause (3) literal 1}
(5)             +A.           (4)/2 rw (2)/1   
\end{alltt}

\item Remove the clauses implied by other clauses:

  Clauses  \texttt{(1)} -- \texttt{(4)} each contain the literal  \texttt{+A}, so they all
  are a trivial consequence of  \texttt{(5)}. Hence   clauses  \texttt{(1)}
  -- \texttt{(4)}
  can be removed.

\item Interpret the answer: A is guilty.
\end{enumerate}
\end{description}

\bigskip

\textbf{Your task:}

\medskip

Perform the above steps for the following six puzzles. \\
For steps {(iii)--(v)} we suggest to use the Plwin tool:
\href{https://ait.plwin.dev/L3-2}{\texttt{https://ait.plwin.dev/L3-2}}. \\
Enter the conjunction of the formulas you obtained in step (ii) into the
tool and then perform the steps (iii)--(v) within the tool.
If you do so, there is no need to submit
any further material.

\bigskip

\begin{enumerate}
%  \setcounter{enumi}{4}
\item Another robbery. A, B, and C were brought in for questioning and the following facts were found:
\begin{enumerate}[label=(\arabic*)]
\item No one other than A, B, and C was involved.
\item A never works without at least one accomplice.
\item C is innocent.
\end{enumerate}
Is B innocent or guilty?

\clearpage

\item ``What do you make of these three facts?'' asked Inspector Craig to Sergeant McPherson.
\begin{enumerate}[label=(\arabic*)]
\item If A is guilty and B is innocent, then C is guilty.
\item C never works alone.
\item A never works with C.
\item No one other than A, B, or C was involved, and at least one of them is guilty.
\end{enumerate}
The Sergeant scratched his head and said, ``Not much, I'm afraid. Can you tell from these facts which are
innocent and which are guilty?''
``No,'' said Craig, ``but there is enough to know that one of them is guilty.'' Which is it?
\vspace*{2.5cm}

\item This time four suspects A, B, C, D were rounded up for questioning after a robbery. It is known for sure that at
least one of them is guilty and that no one outside the four is involved. The following facts appeared:
\begin{enumerate}[label=(\arabic*)]
\item A was definitely innocent.
\item If B was guilty, then he had exactly one accomplice.
\item If C was guilty, then he had exactly two accomplices.
\end{enumerate}
Inspector Craig especially wanted to know whether D was guilty, because he was a particularly dangerous
criminal. Is D guilty or not?
\vspace*{2.5cm}
\item Three men A, B, and C are on trial for participation in a robbery. In this case, the following two facts were
established:
\begin{enumerate}[label=(\arabic*)]
\item If A is innocent or B is guilty, then C is guilty.
\item If A is innocent, then C is innocent.
\end{enumerate}
Can the guilt of any one of the three be established?
\vspace*{2.5cm}

\item In this case, there are four defendants, A, B, C, and D. The following facts are established:
\begin{enumerate}[label=(\arabic*)]
\item If A is guilty, then B was an accomplice.                       
\item If B is guilty then either C was an accomplice or A is innocent.      
\item If D is innocent then A is guilty and C is innocent.                    
\item If D is guilty, so is A.
\end{enumerate}
  Which ones are innocent and which are guilty?
\vspace*{2.5cm}

  
%% \item In this case, the robbery occurred in London. Three well-known criminals A, B, and C were collected for
%% questioning. Now, A and C were identical twins and could not be told apart. Both were timid and would not
%% work without an accomplice (1). B, on the other hand, was bold and always
%% worked alone (2). Also, witnesses said that at the time of the robbery, one of the two twins was seen eating ice cream in Dover, but it is not known which
%% twin (3).
%% Again, if no one but A, B, and C are involved in the robbery (4), which ones are innocent and which are
%% guilty?
%% \vspace*{2.5cm}

\item Mr. McGregor, a London shopkeeper, phoned the police and said that his shop had been robbed. Three suspects
A, B, and C were rounded up for questioning. The following facts were established:
\begin{enumerate}[label=(\arabic*)]
\item Each of the men A, B, C had been in the shop on the day of the robbery, and no one else had been there
on that day.
\item If A was guilty, then he had exactly one accomplice.
\item If B is innocent, so is C.
\item If exactly two are guilty, then A is one of them.
\item If C is innocent, so is B.
\end{enumerate}
Whom did Inspector Craig indict? :-)
  \end{enumerate}


\end{document}

