summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-19 20:15:49 +0200
committerErin van der Veen2018-04-19 20:15:49 +0200
commit531b892a0ceea85e1bbd635950dd7daf9059e95f (patch)
tree18f0c7e8845d33f7dd9f72adca2a1563e2b977a4 /Assignment1/conversion.tex
parentMuller to LTL (diff)
parentMinor textual enhancements; remove outdated todos (diff)
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex6
1 files changed, 5 insertions, 1 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 5eb9dba..72624e6 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,