summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-19 18:33:07 +0200
committerCamil Staps2018-04-19 18:33:07 +0200
commit3d377ca8fbe6492f5b1faf38c09160939e36d711 (patch)
treeb9f2316bff823b8c42518ff6d106f548e153acc7 /Assignment1/conversion.tex
parentLalala (diff)
Example for satisfaction by words; still needed: satisfaction by TS (and equivalence)
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 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,