3 files changed, 21 insertions, 19 deletions
diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex
index a1ecad2..dc3e2d4 100644
--- a/chapters/background/01-neural-networks.tex
+++ b/chapters/background/01-neural-networks.tex
@@ -2,8 +2,8 @@
 \label{sec:neural-networks}
 
 A neural network is a computational model inspired by biological neural networks. It consists of
-connected nodes called neuron, introduced in its early form by Rosenblatt~\cite{rosenblatt1958perceptron}.
-\textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using
+connected nodes called neurons, introduced in its early form by Rosenblatt~\cite{rosenblatt1958perceptron}.
+The \textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using
 backpropagation as popularized by Rumelhart et al.~\cite{rumelhart1986learning}.
 
 \subsection{Neuron}
@@ -51,7 +51,7 @@ The output $y$ is defined as:
         \draw[->] (act) -- (y);
         
     \end{tikzpicture}
-    \caption{Mathematical model of an artificial neuron.}
+    \caption{Graphical representation of a neuron.}
     \label{fig:single-neuron}
 \end{figure}
 
@@ -101,14 +101,15 @@ the outputs.
         \node[above] at (7, 1.2) {Output Layer};
         
     \end{tikzpicture}
-    \caption{Architecture of a Multi-Layer Perceptron (MLP) with one hidden layer.}
+    \caption{Architecture of an MLP with one hidden layer.}
     \label{fig:mlp}
 \end{figure}
 
-One of the most common activation function is the ReLU, defined as:
+One of the most common activation functions is the ReLU, defined as:
 \begin{equation}
     \text{ReLU}(z) = \max(0, z)
 \end{equation}
+The framework focuses on MLP with ReLU activation functions.
 
 \subsection{Neural Network Verification}
 The verification problem of a neural network $F: \mathbb{R}^n \to \mathbb{R}^m$ with input constraint
diff --git a/chapters/background/02-interaction-nets.tex b/chapters/background/02-interaction-nets.tex
index 36a7a32..874110e 100644
--- a/chapters/background/02-interaction-nets.tex
+++ b/chapters/background/02-interaction-nets.tex
@@ -1,11 +1,11 @@
 \section{Interaction Nets}
 \label{sec:interaction-nets}
 
-Interaction Nets, introduced by Yves Lafont et al.~\cite{lafont1990interactionnets}, are a
+\textit{Interaction Nets} (IN), introduced by Lafont~\cite{lafont1990interactionnets}, are a
 graphical model of computation based on graph rewriting.
 
 \subsection{Basic Concepts}
-An interaction net is an undirected graph with labelled vertices, called \textit{agents}. Each agent
+An IN is an undirected graph with labelled vertices, called \textit{agents}. Each agent
 is an instance of a \textit{symbol}, which has a principal port and a fixed number of auxiliary ports:
 \begin{figure}[H]
 	\centering
@@ -16,11 +16,12 @@ is an instance of a \textit{symbol}, which has a principal port and a fixed numb
 		\node[left] at (A.above pax 2) {$\mathit{y}$};
 		\node[right] at (A.above pal) {$\mathit{x}$};
 	\end{tikzpicture}
-	\caption{Example of an agent \textit{Add} with two auxiliary ports.}
+	\caption{Example of an agent \textit{Add} with two auxiliary ports connected to $x, y, z$ wires.}
 	\label{fig:agent}
 \end{figure}
 
-Each port can be wired to at most one other port. When two different agents are wired to their respective principal ports they are called an \textit{active pair}:
+Each port can be wired to at most one other port. When two different agents are wired to their
+respective principal ports they are called an \textit{active pair}:
 
 \begin{figure}[H]
 	\centering
@@ -38,8 +39,8 @@ Each port can be wired to at most one other port. When two different agents are
 \end{figure}
 
 \subsection{Interaction Rules}
-Computation in interaction nets proceeds by rewriting the net using local \emph{interaction rules}. A rule
-is defined only for an active pair and, for any pair of agent types, there is at most one
+Computation in IN proceeds by rewriting the net using local \emph{interaction rules}. A rule
+is defined only for an active pair and for any pair of symbols there is at most one
 interaction rule.
 
 \begin{figure}[H]
@@ -66,10 +67,11 @@ interaction rule.
 \end{figure}
 
 \subsection{Properties}
-Interaction nets possess the following properties:
+IN possess the following properties:
 \begin{itemize}
 	\item \textbf{Locality}: only active pairs can be rewritten.
-	\item \textbf{Linearity}: each interaction rule can be applied in constant time.
+	\item \textbf{Linearity}: each interaction rule rewrites a constant-size subgraph, independent of
+		the overall size of the net.
 	\item \textbf{Strong Confluence}: given a net $\text{IN}$ that can reduce to $\text{IN}_1$ and $\text{IN}_2$ in one
 		step, then both $\text{IN}_1$ and $\text{IN}_2$ reduce to some net $\text{IN}'$ in one step.
 \end{itemize}
diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex
index a55d54d..80e9932 100644
--- a/chapters/background/03-satisfiability-modulo-theories.tex
+++ b/chapters/background/03-satisfiability-modulo-theories.tex
@@ -1,7 +1,7 @@
 \section{Satisfiability Modulo Theories}
 \label{sec:satisfiability-modulo-theories}
 
-Satisfiability Modulo Theories (SMT) is the problem of determining whether a mathematical formula is
+\textit{Satisfiability Modulo Theories} (SMT) is the problem of determining whether a mathematical formula is
 satisfiable within a certain formal theory in first-order logic. Barrett et al.~\cite{barrett2016smtlib}
 defined the SMT-LIB standard for input format and theory definitions.
 
@@ -11,14 +11,13 @@ multiplication by constants, and equality/inequality relations:
 \begin{equation}
     \phi ::= t_1 \sim t_2 \mid \phi_1 \lor \phi_2 \mid \phi_1 \land \phi_2 \mid \neg \phi_1
 \end{equation}
-where $t_1, t_2$ are linear terms of the form $c_1 x_1 + \dots + c_k x_k + c_0$ (with $c_i \in \mathbb{R}$ and $x_i$ being real
+where $t_1, t_2$ are linear terms of the form $c_1 \cdot x_1 + \dots + c_k \cdot x_k + c_0$ (with $c_i \in \mathbb{R}$ and $x_i$ being real
 variables), and $\sim \;\in \{=, \le, <, \ge, >\}$.
 
 To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disjunction:
 \begin{equation}
     (x > 0 \land y = x) \lor (x \le 0 \land y = 0)
 \end{equation}
-For a network with $N$ ReLU neurons, there are up to $2^N$ possible activation patterns. Solving the
-verification property requires the SMT solver, such as Z3 presented by De Moura et al.~\cite{demoura2008z3},
-to implicitly explore this branching search space.
-
+For a network with $n$ ReLU neurons, there are up to $2^n$ possible activation patterns. Solving the
+verification problem requires the SMT solver, such as Z3 presented by De Moura et
+al.~\cite{demoura2008z3}, to implicitly explore this branching search space.