\input{../settings/settings}
\usepackage{amssymb}%
\usepackage{MnSymbol}%
%\usepackage{wasysym}%

\begin{document}

	\klausur{Gdl-SaV-B (Logik)}
		{Prof. M. Mendler, Ph. D.}
		{Wintersemester 16/17}
		{90}
		{Wörterbuch (Englisch-Deutsch/Deutsch-Englisch)}

	\newpage

	\begin{center}
		\begin{tabular}{|c|c|c|c|c|c|c|c|}
			\hline 
			\textbf{(Sub-)Question} & 1 & 2a & 2b & 3a & 3b & 4a & 4b \\ 
			\hline 
			\textbf{Available Marks} & 12 & 12 & 20 & 10 & 12 & 8 & 16 \\ 
			\hline 
			$\Sigma$ &   &   &   &   &   &   &   \\ 
			\hline
		\end{tabular}
	\end{center}
 	
 	\newpage
	
	\textbf{Syntax}
	\begin{enumerate}
		\item Consider the formulas $\phi$ and $\psi$ defined as follows:
		
		$$ \phi =_{def} (P \supset \square R ) \wedge \neg P $$
		$$ \psi =_{def} S \wedge \neg \diamondsuit Q $$
		
		Use the Martelli-Montanari Algorithm (the algorithm is given in Apeendix I) to check whether there is a \textit{most general unifier} $\theta$ for $\phi$ and $\psi$, i.e., a solution for the unification problem $ E = \{\phi = \psi\}$. In case there is such a unifier, state it.
		
		Make clear how you obtain your results by providing \textbf{every single transformation step} of the algorithm, specifyfing the corresponding number of the rule which you apply.
		
		\textbf{Hilbert and Tableau Calculus}
		\item
		\begin{enumerate}
				\item With the model axiom $\Gamma = \{A\}$, find a suitable Hilbert deduction in the modal KD such that $$ KD;\Gamma;\vdash_{H} \lozenge(A \vee C).$$
				In other words: prove that $\lozenge(A \vee C)$ holds if $A$ holds, using the modal Hilbert Calculus with the axiom schmees from KD.\\
				For this, you need (beside your model axiom) the following:
				\begin{itemize}
					\item the rule of \textit{Modus Ponens,}
					\item the rule of \textit{Necessitation,}
					\item the propositional axiom scheme: $P \supset (P \vee Q),$
					\item the modal axiom scheme (D): $\square P \supset \lozenge P$.
				\end{itemize}
				\textbf{Hint:} You may need to instantiate the variables $P$ and $Q$ of the axiom schemes appropriately to perform the proof.
				\item Consider the formula $\phi$ given as
				$$ ((\lozenge \square P) \wedge \lozenge Q \supset \square (P \wedge \lozenge Q). $$
				Using the S5 tableau calculus (see Appendix II) show that $\phi$ is valid in all S5-frames.
		\end{enumerate}
		 
		 \item A traffic light can have four different states: \textit{red, red/yellow, green} and \textit{yellow}. In a working traffic light, these states change in the indicated order.
		 Consider the set $Var =_{def} \{RED, YELLOW, GREEN\}$ of propositional variables with the following meanings:
		 \begin{center}
			 \begin{tabular}{|l|l|}
				 \hline 
				 \textbf{Variable} & \textbf{Meaning} \\ 
				 \hline
				 \hline
				 $RED$ & \textit{The red light is on.} \\ 
				 \hline 
				 $YELLOW$ & \textit{The yellow light is on.} \\ 
				 \hline 
				 $GREEN$ & \textit{The green light is on.} \\ 
				 \hline 
			\end{tabular}
		 \end{center}
		 
		 In the \textit{red/yellow}, both $RED$ and $YELLOW$ hold.
		 
		 \begin{enumerate}
		 	\item Some broken traffic light has a malfunction and satisties the \textit{Propositional Temporal Logic (PLTL)} formula $\psi$ defined thus:
		 	$$ \psi =_{def} \diamondsuit RED \wedge \square (RED \supset X RED) $$
		 	
		 	Draw a time-line representing a model $(\mathcal{T},V)$ with at least one world $t$ where $\psi$ holds.
		 	
		 	\textbf{Explain in detail} the properties of your model, which enforce that $\mathcal{T},V,t \models \psi$ and how they enforce it.
		 	\item Find a formula of PLTL that expresses the following statement:
		 	\begin{quote}
		 		\textit{Whenever the light is red, it becomes green eventually after being red/yellow for some time (i.e., red/yellow at least for one time instance).}
		 		
		 		Note that between states \textit{red} and \textit{green}, \textbf{only} \textit{red/yellow} is permitted.
		 	\end{quote}
		 \end{enumerate}
		 
		 \textbf{Semantics and Correspondence Theory}
		 
		 \item
		 \begin{enumerate}
		 	\item Consider a mono-modal frame $\mathcal{F}_{1} = (W_{1} \rightarrow_{1})$ with $W_{1} =_{def} \{w_{1},w_{2},w_{3},w_{4}\}$and $\rightarrow_{1}$ as indicated in the following figure. 

			\image{0.5}{fig1.PNG}{}{}

			Copy the transition system of $\mathcal{F}_{1}$ to your exam answer paper and add further transitions to obtain an extended frame $\mathcal{F}_{2} = (W_{1},\rightarrow)$ such that the \textbf{frame axiom (5)} holds, i.e., such that $\mathcal{F}_{2} \models \lozenge P \supset \square \lozenge P.$ Add only a minimal amount of transitions that is necessary to make the statement become true. Do not remove any transition and do not change $W_{1}$!
			
			\item 			
			Prove formally that in \textbf{all} frames $\mathcal{F}$ (not only in $\mathcal{F}_{1}$ or $\mathcal{F}_{2}$) it holds:
			$$ \mathcal{F} \models \square (P \supset Q) \supset (\square P \supset \square Q). $$
			Do this by arguing on the formal semantics of normal modal logics. In other words prove			
			$$ \mathcal{F},V,w \models \square (P \supset Q) \supset (\square P \supset \square Q) $$
			
			for an arbitrary frame $\mathcal{F} = (W,\rightarrow)$, valuation $V$ and world $w \in W$.
			
			Do \textbf{not} use Hilbert Calculus or a Tableau Calculus!
			
			
		 \end{enumerate}
	\end{enumerate}
\end{document}