diff options
author | Camil Staps | 2018-04-19 18:33:07 +0200 |
---|---|---|
committer | Camil Staps | 2018-04-19 18:33:07 +0200 |
commit | 3d377ca8fbe6492f5b1faf38c09160939e36d711 (patch) | |
tree | b9f2316bff823b8c42518ff6d106f548e153acc7 /Assignment1/conversion.tex | |
parent | Lalala (diff) |
Example for satisfaction by words; still needed: satisfaction by TS (and equivalence)
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 6 |
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, |