From d8637ef9adee6a033e311ba2b71ad9a6089149a2 Mon Sep 17 00:00:00 2001
From: Marcin Chrzanowski <mc370754@students.mimuw.edu.pl>
Date: Mon, 9 Aug 2021 20:49:20 -0400
Subject: Mention MSO to automata theorem

---
 mgr.tex | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'mgr.tex')

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
-- 
cgit v1.2.3