From 946e713c1a9df6f751538b62f6098431add67fc8 Mon Sep 17 00:00:00 2001
From: Marcin Chrzanowski <mc370754@students.mimuw.edu.pl>
Date: Thu, 14 Oct 2021 14:37:13 +0200
Subject: Add references in text

---
 mgr.tex | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'mgr.tex')

diff --git a/mgr.tex b/mgr.tex
index fd09164..d780602 100644
--- a/mgr.tex
+++ b/mgr.tex
@@ -78,12 +78,14 @@ might not always be feasible or desirable.
 Already model checking is known to be computationally difficult for various
 interesting logics, but the situation can improve when restricting the class of
 structures considered. For example, MSO model checking is NP-hard in general,
-but Courcelle showed that deciding if an MSO sentence holds in a structure of
-bounded treewidth can be done in time linear in the size of the structure.  % TODO: referencja do Courcella
+but \textcite{courcelle1990} showed that deciding if an MSO sentence holds in a
+structure of bounded treewidth can be done in time linear in the size of the
+structure.
 
 Similarly, query evaluation of MSO queries on bounded treewidth structures was
-shown to be polynomial in the size of the structure and the output by Courcelle
-and Mosbah. Their result was improved by Frick, Flum, and Grohe to linear time.
+shown to be polynomial in the size of the structure and the output by
+\textcite{courcelle1992}. Their result was improved by \textcite{flum2001} to
+linear time.
 
 In this work, instead of evaluation, we will instead consider \definedterm{query
 answering}. In this setting, we are insterested in alrogithms that first
@@ -161,8 +163,8 @@ being output. \textcite{bagan2006} introduced this second notion and showed that
 enumerating MSO queries is \lineardelaylin\ on trees. This in particular means
 that enumerating MSO queries for formulae whose free variables are all first
 order is in \constantdelaylin, and \textcite{kazana2013} revisit this result,
-proving it using Colcombet's deterministic factorization forests rather than
-Bagan's intricate indexing structure.
+proving it using deterministic factorization forests due to \textcite{colcombet}
+rather than Bagan's intricate indexing structure.
 
 Colcombet's result could likely be used to solve the problem of branch infix
 regular queries, which we introduce as a subproblem of MSO query answering in
-- 
cgit v1.2.3

