ha01.tex

\documentclass[12pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{lmodern}

\begin{document}
\noindent
\noindent \large WiSe 24/25 \hfill
Logik

\begin{center}
\textbf{AL-Hausarbeit  Aufgabe 1}\\
\vspace*{0.5cm}
\textbf{Gruppe:} 0395694, 0471850, 234567 % Tragen Sie hier die Matrikelnummern der Mitglieder ihrer Gruppe ein.

\end{center}

\subsection*{Formel $\varphi_{K,T,P,M}$}

Sei $K$ die Menge der Kommiliton*innen, $T$ die Menge der möglichen Termine, 
$P$ die Menge der Plätzchensorten und $M \subseteq K \times P$ die Relation, 
die $(k,p)$ enthält, falls $k$ die Plätzchensorte $p$ mag.

Verwendete atomare Formeln:
\begin{itemize}
    \item $\text{eingeladen}(k,t)$: Person $k$ ist zu Termin $t$ eingeladen.
    \item $\text{ausweichtermin}(k,t)$: Termin $t$ ist ein Ausweichtermin für Person $k$.
    \item $\text{gebacken}(p,t)$: Die Plätzchensorte $p$ wird an Termin $t$ gebacken.
\end{itemize}

Wir fordern:

(i) Jede*r Kommiliton*in wird genau einem Termin zugewiesen, und es gibt mindestens einen weiteren Termin als Ausweichtermin. Außerdem soll jede*r nur einen Einladungstermin haben.

Erläuterung außerhalb der Formel:  
- Der Ausdruck $\bigvee_{t \in T}(\text{eingeladen}(k,t) \wedge \bigvee_{t' \in T\setminus\{t\}}\text{ausweichtermin}(k,t'))$ stellt sicher, dass es für jede Person $k$ genau einen Termin gibt, zu dem $k$ eingeladen ist, und mindestens einen anderen Termin als Ausweichtermin.  
- Der Ausdruck $\bigwedge_{\substack{t,t' \in T \\ t \neq t'}} \neg(\text{eingeladen}(k,t)\wedge\text{eingeladen}(k,t'))$ stellt sicher, dass es nicht zwei unterschiedliche Einladungstermine für dieselbe Person gibt.

\begin{align*}
\varphi_{K,T,P,M} := 
& \bigwedge_{k \in K}\Biggl[
   \Bigl(
     \bigvee_{t \in T}\bigl(\text{eingeladen}(k,t) \wedge \bigvee_{t' \in T\setminus\{t\}} \text{ausweichtermin}(k,t')\bigr)
   \Bigr) \\
& \qquad\wedge
   \bigwedge_{\substack{t,t' \in T \\ t \neq t'}} 
     \neg\bigl(\text{eingeladen}(k,t)\wedge \text{eingeladen}(k,t')\bigr)
\Biggr].
\end{align*}

(ii) Jede Plätzchensorte wird bei maximal einem Treffen gebacken:
\[
\bigwedge_{p \in P}\bigwedge_{\substack{t,t' \in T \\ t \neq t'}} \neg(\text{gebacken}(p,t) \wedge \text{gebacken}(p,t')).
\]

(iii) An Terminen ohne Einladungen werden keine Plätzchen gebacken, und umgekehrt:
\[
\bigwedge_{t \in T} \left( \bigvee_{k \in K}\text{eingeladen}(k,t) \;\leftrightarrow\; \bigvee_{p \in P}\text{gebacken}(p,t) \right).
\]

(iv) Wenn jemand eingeladen wird, muss diese Person alle gebackenen Plätzchensorten mögen:
\[
\bigwedge_{k \in K}\bigwedge_{t \in T}\bigl(\text{eingeladen}(k,t) \to \bigwedge_{p \in P}(\text{gebacken}(p,t) \to ((k,p)\in M))\bigr).
\]

(v) An jedem Ausweichtermin muss mindestens eine Plätzchensorte gebacken werden, die die Person mag:
\[
\bigwedge_{k \in K}\bigwedge_{t \in T}\bigl(\text{ausweichtermin}(k,t) \to \bigvee_{p \in P}(\text{gebacken}(p,t)\wedge((k,p)\in M))\bigr).
\]

\subsection*{Ergebnisse aus der Belegung ablesen}

Eine erfüllende Belegung der Formel $\varphi_{K,T,P,M}$ erlaubt die folgende Interpretation:
\begin{itemize}
    \item $\text{eingeladen}(k,t)$: $k$ wird zu $t$ eingeladen.
    \item $\text{ausweichtermin}(k,t)$: $t$ ist ein möglicher Ersatztermin für $k$.
    \item $\text{gebacken}(p,t)$: Die Plätzchensorte $p$ wird an $t$ gebacken.
\end{itemize}

Aus der erfüllenden Belegung können wir direkt entnehmen, wer zu welchem Termin eingeladen ist, welche Plätzchensorten gebacken werden und welche Termine mögliche Ersatztermine sind.

\end{document}