Additional typo fixes

documentation/linter.tex

@@ -53,6 +53,8 @@
 
 \begin{document}
 
+\maketitle
+
 \section{Introduction}
 \begin{frame}{Motivation}
   \begin{itemize}
@@ -169,6 +171,7 @@ \subsection{Terminology}
   \item[NP-hard] Problem where checking a solution is fast but
     computing a solution is non-polynomial in complexity
     (e.g. $O(2^n)$)
+  \item[Undecidable] Problem that cannot be solved by any algorithm
   \item[SMT] SAT modulo theory, an extension of SAT with theories like
     integer or float arithmetic
   \item[SMT Solver] Tool to automatically solve SMT problems
@@ -179,7 +182,7 @@ \subsection{Terminology}
 \end{frame}
 
 \begin{frame}{Terminology II}
-  \begin{description}
+  \begin{description}[Under-approximate]
   \item[Sound] Reasoning that does not miss bugs (i.e. no
     false negatives)
   \item[Complete] Reasoning that does not have false alarms
@@ -765,7 +768,7 @@ \subsection{Approximating decimals}
   \item $\sqrt{2}$ is a real (but not rational, and also not a decimal)
     \pause
   \item There are things true in $\mathbb{D}$ that are not true
-    $\mathbb{R}$: $\forall x \in \mathbb{D} \mid x + \frac{1}{3} = 0$
+    $\mathbb{R}$: $\forall x \in \mathbb{D} \mid x + \frac{1}{3} \neq 0$
     \pause
   \item There are things true in $\mathbb{R}$ that are not true
     $\mathbb{D}$: $\exists x \in \mathbb{R} \mid x * x = 2$
@@ -779,8 +782,7 @@ \subsection{Approximating decimals}
     \pause
   \item Model as a pair of integers $value = \frac{a}{b}$ and say:
     \begin{itemize}
-    \item $b > 0$
-    \item $\exists n \in \mathbb{N} | b = 10^n$
+    \item $\exists n \in \mathbb{N} | n > 0 \land b = 10^n$
     \end{itemize}
     \pause
   \item This is awful because: