%% General definitions
\documentclass{article} %% Determines the general format.
\usepackage{a4wide} %% paper size: A4.
\usepackage[utf8]{inputenc} %% This file is written in UTF-8.
%% Some editors on Windows cannot save files in UTF-8.
%% If there is a problem with special characters not showing up
%% correctly, try switching "utf8" to "latin1" (ISO 8859-1).
\usepackage[T1]{fontenc} %% Format of hte resulting PDF file.
\usepackage{fancyhdr} %% Package to create a header on each page.
\usepackage{lastpage} %% Used for "Page X of Y" in the header.
                      %% For this to work, you have to call pdflatex twice.
\usepackage{enumerate} %% Used to change the style of enumerations (see below).

\usepackage{amssymb} %% Definitions for math symbols.
\usepackage{amsmath} %% Definitions for math symbols.

\usepackage{tikz}  %% Pagacke to create graphics (graphs, automata, etc.)
\usetikzlibrary{automata} %% Tikz library to draw automata
\usetikzlibrary{arrows}   %% Tikz library for nicer arrow heads


%% Left side of header
\lhead{\course\\\semester\\Exercise \homeworkNumber}
%% Right side of header
\rhead{\authorname\\Page \thepage\ of \pageref{LastPage}}
%% Height of header
\usepackage[headheight=36pt]{geometry}
%% Page style that uses the header
\pagestyle{fancy}

\newcommand{\authorname}{A. Student}
\newcommand{\semester}{Spring semester 2015}
\newcommand{\course}{Theory of Computer Science}
\newcommand{\homeworkNumber}{1}


\begin{document}

\section*{Creating \LaTeX\ exercise submissions}

You will find many different online tutorials on how to set up a \LaTeX\ environment and compile files like this one.
For example:
\begin{itemize}
    \item \small\texttt{http://en.wikibooks.org/wiki/LaTeX/Installation} (english)
    \item \small\texttt{https://www.dpg-physik.de/dpg/gliederung/junge/rg/wuerzburg/LaTeX-InstallationsTutorial.pdf}
    (german)
\end{itemize}
Please ask the tutors if you have any problems with or questions about this.

The following solutions show how to use some commands you will need for
the exercises and demonstrate the level of detail a complete solution
should ideally have.

\section*{Aufgabe 1.1}

Atomic propositions: ItsRaining, ItsCold, TheSunIsShining,
BobWantsIceCream.

%% You can use "enumerate" to create enumerated lists.
%% The default style is to number the lists in Arabic numerals but we
%% want to use the style from the exercise sheet and explicitly set
%% the style in brackets. This is the reason we loaded the package
%% "enumerate" above.
\begin{enumerate}[(a)]
    %% Text between to dollar signs is in the so-called math mode.
    %% This mode is used to set formulas and equations and a lot of math
    %% symbols only work in math mode.
    %% Letters have a different layout in math mode: single letters are
    %% for example treated as variables. If we write "$ItsRaining$",
    %% the result looks strange because we tell LaTeX to create a layout
    %% for variables "I", "t", "s", "R", and so on (like in a
    %% multiplication).
    %% To avoid this, we use the command "\text{...}" to set regular
    %% text inside math mode.
    \item $(\lnot\text{ItsRaining} \rightarrow (\lnot\text{ItsCold}
            \land \text{TheSunIsShining}))$
    \item $((\lnot\text{ItsRaining}\lor\text{TheSunIsShining})
            \leftrightarrow \text{BobWantsIceCream})$
\end{enumerate}

\section*{Aufgabe 1.2}
\begin{enumerate}[(a)]
    \item Since $\mathcal I(A) = 0$, we know that $\mathcal
      I\not\models A$ and using the semantic of conjunctions
      that $\mathcal I\not\models (A\land B)$.
      This means that $\mathcal I\models \lnot(A\land B)$ (*).
      Replacing the abbreviation of the implication, we get $\phi \equiv
      (\lnot(A\land B)\lor C)$. Using the semantic of disjunctions
      with (*), we conclude that $\mathcal I\models \phi$.

      Alternatively, we can do a systematic proof:
      %% Text between \begin{align*} and \end{align*} contains multiple
      %% lines separated by "\\" and aligned at the "&" symbol.
      %% The Text in this environment is automatically in math mode,
      %% which means we have to use "\text{...}" again to correctly
      %% display regular text.
      \begin{align*}
        \mathcal I\models((A\land B)\rightarrow C)
        &\text{ iff.\ }\mathcal I\models(\lnot(A\land B)\lor C)\\
        &\text{ iff.\ }\mathcal I\models\lnot(A\land B)
                        \text{ or }\mathcal I\models C\\
        &\text{ iff.\ }[\text{not }\mathcal I\models(A\land B)]
                        \text{ or }\mathcal I\models C\\
        &\text{ iff.\ }[\text{not } [\mathcal I\models A
                                \text{ and }\mathcal I\models B]]
                        \text{ or }\mathcal I\models C\\
        &\text{ iff.\ }[\text{not } [\mathcal I(A) = 1
                                \text{ and }\mathcal I(B) = 1]]
                        \text{ or }\mathcal I\models C\\
        &\text{ iff.\ }[\text{not
                         \textless false statement \textgreater}]
                         \text{ or }\mathcal I\models C\\
        &\text{ iff.\ }\text{\textless true statement\textgreater\
                        or }\mathcal I\models C\\
        &\text{ iff.\ }\text{\textless true statement\textgreater}
      \end{align*}

    \item Replacing the abbreviation of the biimplication, we get
      %% Another option the change to math mode is "\[...\]".
      %% This sets a single line in math mode which will be centered in
      %% a separate paragraph. This is done for important formula that
      %% should be emphasized over the regular text.
      \[\phi \equiv ((A\rightarrow (B\lor C)) \land ((B\lor C)\rightarrow A)).\]
      We consider $\phi_1 = (A\rightarrow (B\lor C))$ and
      $\phi_2 = ((B\lor C)\rightarrow A)$ separately for now.

      We start with $\phi_1$. Replacing the abbreviation for implication,
      shows $\phi_1 \equiv (\lnot A\lor (B\lor C))$. Since
      $\mathcal I(C) = 1$, we know that $\mathcal I\models C$ and using
      the semantic for disjunctions $\mathcal I\models (B\lor C)$, as well.
      This shows (again with the semantic for disjunctions)
      $\mathcal I\models\phi_1$ (*).

      Removing the abbreviation for the implication in $\phi_2$, we get $\phi_2 \equiv (\lnot(B\lor
      C)\lor A)$. Since $\mathcal I(A) = 1$, we know that $\mathcal I\models A$, which directly shows with the
      semantic for disjunctions that $\mathcal I\models \phi_2$ (**).

      The results (*) and (**) show $\mathcal I\models \phi$ with the semantic for conjunctions.

      Of course we could also have done a systematic proof here, but this would have been more complicated.
\end{enumerate}


\section*{Aufgabe 1.3}
\begin{enumerate}[(a)]
  \item Truth table for $\phi$:

    \begin{tabular}{rr|ccc}
    $\mathcal I(A)$ & $\mathcal I(B)$ & $\mathcal I\models (A\rightarrow B)$ &
    $\mathcal I\models (B\rightarrow A)$
    &$\mathcal I\models ((A\rightarrow B) \lor (B\rightarrow A))$\\\hline
    $0$ & $0$ & Yes & Yes & Yes\\
    $0$ & $1$ & Yes & No & Yes\\
    $1$ & $0$ & No & Yes & Yes\\
    $1$ & $1$ & Yes & Yes & Yes
    \end{tabular}
    \bigskip

    Since the result for all interpretations is ``Yes'', the formula $\phi$
    is a tautology and thus also satisfiable. For the same reason it is not
    falsifiable and thus also not unsatisfiable.
  \item The formula is satisfiable which can be seen for the interpretation
    $\mathcal I = \{A\mapsto 1,B\mapsto 0, C\mapsto 1, D\mapsto 1\}$:
    Since $\mathcal I(A) = 1$, we know that $\mathcal I\models A$ and with the semantic
    for disjunctions $\mathcal I\models (A\lor B)$. With $\mathcal I(C)=1$ we can
    argue analogously that $\mathcal I\models (C\lor D)$. Together with the
    semantic for conjunctions we conclude that $\mathcal I\models\psi$.

    From satisfiability we can directly conclude that $\psi$ is not
    unsatisfiable.

    The formula $\psi$ is also falsifiable, which the
    interpretation $\mathcal I' = \{A\mapsto 0,B\mapsto 0, C\mapsto 1, D\mapsto 1\}$
    shows: Since $\mathcal I'(A)=0$ and $\mathcal I'(B) = 0$, we know that $\mathcal
    I'\not\models (A\lor B)$. So $\mathcal I'$ cannot be a model of the conjunction $\psi$.

    Since $\psi$ is falsifiable, it cannot be a tautology.
\end{enumerate}

\section*{Aufgabe 1.4}
Example automaton:
      %% Options:
      %% "->": edges are directed
      %% ">=stealth'": better arrow heads (uses \usetikzlibrary{arrows})
      %% "auto": automatic location of edge labels
      %% "node distance=3cm": distance between nodes with relative positioning
      %%
      %% Styles: (uses \usetikzlibrary{automata})
      %% "state": use with every state of the automaton
      %% "accepting": use with accepting states
      %% "initial above": initial state with incoming arrow from above
      %% "initial text=": no text above the arrow that points to the initial state
      %%
      %% Relative node positioning:
      %% left of, right of, below of, above of
      %%
      %% Edge positioning:
      %% (no options): direct connection
      %% "loop right": edge from a node to itself (to the right of the node)
      %% "bend left": curved edge to the left
      %% "swap": edge label on the other side


      \begin{tikzpicture}[->,>=stealth',auto,node distance=3cm]
          \node[initial above, initial text=, state] (q0) {$z_0$};
          \node[state]            (q1) [left of=q0] {$z_1$};
          \node[state,accepting]  (q2) [right of=q0] {$z_2$};

          \path (q0) edge node {$0$} (q1)
                (q0) edge[ loop right] node {$1$} (q0)
                (q1) edge[ bend right] node[swap] {$0$} (q2)
                (q1) edge[ bend left] node {$1$} (q0)
                (q2) edge[ loop above] node [swap] {$0$} (q2)
                (q2) edge[ bend right] node [swap] {$1$} (q0);
      \end{tikzpicture}
\end{document}