Mention MSO to automata theorem

1 files changed, 11 insertions, 4 deletions

diff --git a/mgr.tex b/mgr.tex
index b6c18b9..a7bb567 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -158,10 +158,17 @@ ancestor of itself; $<$ can be used to signify a strict ancestor). Note that in
 the case of MSO on trees, $\leq$ could be defined using just the edge relation
 $E$.
 
-\subsection{Query answering problems}
-d
-\section{Known algorithms we will use}
-\subsection{Least Common Ancestor}
+We make use of a fundamental theorem tying MSO logic on trees and tree automata:
+
+\begin{theorem}
+    For every MSO formula $\varphi$ over trees, there exists a tree automaton
+    $A$ such that for every tree $T$, $T \models \varphi$ if, and only if $T \in
+    L(A)$.
+\end{theorem}
+
+We note that the converse of this theorem is also true (i.e. that for every tree
+automaton, there is a corresponding MSO formula), however we will use only the
+MSO to automata direction in this work.
 
 \queryproblem{%
     Least Common Ancestor (LCA) Queries