Example for satisfaction by words; still needed: satisfaction by TS (and equivalence)

1 files changed, 5 insertions, 1 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 5b97530..e474f74 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -20,7 +20,11 @@ The syntactic algorithm as proposed by Gabbay has its foundation in the followin
 		For this paragraph we will use Gabbay's definitions.}
 \begin{enumerate}
 	\item Every PLTL formula can be written using no other temporal operators than $\Sop$ and $\Uop$ operators.
-	\item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.
+	\item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.%
+		\footnote{%
+			This is known as the Separation Theorem.
+			It was originally proven by \citet{Gabbay1980}.
+			Folklore has it that when Hans Kamp, a philosopher working on temporal logics, heard of the result, he went out and bought Gabbay a cake (\url{https://cstheory.stackexchange.com/a/29452}, retrieved April 19, 2018).}
 	\item The same formula without past modalities $\psi$, a boolean combination of $\wfff \cup \wffn$, is initially equivalent to $\phi$.
 \end{enumerate}
 When these facts are considered in sequence,