%% Allgemeine Definitionen
\documentclass{article} %% Bestimmt die allgemeine Formatierung der Abgabe.
\usepackage{a4wide} %% Papierformat: A4.
\usepackage[utf8]{inputenc} %% Datei wird im UTF-8 Format geschrieben.
%% Unter Windows werden Dateien je nach Editor nicht in diesem Format
%% gespeichert und Umlaute werden dann nicht richtig erkannt.
%% Versucht in diesem Fall "utf8" auf "latin1" (ISO 8859-1) wechseln.
\usepackage[T1]{fontenc} %% Format der Zeichen im erstellten PDF.
\usepackage[nswissgerman]{babel} %% Regeln für automatische Worttrennung.
\usepackage{fancyhdr} %% Paket um einen Header auf jeder Seite zu erstellen.
\usepackage{lastpage} %% Wird für "Seite X von Y" im Header benötigt.
                      %% Damit das funktioniert, muss pdflatex zweimal
                      %% aufgerufen werden.
\usepackage{enumerate} %% Hiermit kann der Stil der Aufzählungen
                       %% verändert werden (siehe unten).

\usepackage{amssymb} %% Definitionen für mathematische Symbole.
\usepackage{amsmath} %% Definitionen für mathematische Symbole.

\usepackage{tikz}  %% Paket für Grafiken (Graphen, Automaten, etc.)
\usetikzlibrary{automata} %% Tikz-Bibliothek für Automaten
\usetikzlibrary{arrows}   %% Tikz-Bibliothek für Pfeilspitzen


%% Linke Seite des Headers
\lhead{\course\\\semester\\Übungsblatt \homeworkNumber}
%% Rechte Seite des Headers
\rhead{\authorname\\Seite \thepage\ von \pageref{LastPage}}
%% Höhe des Headers
\usepackage[headheight=36pt]{geometry}
%% Seitenstil, der den Header verwendet.
\pagestyle{fancy}

\newcommand{\authorname}{A. Student\\Another Student}
\newcommand{\semester}{Frühjahrssemester 2017}
\newcommand{\course}{Theorie der Informatik}
\newcommand{\homeworkNumber}{1}


\begin{document}

\section*{Abgaben mit \LaTeX\ erstellen}

Im Netz finden Sie viele Anleitungen zum Einrichten einer \LaTeX\ Umgebung und zum Kompilieren von Dateien wie dieser.
Zum Beispiel:
\begin{itemize}
    \item \small\texttt{https://www.dpg-physik.de/dpg/gliederung/junge/rg/wuerzburg/LaTeX-InstallationsTutorial.pdf}
    \item \small\texttt{http://en.wikibooks.org/wiki/LaTeX/Installation}
\end{itemize}
Bei Problemen und Fragen wenden Sie sich bitte an die Tutoren.

Die folgenden Lösungen zeigen, wie einige der Befehle verwendet werden,
die Sie für die Lösungen brauchen werden, und wieviel Details eine
vollständige Lösung idealerweise haben sollte.

\section*{Aufgabe 1.1}

Atomare Aussagen: EsRegnet, EsIstKalt, DieSonneScheint,
BobHatLustAufEis.

%% Mit enumerate können Aufzählungen gemacht werden.
%% Die Standardeinstellung ist die Aufzählung zu nummerieren, wir
%% wollen aber die Einstellungen aus dem Aufgabenblatt übernehmen
%% und geben den Stil in eckigen Klammern an. Dazu haben wir oben das
%% Paket "enumerate" geladen.
\begin{enumerate}[(a)]
    %% Text zwischen zwei Dollarzeichen ist im sogenannten Mathemodus.
    %% In diesem Modus werden Formeln und Gleichungen gesetzt und viele
    %% mathematische Symbole funktionieren nur im Mathemodus.
    %% Im Mathemodus werden Zeichen anders gesetzt, zum Beispiel werden
    %% einzelne Buchstaben im Mathemodus als Variablen behandelt.
    %% Wenn wir "$EsRegnet$" schreiben, sieht das komisch aus, weil
    %% wir damit latex sagen es soll die Variablen "E", "s", "R", usw.
    %% hintereinanderschreiben (wie in einer Multiplikation).
    %% Wir verwenden daher den Befehl "\text{...}" um Text im Mathemodus
    %% wieder als normalen Text zu behandeln.
    \item $(\lnot\text{EsRegnet} \rightarrow (\lnot\text{EsIstKalt}
            \land \text{DieSonneScheint}))$
    \item $((\lnot\text{EsRegnet}\lor\text{DieSonneScheint})
            \leftrightarrow \text{BobHatLustAufEis})$
\end{enumerate}


\clearpage

\section*{Aufgabe 1.2}
\begin{enumerate}[(a)]
    \item Da $\mathcal I(A) = 0$, gilt $\mathcal
      I\not\models A$ und damit mit der Semantik für Konjunktionen
      auch $\mathcal I\not\models (A\land B)$. Daraus folgt, dass
      $\mathcal I\models \lnot(A\land B)$ (*). Löst man die
      Abkürzung der Implikation auf, erhält man $\phi \equiv
      (\lnot(A\land B)\lor C)$.  Aus der Semantik für
      Disjunktionen folgt mit (*) direkt, dass $\mathcal I\models
      \phi$.

      Oder alternativ mit einem systematischeren Beweis:
      %% Text zwischen \begin{align*} und \end{align*} enthält mehrere
      %% Zeilen die durch "\\" getrennt werden und an dem Zeichen "&"
      %% ausgerichtet werden.
      %% Der Text in dieser Umgebung ist automatisch im Mathemodus, d.h.
      %% um Text richtig darzustellen, müssen wir wieder "\text{...}"
      %% verwenden.
      \begin{align*}
        \mathcal I\models((A\land B)\rightarrow C)
        &\text{ gdw.\ }\mathcal I\models(\lnot(A\land B)\lor C)\\
        &\text{ gdw.\ }\mathcal I\models\lnot(A\land B)
                        \text{ oder }\mathcal I\models C\\
        &\text{ gdw.\ }[\text{nicht }\mathcal I\models(A\land B)]
                        \text{ oder }\mathcal I\models C\\
        &\text{ gdw.\ }[\text{nicht } [\mathcal I\models A
                                \text{ und }\mathcal I\models B]]
                        \text{ oder }\mathcal I\models C\\
        &\text{ gdw.\ }[\text{nicht } [\mathcal I(A) = 1
                                \text{ und }\mathcal I(B) = 1]]
                        \text{ oder }\mathcal I\models C\\
        &\text{ gdw.\ }[\text{nicht
                         \textless falsche Aussage\textgreater}]
                         \text{ oder }\mathcal I\models C\\
        &\text{ gdw.\ }\text{\textless wahre Aussage\textgreater\
                        oder }\mathcal I\models C\\
        &\text{ gdw.\ }\text{\textless wahre Aussage\textgreater}
      \end{align*}

    \item Löst man die Abkürzung des Bikonditionals auf, erhält man
      %% Eine andere Möglichkeit in den Mathemodus zu wechseln ist "\[...\]".
      %% Damit wird eine einzelne Zeile in den Mathemodus gesetzt und kommt
      %% in einen eigenen Absatz. Das macht man für wichtigere Formeln,
      %% die man vom normalen Text etwas abheben will.
      \[\phi \equiv ((A\rightarrow (B\lor C)) \land ((B\lor C)\rightarrow A)).\]
      Wir betrachten $\phi_1 = (A\rightarrow (B\lor C))$ und
      $\phi_2 = ((B\lor C)\rightarrow A)$ zunächst getrennt.

      Wir beginnen mit $\phi_1$. Löst man die Implikation auf,
      ergibt sich $\phi_1 \equiv (\lnot A\lor (B\lor C))$. Da
      $\mathcal I(C) = 1$, gilt $\mathcal I\models C$ und damit wegen
      der Semantik für Disjunktionen auch $\mathcal I\models (B\lor C)$.
      Das ergibt (wiederum mit der Semantik für Disjunktionen)
      $\mathcal I\models\phi_1$ (*).

      Löst man die Implikation in $\phi_2$ auf, erhält man $\phi_2 \equiv (\lnot(B\lor
      C)\lor A)$. Da $\mathcal I(A) = 1$, gilt $\mathcal I\models A$, was mit der
      Semantik für Disjunktionen direkt ergibt, dass $\mathcal I\models \phi_2$ (**).

      Die Zwischenergebnis (*) und (**) ergeben mit der Semantik für Konjunktionen,
      dass $\mathcal I\models \phi$.

      Natürlich könnten wir auch hier wieder alternativ einen systematischen Beweis
      machen, das würde allerdings recht unübersichtlich.
\end{enumerate}


\clearpage

\section*{Aufgabe 1.3}
\begin{enumerate}[(a)]
  \item Wahrheitstafel für $\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$ & Ja & Ja & Ja\\
    $0$ & $1$ & Ja & Nein & Ja\\
    $1$ & $0$ & Nein & Ja & Ja\\
    $1$ & $1$ & Ja & Ja & Ja
    \end{tabular}
    \bigskip

    Da das Ergebnis für alle Interpretation "`Ja"' ist, ist die Formel $\phi$ eine
    Tautologie und damit auch erfüllbar. Sie ist aus dem gleichen Grund nicht
    falsifizierbar und damit auch nicht unerfüllbar.
  \item Die Formel ist erfüllbar, was man zum Beispiel aus der Interpretation
    $\mathcal I = \{A\mapsto 1,B\mapsto 0, C\mapsto 1, D\mapsto 1\}$ erkennen
    kann: Da $\mathcal I(A) = 1$, gilt $\mathcal I\models A$ und mit der Semantik
    für Disjunktionen $\mathcal I\models (A\lor B)$. Mit $\mathcal I(C)=1$ kann
    man analog argumentieren, dass $\mathcal I\models (C\lor D)$. Zusammen folgt
    mit der Semantik für Konjunktionen, dass $\mathcal I\models\psi$.

    Aus der Erfüllbarkeit können wir direkt schliessen, dass $\psi$ nicht
    unerfüllbar ist.

    Die Formel $\psi$ ist ausserdem falsifizierbar, was wir mit der
    Interpretation $\mathcal I' = \{A\mapsto 0,B\mapsto 0, C\mapsto 1, D\mapsto 1\}$
    zeigen: Da $\mathcal I'(A)=0$ und $\mathcal I'(B) = 0$, gilt $\mathcal
    I'\not\models (A\lor B)$. Damit kann $\mathcal I'$ auch kein Modell der
    Konjunktion $\psi$ sein.

    Da $\psi$ falsifizierbar ist, kann die Formel keine Tautologie sein.
\end{enumerate}

\clearpage

\section*{Aufgabe 1.4}
Beispiel für einen Automaten:
      %% Optionen:
      %% "->": Kanten sind gerichtet
      %% ">=stealth'": Bessere Pfeilspitzen (braucht \usetikzlibrary{arrows})
      %% "auto": Automatische Anordnung der Kantenbeschriftungen
      %% "node distance=3cm": Abstand der Knoten bei relativer Anordnung
      %%
      %% Styles: (braucht \usetikzlibrary{automata})
      %% "state": Bei jedem Zustand mit angeben
      %% "accepting": Akzeptierender Zustand
      %% "initial above": Startzustand mit Pfeil von oben
      %% "initial text=": Kein Text ueber dem Pfeil auf den Startzustand
      %%
      %% Knotenanordnung:
      %% left of, right of, below of, above of
      %%
      %% Kantenanordnung:
      %% (ohne Optionen): direkte Verbindung
      %% "loop right": Kante von einem Knoten auf sich selbst (rechts neben dem Knoten)
      %% "bend left": Kante mit Linkskurve
      %% "swap": Kantenbeschriftung auf die andere Seite


      \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}
