compile predlogic chapter

compile

@@ -104,7 +104,7 @@ compile_wrapper() {
 
 compile_chapter() {
   #for chapter in smtzthree proplogic satsolver ndpred predlogic ndpred smt bdd eqchecking symbenc temporal
-  for chapter in  smtzthree eqchecking
+  for chapter in  predlogic
   do
     set_chapter "\\chapter${chapter}true"
     compile_wrapper "$chapter" "$@"

main.tex

@@ -100,7 +100,7 @@
 \fi
 
 \ifchapterpredlogic
-  \setsectionnum{4}
+  \setsectionnum{6}
   \section{Predicate Logic}
   \input{predicate_logic/predicate_logic.tex}
   \pagebreak

predicate_logic/0001.tex

@@ -0,0 +1,10 @@
+\item \lect Model the following declarative sentences with predicate logic, as detailed as possible. Clearly indicate the intended meaning of all function, predicate, and constant symbols that you use.
+
+\begin{enumerate}
+	\item Some students like Alice.
+	\item Every teacher likes Bob.
+	\item Some students like every teacher.
+	\item Some students and Bob play a game.
+	\item Not every student plays games.
+	\item Some teachers play no games.
+\end{enumerate}

predicate_logic/0001_sol.tex

@@ -0,0 +1,23 @@
+$\mathcal{A} = \text{People}$ \\
+
+\begin{enumerate}
+	\item $\exists x \big(S(x) \land L(x, Alice)\big)$ \\
+	      $S(x) \ldots $ $x$ is a student \\
+	      $L(x, y) \ldots $ $x$ likes $y$ \\
+	\item $\forall x \big(T(x) \imp L(x, Bob)\big)$ \\
+	      $T(x) \ldots $ $x$ is a teacher \\
+	      $L(x, y) \ldots $ $x$ likes $y$ \\
+	\item $\exists x \big(S(x) \land \forall y \big(T(y) \imp L(x, y)\big) \big)$ \\
+	      $S(x) \ldots $ $x$ is a student \\
+	      $T(x) \ldots $ $x$ is a teacher \\
+	      $L(x, y) \ldots $ $x$ likes $y$ \\
+	\item $P(Bob) \land \exists x \big(S(x) \land P(x)\big)$ \\
+	      $S(x) \ldots $ $x$ is a student \\
+  	      $P(x) \ldots $ $x$ plays a game \\
+	\item $\lnot \forall x \big(S(x) \imp P(x)\big)$\\
+	      $S(x) \ldots $ $x$ is a student \\
+  	      $P(x) \ldots $ $x$ plays a game \\
+	\item $\exists x \big(T(x) \imp \lnot P(x)\big)$\\
+	      $T(x) \ldots $ $x$ is a teacher \\
+  	      $P(x) \ldots $ $x$ plays a game
+\end{enumerate}

predicate_logic/0002.tex

@@ -0,0 +1,8 @@
+\item \lect Model the following declarative sentences with predicate logic, as detailed as possible. Clearly indicate the intended meaning of all function, predicate, and constant symbols that you use.
+
+\begin{enumerate}
+	\item Alice has no sister.
+	\item A person who wears a crown is either a king or a queen.
+	\item Not everybody likes everybody.
+	\item Everybody loves somebody.
+\end{enumerate}

predicate_logic/0002_sol.tex

@@ -0,0 +1,15 @@
+$\mathcal{A} = \text{People}$ \\
+
+\begin{enumerate}
+    \item $\forall x \big(A(x) \imp \lnot S(x) \big)$ \\
+    	  $A(x) \ldots $ $x$ is Alice \\
+	      $S(x) \ldots $ $x$ has a sister \\
+    \item $\forall x \big(C(x) \imp K(x) \lor Q(x) \big)$ \\
+    	  $C(x) \ldots $ $x$ wears a crown \\
+	      $K(x) \ldots $ $x$ is a king \\
+	      $Q(x) \ldots $ $x$ is a queen \\
+	\item $\lnot \forall x \forall y \big(L(x,y) \big)$ \\
+          $L(x, y) \ldots $ $x$ likes $y$ \\
+	\item $\forall x \exists y \big(L(x,y) \big)$ \\
+          $L(x, y) \ldots $ $x$ loves $y$
+\end{enumerate}

predicate_logic/0003.tex

@@ -0,0 +1,7 @@
+\item \lect Model the following declarative sentences with predicate logic, as detailed as possible. Clearly indicate the intended meaning of all function, predicate, and constant symbols that you use.
+
+\begin{enumerate}
+    \item The construction takes a long time, is noisy, and blocks the sun.
+    \item If there is no school, at least one parent of each kid has to take vacation and cannot got to work.
+    \item All students have to take the exam eventually.
+\end{enumerate}

predicate_logic/0003_sol.tex

@@ -0,0 +1,17 @@
+\begin{enumerate}
+    \item $x \land y \land z$ \\
+          $x \ldots $ the construction side takes a long time \\
+          $y \ldots $ the construction side is noisy \\
+          $z \ldots $ the construction side blocks the sun \\
+    \item $\lnot a \imp \forall x \exists y \big(K(x) \land P(x,y) \imp V(y) \land \lnot W(y)\big)$ \\
+          $a \ldots $ there is school \\
+          $K(x) \ldots x$ is a kid \\
+          $P(x,y) \ldots y$ is parent of $x$\\
+          $V(x) \ldots x $ takes vacation \\
+          $W(x) \ldots x $ goes to work \\
+	      $\mathcal{A} = \text{$people$}$ \\
+    \item $\forall x \big(S(x) \imp E(x) \big)$ \\
+    	  $S(x) \ldots x$ is a student \\
+	      $E(x) \ldots x$ takes the exam \\
+        $\mathcal{A} = \text{People}$
+\end{enumerate}

predicate_logic/0004.tex

@@ -0,0 +1,7 @@
+\item \lect Model the following declarative sentences with predicate logic, as detailed as possible. Clearly indicate the intended meaning of all function, predicate, and constant symbols that you use.
+    
+\begin{enumerate}
+    \item If all kids wear gloves, then all parents will be happy.
+    \item All kids love pizza and spaghetti. 
+    \item All kids are fun, energetic, and cannot sit still.
+\end{enumerate}

predicate_logic/0004_sol.tex

@@ -0,0 +1,18 @@
+$\mathcal{A} = \text{People}$ \\
+
+\begin{enumerate}
+    \item $\forall x \big(K(x) \land G(x) \imp \forall y \big(P(y) \land H(y) \big) \big)$ \\
+          $K(x) \ldots x $ is a kid \\
+          $G(x) \ldots x $ wears gloves \\
+          $P(x) \ldots x $ is a parent \\
+          $H(x) \ldots x $ is happy \\
+    \item $\forall x \big(K(x) \imp P(x) \land S(x) \big)$ \\
+          $K(x) \ldots x $ is a kid \\
+          $P(x) \ldots x $ loves pizza \\
+          $S(x) \ldots x $ loves spaghetti \\
+    \item $\forall x \big(K(x) \imp F(x) \land E(x) \land \lnot S(x) \big)$ \\
+          $K(x) \ldots x $ is a kid \\
+          $F(x) \ldots x $ is fun \\
+          $E(x) \ldots x $ is energetic \\
+          $S(x) \ldots x $ can sit still
+\end{enumerate}

predicate_logic/0005.tex

@@ -0,0 +1,5 @@
+\item Consider the following declarative sentence (known as \textit{Goldbach's Conjecture}):
+
+\textit{"Every even integer greater than 2 is equal to the sum of two prime numbers."}
+
+Model this sentence with predicate logic, as detailed as possible. Clearly indicate the intended meaning of all function, predicate, and constant symbols that you use.

predicate_logic/0005_sol.tex

@@ -0,0 +1,4 @@
+$\forall x \exists y,z \big(E(x) = P(y) + P(z)\big)$ \\
+$E(x) \ldots x $ is even \\
+$P(x) \ldots x $ is prime number \\
+$\mathcal{A} = \N$

predicate_logic/0006.tex

@@ -0,0 +1,2 @@
+\item \lect The syntax of predicate logic is defined via 2 types of sorts: \emph{terms} and
+\emph{formulas}. What are terms and what are formulas? Give examples for both.

predicate_logic/0006_sol.tex

@@ -0,0 +1,2 @@
+\emph{terms}: Terms talk about objects, they are elements of the domain: individual objects like Alice or Bob, variables since they represent objects like $x, y$, function symbols since they refer to objects like $m(x)$ or $x+y$\\ \\
+\emph{formulas}: Formulas have a truth value. Each predicate is a formula, e.g. $S(x)$, $P(x)$, $\forall x \big(S(x) \imp P(x) \big)$ 

predicate_logic/0007.tex

@@ -0,0 +1 @@
+\item \lect Give the definition of the syntax of predicate logic.

predicate_logic/0007_sol.tex

@@ -0,0 +1,20 @@
+\begin{itemize}
+    \item $\mathcal{V}$: Defines the set of variable symbols, e.g., $x,y,z$.
+    \item $\mathcal{F}$: Defines the set of function symbols, e.g., $f,g,h$.
+    \item $\mathcal{P}$: Defines the set of predicate symbols, e.g., $P,Q,R$. \\
+\end{itemize}
+Terms are defined as follows:
+\begin{itemize}
+    \item Any variable is a term.
+    \item If $c \in \mathcal{F}$ is a nullary function, then $c$ is a term.
+    \item If $t_1, t_2, \ldots t_n$ are terms and $f \in \mathcal{F}$ has arity $n > 0$, then $f(t_1, t_2, \ldots t_n)$ is a term.
+    \item Nothing else is a term. \\
+\end{itemize}
+Formulas are defined as follows:
+\begin{itemize}
+    \item If $P \in \mathcal{P}$ is a predicate with arity $n > 0$ and $t_1, t_2, \ldots t_n$ are terms over $\mathcal{F}$, then $P(t_1, t_2, \ldots t_n)$ is a formula.
+    \item If $\phi$ is a formula, then $\lnot \phi$ is a formula.
+    \item If $\phi$ and $\psi$ are formulas, then $(\phi \land \psi)$, $(\phi \lor \psi)$, $(\phi \imp \psi)$ are formulas.
+    \item If $\phi$ is a formula and $x$ is a variable, then $(\forall x \phi)$ and $(\exists x \phi)$ are formulas.
+    \item Nothing else is a formula. 
+\end{itemize}

predicate_logic/0008.tex

@@ -0,0 +1,2 @@
+\item Draw the syntax tree for the following formula:
+$$\forall x \; \Big(  \big(P(x,y) \imp P(x,x)\big)  \lor    \big(Q(y, z) \land \exists y \; R(x,y,z)\big)   \Big)$$

predicate_logic/0008_sol.tex

@@ -0,0 +1,17 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+ [.$\forall x$ 
+    [.$\lor$
+        [.$\imp$
+            [.$P$ $x$ $y$ ]
+            [.$P$ $x$ $y$ ]
+        ]
+        [.$\land$
+            [.$Q$ $y$ $z$ ]
+            [.$\exists y$
+                [.$R$ $x$ $y$ $z$ ]
+            ] 
+        ]
+    ]
+ ]
+\end{tikzpicture}

predicate_logic/0009.tex

@@ -0,0 +1,2 @@
+\item \lect Draw the syntax tree for the following formula:
+$$\forall x \exists y \; (P(x, f(y)) \land Q(y, z) \imp R(f(z))).$$

predicate_logic/0009_sol.tex

@@ -0,0 +1,19 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+ [.$\forall x$ 
+    [.$\forall y$
+        [.$\imp$
+            [.$\land$ 
+                [.$P$
+                    [.$x$ ]
+                    [.$f$ $y$ ]
+                ]
+                [.$Q$ $y$ $z$ ]
+            ]
+            [.$R$
+                [.$f$ $z$ ]
+            ]
+        ]
+    ]
+ ]
+\end{tikzpicture}

predicate_logic/0010.tex

@@ -0,0 +1,3 @@
+\item \lect Given the formula 
+$$P(x,y) \lor \exists y \forall x \; \big(Q(x,y)\land R(y,z) \big),$$
+construct a syntax tree for $\phi$ and determine the \textit{scope} of its quantifiers and which occurrences of the variables are \textit{free} and which are \textit{bound}.

predicate_logic/0010_sol.tex

@@ -0,0 +1,17 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+ [.$\lor$ 
+    [.$P$ $x$ $y$ ]
+    [.$\exists y$
+        [.$\forall x$
+            [.$\land$ 
+                [.$Q$ $x$ $y$ ]
+                [.$R$ $y$ $z$ ]
+            ]
+        ]
+    ]
+ ]
+\end{tikzpicture} 
+\newline \\
+Free variables: $x, y, z$ \\
+Bound variables: $x, y$

predicate_logic/0011.tex

@@ -0,0 +1 @@
+\item \lect Given the formula $$\phi = \forall x \exists z \; \big( \lnot P(x) \lor Q(y, f(z))\big) \imp \big( \exists x \; P(y) \land Q(f(x), z)\big),$$ construct a syntax tree for $\phi$ and determine the \textit{scope} of its quantifiers and which occurrences of the variables are \textit{free} and which are \textit{bound}.

predicate_logic/0011_sol.tex

@@ -0,0 +1,32 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\imp$ 
+    [.$\forall x$ 
+        [.$\exists z$
+            [.$\lor$
+                [.$\lnot$
+                    [.$P$ $x$ ]
+                    ]
+                [.$Q$
+                    [.$y$ ]
+                    [.$f$ $z$ ]
+                ]
+            ]
+        ]
+    ]
+    [.$\land$ 
+        [.$\exists x$
+            [.$\land$
+                [.$P$ $y$ ]
+                [.$Q$
+                    [.$f$ $x$ ]
+                    [.$z$ ]
+                ]
+            ]
+        ]
+    ]
+]
+\end{tikzpicture} 
+\newline \\
+Free variables: $y, z$ \\
+Bound variables: $x, z$

predicate_logic/0012.tex

@@ -0,0 +1,2 @@
+\item \lect Give a model $\mathcal{M}$ for the following formula:
+$$\phi \coloneqq \exists x \forall y P(x,y).$$

predicate_logic/0012_sol.tex

@@ -0,0 +1,2 @@
+$\mathcal{M}: \mathcal{A} = \{a, b\}$ \\
+$P^\mathcal{M} = \{(a,a), (a,b)\}$

predicate_logic/0013.tex

@@ -0,0 +1,5 @@
+\item \lect Consider the formula 
+$$\phi \coloneqq \forall x \exists y (P(x,y)\wedge Q(x)).$$
+Give a model the satisfies the formula and a second one that falsifies the formula.
+
+Show using the parse tree why your models satisfy are falsify the formula.

predicate_logic/0013_sol.tex

@@ -0,0 +1,95 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+ [.$\forall x$
+    [.$\exists y$
+        [.$\land$ 
+            [.$P$ $x$ $y$ ]
+            [.$Q$ $x$ ]
+        ]
+    ]
+ ]
+\end{tikzpicture} 
+
+\begin{multicols}{2}
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\exists y$
+    [.$\land$ 
+        [.$P$ $a$ $y$ ]
+        [.$Q$ $a$ ]
+    ]
+]
+\end{tikzpicture} 
+\newline
+Subtree: $x=a$ \\
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\land$ 
+    [.$P$ $a$ $a$ ]
+    [.$Q$ $a$ ]
+]
+\end{tikzpicture} 
+\newline
+Subtree: $x=a \land y=a$ \\
+Evaluates $\mathcal{M}_1$ to true. \\
+Evaluates $\mathcal{M}_2$ to false.
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\land$ 
+    [.$P$ $a$ $b$ ]
+    [.$Q$ $a$ ]
+]
+\end{tikzpicture} 
+\newline
+Subtree: $x=a \land y=b$ \\
+Evaluates $\mathcal{M}_1$ to true. \\
+Evaluates $\mathcal{M}_2$ to false.
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\exists y$
+    [.$\land$ 
+        [.$P$ $b$ $y$ ]
+        [.$Q$ $b$ ]
+    ]
+]
+\end{tikzpicture} 
+\newline
+Subtree: $x=b$ \\
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\land$ 
+    [.$P$ $b$ $a$ ]
+    [.$Q$ $b$ ]
+]
+\end{tikzpicture} 
+\newline
+Subtree: $x=b \land y=a$ \\
+Evaluates $\mathcal{M}_1$ to true. \\
+Evaluates $\mathcal{M}_2$ to false.
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\land$ 
+    [.$P$ $b$ $b$ ]
+    [.$Q$ $b$ ]
+]
+\end{tikzpicture} 
+\newline
+Subtree: $x=b \land y=b$ \\
+Evaluates $\mathcal{M}_1$ to true. \\
+Evaluates $\mathcal{M}_2$ to false.
+\end{multicols}
+
+$\mathcal{M}_1: \mathcal{A} = \{a, b\}$ \\
+$P$ = true \\
+$Q$ = true \\ 
+$\mathcal{M}_1 \models \phi$ \\ 
+
+$\mathcal{M}_2: \mathcal{A} = \{a, b\}$ \\
+$P$ = true \\
+$Q$ = false \\ 
+$\mathcal{M}_2 \not\models \phi$

predicate_logic/0014.tex

@@ -0,0 +1,6 @@
+\item \lect Consider the formula $$\phi = \exists x \forall y \; \big( P(x,y) \imp (Q(x,y) \lor R(x,y))\big).$$
+Does the following model $\mathcal{M}$ satisfy the formula? \\
+            $\mathcal{A} = \{a,b\}$ \\
+            $P^\mathcal{M} = \{(a,a),(a,b)\}$ \\
+            $Q^\mathcal{M} = \{(a,a),(b,a)\}$\\
+            $R^\mathcal{M} = \{(a,a),(b,b)\}$

predicate_logic/0014_sol.tex

@@ -0,0 +1,58 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+ [.$\exists x$
+    [.$\forall y$
+        [.$\imp$ 
+            [.$P$ $x$ $y$ ]
+            [.$\lor$
+                [.$Q$ $x$ $y$ ]
+                [.$R$ $x$ $y$ ]
+            ]
+        ]
+    ]
+ ]
+\end{tikzpicture}
+\newline
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\forall y$
+    [.$\imp$ 
+        [.$P$ $b$ $y$ ]
+        [.$\lor$
+            [.$Q$ $b$ $y$ ]
+            [.$R$ $b$ $y$ ]
+        ]
+    ]
+]
+\end{tikzpicture}
+\newline 
+Subtree: $x=b$ \\
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\imp$ 
+    [.$P$ $b$ $a$ ]
+    [.$\lor$
+        [.$Q$ $b$ $a$ ]
+        [.$R$ $b$ $a$ ]
+    ]
+]
+\end{tikzpicture}
+\newline 
+Subtree: $x=b \land y=a$
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\imp$ 
+    [.$P$ $b$ $b$ ]
+    [.$\lor$
+        [.$Q$ $b$ $b$ ]
+        [.$R$ $b$ $b$ ]
+    ]
+]
+\end{tikzpicture}
+\newline 
+Subtree: $x=b \land y=b$
+
+The model $\mathcal{M}$ satisfies the formula.

predicate_logic/0015.tex

@@ -0,0 +1,2 @@
+\item \lect Give the definition of a model in predicate logic.
+Discuss what needs to be defined in a \emph{model} of a predicate logic formula. Give an example for each data that could be contained in a model.

predicate_logic/0015_sol.tex

@@ -0,0 +1,9 @@
+\textbf{Definition - Model in Predicate Logic.} \textit{A model $\mathcal{M}$ consists of the following set of data:}
+\begin{itemize}
+    \item \textit{A non-empty set $\mathcal{A}$, the universe/domain of concrete values;}
+    \item \textit{for each nullary function symbol $f \in \mathcal{F}$, a concrete element $f^\mathcal{M} \in \mathcal{A}$;}
+    \item \textit{for each nullary predicate symbol $P \in \mathcal{P}$, a truth value;}
+    \item \textit{for each function symbol $f \in \mathcal{F}$ with arity $n > 0$ a concrete function $f^\mathcal{M}: \mathcal{A}^n \imp \mathcal{A}$;}
+    \item \textit{for each predicate smybol $P \in \mathcal{P}$ with arity $n > 0$: subset $P^\mathcal{M} \subseteq	\mathcal{A}^n$;}
+    \item \textit{for any free variable} var: \textit{a lookup-table $t:$} var \textit{$\imp \mathcal{A}$.}
+\end{itemize}

predicate_logic/0016.tex

@@ -0,0 +1,4 @@
+\item \lect For the following formula in \textit{Predicate Logic}, find a \textit{model} that satisfies the formula and one that does not. Draw a syntax tree and state all free variables while solving this task.
+\begin{enumerate}
+  \item $\forall x \exists y \; \big( P(f(y))~\land~P(x) \big) ~\imp~Q(f(f(y)))$
+\end{enumerate}

predicate_logic/0016_sol.tex

@@ -0,0 +1,34 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\imp$
+    [.$\forall x$
+        [.$\exists y$
+            [.$\land$
+                [.$P$
+                    [.$f$ $y$ ]
+                ]
+                [.$P$ $x$ ]
+            ]
+        ]
+    ]
+    [.$Q$
+        [.$f$
+            [.$f$ $y$ ]
+        ]
+    ]
+]
+\end{tikzpicture}
+\newline \\
+Free variables: $y$ \\
+
+$\mathcal{M}_1: \mathcal{A} = \{a, b\}$ \\
+$P^{\mathcal{M}_1}$ = true \\
+$Q^{\mathcal{M}_1}$ = true \\
+$\mathcal{M}_1 \models \phi$ \\
+$f$ can be defined arbitrarily in this case.
+
+$\mathcal{M}_2: \mathcal{A} = \{a, b\}$ \\
+$P^{\mathcal{M}_2}$ = true \\
+$Q^{\mathcal{M}_2}$ = false \\
+$\mathcal{M}_2 \not\models \phi$
+$f$ can be defined arbitrarily in this case.

predicate_logic/1001.tex

@@ -0,0 +1,8 @@
+\item \self Translate the following sentences into predicate logic. Be as precise as possible. Give the meaning of any function and predicate symbols you use.
+
+\begin{enumerate}
+  \item Nobody knows everybody.
+  \item All birds can fly, except for penguins and ostrichs.
+  \item Not all birds can fly, but some birds can fly.
+  \item All kids are cute and quite if and only if they are sleeping
+\end{enumerate}

predicate_logic/1002.tex

@@ -0,0 +1,3 @@
+\item \ifassignmentsheet \points{2} \fi Translate the following sentence into predicate logic. Be as precise as possible. Give the meaning of any function and predicate symbols you use.
+
+\textit{Every even integer greater than 2 is equal to the sum of two prime numbers.}

predicate_logic/1003.tex

@@ -0,0 +1,13 @@
+\item \self Consider the following declarative sentence:
+
+\textit{``For every natural number it holds that it is prime if and
+only if there is no smaller natural number, except for 1, that
+divides it.''}
+
+Model this sentence with predicate logic, as detailed as possible.
+Clearly indicate the intended meaning of all function, predicate, and
+constant symbols that you use.
+
+Also, model the same sentence in propositional logic, as detailed as
+possible. Clearly indicate the intended meaning of each propositional
+variable you use.

predicate_logic/1004.tex

@@ -0,0 +1,7 @@
+\item \self
+
+\textit{``For all triangles it holds it is a scalene triangle iff all its sides have different lengths and all its angles have different measure.''}
+
+Model this sentence with predicate logic, as detailed as possible.
+Clearly indicate the intended meaning of all function, predicate, and
+constant symbols that you use.

predicate_logic/1005.tex

@@ -0,0 +1,11 @@
+\item \self
+
+\textit{``Everyone gets a break once in a while, but the break cannot last forever''}
+
+Model this sentence with predicate logic, as detailed as possible.
+Clearly indicate the intended meaning of all function, predicate, and
+constant symbols that you use.
+
+Also, model the same sentence in propositional logic, as detailed as
+possible. Clearly indicate the intended meaning of each propositional
+variable you use.

predicate_logic/1006.tex

@@ -0,0 +1,7 @@
+\item \self
+Model the following sentences with predicate logic, as detailed as possible. Clearly indicate the intended meaning of all function, predicate, and constant symbols that you use.
+
+\begin{enumerate}
+    \item Every integer is greater or equal to one.
+    \item For any two integers, their sum  is smaller than their product
+\end{enumerate}

predicate_logic/1007.tex

@@ -0,0 +1,11 @@
+\item \self Given is the following formula in predicate logic
+$$\phi = \forall x \exists y \Bigl(
+\bigl(
+Q(x,y) \wedge P(x,y)
+\bigr)
+\implies
+\bigl(
+R(y, x)  \wedge P(x,y)
+\bigr)
+\Bigr). $$
+Draw the syntax tree for $\phi$.

predicate_logic/1008.tex

@@ -0,0 +1,11 @@
+\item \self Given is the following formula in predicate logic
+$$\phi = \exists x \forall y \Bigl(
+\bigl(
+P(x,y) \implies Q(x,y)
+\bigr)
+\vee
+\bigl(
+P(y, x)  \implies R(x,y)
+\bigr)
+\Bigr). $$
+Draw the syntax tree for $\phi$.

predicate_logic/1009.tex

@@ -0,0 +1,7 @@
+\item In the context of predicate logic:
+\begin{enumerate}
+    \item What is the scope of a quantifier?
+    \item What is the difference between \emph{free} and \emph{bound} variables?
+\end{enumerate}
+
+Given an example that shows the difference.

predicate_logic/1010.tex

@@ -0,0 +1 @@
+\item \self In the context of predicate logic, give a definition of \textit{substitution} of variables.

predicate_logic/1011.tex

@@ -0,0 +1,3 @@
+\item \self What does it mean to \emph{substitute a term $t$ for a variable $x$ in a predicate logic formula?}
+Which rules to you have to consider when performing substitution?
+Give an example.

predicate_logic/1012.tex

@@ -0,0 +1,7 @@
+\item \self Consider the following formula.
+$$\phi \coloneqq \forall y \big(P(x) \land Q(y)\big) \lor \big(R(y) \land Q(x)\big)$$
+\begin{enumerate}
+    \item  Compute $\phi[f(x)/x]$.
+    \item  Compute $\phi[f(y)/x]$.
+    \item  Compute $\phi[f(z)/x]$.
+\end{enumerate}

predicate_logic/1013.tex

@@ -0,0 +1,8 @@
+\item \self Consider the following formula.
+$$\phi \coloneqq \forall y \big(P(x) \land Q(y)\big) \rightarrow  \exists x \big(R(y) \land Q(x)\big)$$
+\begin{enumerate}
+    \item  Compute $\phi[f(y)/x]$.
+    \item  Compute $\phi[f(x)/y]$.
+    \item  Compute $\phi[k/z]$.
+    \item  Compute $\phi[x/z]$.
+\end{enumerate}

predicate_logic/1014.tex

@@ -0,0 +1,8 @@
+\item \self Given the formula $$\phi = \forall x \exists z \; \big( \lnot P(x) \lor Q(y, f(z))\big) \imp \big(\lnot \exists x \; P(y) \land Q(f(x), z)\big).$$ 
+
+\begin{enumerate}
+    \item  Compute $\phi[f(y)/x]$.
+    \item  Compute $\phi[f(x)/y]$.
+    \item  Compute $\phi[k/z]$.
+    \item  Compute $\phi[x/z]$.
+\end{enumerate}

predicate_logic/1015.tex

@@ -0,0 +1,16 @@
+\item \self In the following list, tick all items that are required for a
+    complete model of a formula $\varphi$ in predicate logic.
+\begin{itemize}
+\item[$\square$] A non-empty, possibly infinite set of values for
+    variables and functions.
+\item[$\square$] A concrete value for every bound variable in
+    $\varphi$.
+\item[$\square$] A concrete value for free bound variable in
+    $\varphi$.
+\item[$\square$] A definition for each predicate in $\varphi$,
+    detailing for which values/tuples the predicate returns
+    \emph{true}.
+\item[$\square$] A definition for each function in $\varphi$,
+    detailing for which values/tuples the predicate returns
+    \emph{true}.
+\end{itemize}

predicate_logic/1016.tex

@@ -0,0 +1,21 @@
+\item \self Given is the following formula in predicate logic
+$$\phi = \forall x \exists y \Bigl(
+\bigl(
+Q(x,y) \wedge P(x,y)
+\bigr)
+\implies
+\bigl(
+R(y, x)  \wedge P(x,y)
+\bigr)
+\Bigr) $$
+and the model $\mathcal{M}$:
+
+\begin{itemize}
+\item  $\mathcal{A} = \{a, b\} $
+\item  $P^\mathcal{M} = \{(m,a) | m \in \mathcal{A} \}$
+\item  $Q^\mathcal{M} = \{(b,m) | m \in \mathcal{A} \}$
+\item  $R^\mathcal{M} = \{(a,b),(b,a), (b,b) \}$
+\end{itemize}
+
+Does the model $\mathcal{M}$ satisfy the formula $\phi$?
+Explain your answer by drawing a \textbf{syntax tree} and evaluate the model $\mathcal{M}$ with the help of this syntax tree.

predicate_logic/1017.tex

@@ -0,0 +1,23 @@
+\item
+  \ifassignmentsheet \points{2} \fi
+Given is the following formula in predicate logic
+$$\phi = \exists x \forall y \Bigl(
+\bigl(
+P(x,y) \implies Q(x,y)
+\bigr)
+\vee
+\bigl(
+P(y, x)  \implies R(x,y)
+\bigr)
+\Bigr) $$
+and the model $\mathcal{M}$:
+
+\begin{itemize}
+\item  $\mathcal{A} = \{a, b\} $
+\item  $P^{M} = \{(a,b), (b,b), (b,a)\}$
+\item  $Q^{M} = \{(a,a)\}$
+\item  $R^{M} = \{(b,b)\}$
+\end{itemize}
+
+Does the model $\mathcal{M}$ satisfy the formula $\phi$?
+Evaluate $\Model$ using a syntax tree.

predicate_logic/1017_sol.tex

@@ -0,0 +1,88 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+ [.$\exists x$
+    [.$\forall y$
+        [.$\lor$
+            [.$\imp$
+                [.$P$ $x$ $y$ ]
+                [.$Q$ $x$ $y$ ]
+            ]
+            [.$\imp$
+                [.$P$ $y$ $x$ ]
+                [.$R$ $x$ $y$ ]
+            ]
+        ]
+    ]
+ ]
+\end{tikzpicture}
+
+\begin{itemize}
+  \item $x=a$
+\end{itemize}
+
+\begin{multicols}{2}
+  $$x=a \land y=a$$
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+        [.$\lor$
+            [.$\imp$
+                [.$P$ $a$ $a$ ]
+                [.$Q$ $a$ $a$ ]
+            ]
+            [.$\imp$
+                [.$P$ $a$ $a$ ]
+                [.$R$ $a$ $a$ ]
+            ]
+        ]
+\end{tikzpicture}
+ \begin{align*}
+   &(P(a,a) \imp Q(a,a)) \lor (P(a,a) \imp R(a,a)) = \\
+   &(\false \imp \true) \lor (\false \imp \true) = \true
+ \end{align*}
+\columnbreak
+  $$x=a \land y=b$$
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+        [.$\lor$
+            [.$\imp$
+                [.$P$ $a$ $b$ ]
+                [.$Q$ $a$ $b$ ]
+            ]
+            [.$\imp$
+                [.$P$ $b$ $a$ ]
+                [.$R$ $a$ $b$ ]
+            ]
+        ]
+\end{tikzpicture}
+ \begin{align*}
+   &(P(a,b) \imp Q(a,b)) \lor (P(b,a) \imp R(b,a)) = \\
+   &(\true \imp \false) \lor (\true \imp \false) = \false
+ \end{align*}
+\end{multicols}
+
+
+\begin{itemize}
+  \item $x=b$
+\end{itemize}
+
+\begin{centering}
+  $$x=b \land y=a$$
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+        [.$\lor$
+            [.$\imp$
+                [.$P$ $b$ $a$ ]
+                [.$Q$ $b$ $a$ ]
+            ]
+            [.$\imp$
+                [.$P$ $a$ $b$ ]
+                [.$R$ $b$ $a$ ]
+            ]
+        ]
+\end{tikzpicture}
+ \begin{align*}
+   &(P(b,a) \imp Q(b,a)) \lor (P(a,b) \imp R(b,a)) = \\
+   &(\true \imp \false) \lor (\true \imp \false) = \false
+ \end{align*}
+\end{centering}
+We do not need to evaluate $x=b \land y=b$. $M\nmodels\varphi$.

predicate_logic/1018.tex

@@ -0,0 +1,6 @@
+\item \self For the formula below,  find one
+    model that satisfies the formula, and one model that does not
+    satisfy the formula.
+    Explain your answer by drawing a \textbf{syntax tree} and evaluate the model $\mathcal{M}$ with the help of this syntax tree.
+
+ $$\exists x (P(x) \land Q(f(x))) \lor (\neg P(x) \land \neg Q(f(x))$$

predicate_logic/1019.tex

@@ -0,0 +1,6 @@
+\item \self For the formula below,  find one
+    model that satisfies the formula, and one model that does not
+    satisfy the formula.
+    Explain your answer by drawing a \textbf{syntax tree} and evaluate the model $\mathcal{M}$ with the help of this syntax tree.
+    
+ $$\neg\forall x ((P(x) \implies P(y)) \land P(x))$$

predicate_logic/1020.tex

@@ -0,0 +1,6 @@
+\item \ifassignmentsheet \points{3} \fi  For the formula below, state one
+    model that satisfies the formula, and one model that does not
+    satisfy the formula.
+    Explain your answer by drawing a syntax tree and evaluate your models with the help of this syntax tree.
+
+ $$\forall x \exists y (P(f(x),y) \land \neg P(x,f(y)))$$

predicate_logic/1021.tex

@@ -0,0 +1,5 @@
+\item For each of the formulas in predicate logic below, find a model that satisfies the formula and one that does not. Draw a syntax tree and state all free variables while solving this task.
+\begin{enumerate}
+    \item $\neg\forall x ((P(x) \implies P(y)) \land P(x))$
+    \item $\forall x \exists y (P(x,y) \land \neg P(f(x),f(y)))$
+\end{enumerate}

predicate_logic/1022.tex

@@ -0,0 +1,6 @@
+\item \self Consider the following declarative sentences:
+
+\textit{"Every person who has the same parents as John Doe and is different from John Doe himself is a sibling of John Doe."}
+
+Model this sentence with predicate logic, as detailed as possible. Clearly indicate the intended meaning of all function, predicate, and constant symbols that you use.\\
+Also, model the same sentence in propositional logic, as detailed as possible. Clearly indicate the intended meaning of each propositional variable you use.

predicate_logic/1023.tex

@@ -0,0 +1,3 @@
+\item \ifassignmentsheet \points{2} \fi Translate the following sentence into predicate logic. Be as precise as possible. Give the meaning of any function and predicate symbols you use.
+
+\textit{Every person who has the same parents as John Doe and is different from John Doe himself is a sibling of John Doe.}

predicate_logic/2001.tex

@@ -0,0 +1,23 @@
+\item
+  \ifassignmentsheet \point{1}
+  \else \prac
+  \fi
+Consider the sentence $\phi = \exists x \forall y (P(x,y) \implies (Q(x,y) \lor R(x,y)))$.
+Does the following model satisfy $\phi$?
+
+The model $M$ consists of:
+\begin{itemize}
+\item  $A = \{a, b, c\} $
+\item  $P^{M} = \{(a,a), (a,b), (b,a), (b,b), (c,a), (c,b)\}$
+\item  $Q^{M} = \{(a,m) | m \in A \}$
+\item  $R^{M} = \{(a,a), (b,a), (a,c), (b,c), (c,c)\}$
+\end{itemize}
+
+
+% \item The model $M'$ consists of:
+%\begin{itemize}
+%\item  $A = \mathbb{Z} $
+%\item  $P^{M} = \{(m,n) | m \ge n \}$
+%\item  $Q^{M} = \{(m,n) | m \le n \}$
+%\item  $R^{M} = \{(m,n) | m = -n \}$
+%\end{itemize}

predicate_logic/2001_sol.tex

@@ -0,0 +1,82 @@
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+ [.$\exists x$
+    [.$\forall y$
+        [.$\imp$
+            [.$P$ $x$ $y$ ]
+            [.$\lor$
+                [.$Q$ $x$ $y$ ]
+                [.$R$ $x$ $y$ ]
+            ]
+        ]
+    ]
+ ]
+\end{tikzpicture}
+
+
+\begin{multicols}{2}
+
+  $$x=a \land y=a$$
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+% [.$\exists x$
+%    [.$\forall y$
+        [.$\imp$
+            [.$P$ $a$ $a$ ]
+            [.$\lor$
+                [.$Q$ $a$ $a$ ]
+                [.$R$ $a$ $a$ ]
+            ]
+        ]
+%    ]
+% ]
+\end{tikzpicture}
+ \begin{align*}
+   &P(a,a) \imp (Q(a,a) \lor R(a,a)) = \\
+   &\true \imp (\true \lor \true) = \true
+ \end{align*}
+\columnbreak
+  $$x=a \land y=b$$
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+% [.$\exists x$
+%    [.$\forall y$
+        [.$\imp$
+            [.$P$ $a$ $b$ ]
+            [.$\lor$
+                [.$Q$ $a$ $b$ ]
+                [.$R$ $a$ $b$ ]
+            ]
+        ]
+%    ]
+% ]
+\end{tikzpicture}
+ \begin{align*}
+   &P(a,b) \imp (Q(a,b) \lor R(a,b)) = \\
+   &\true \imp (\true \lor \false) = \true
+ \end{align*}
+\end{multicols}
+\begin{centering}
+  $$x=a \land y=c$$
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+% [.$\exists x$
+%    [.$\forall y$
+        [.$\imp$
+            [.$P$ $a$ $c$ ]
+            [.$\lor$
+                [.$Q$ $a$ $c$ ]
+                [.$R$ $a$ $c$ ]
+            ]
+        ]
+%    ]
+% ]
+\end{tikzpicture}
+ \begin{align*}
+   &P(a,c) \imp (Q(a,c) \lor R(a,c)) = \\
+   &\false \imp (\true \lor \true) = \true
+ \end{align*}
+\end{centering}
+
+We have found an $x$, such that for all $y$ the formula evaluates to \textit{true}. Therefore $$M \models \varphi.$$

predicate_logic/2002.tex

@@ -0,0 +1,9 @@
+\item
+  \ifassignmentsheet \points{3}
+  \else \prac
+  \fi
+For each of the formulas of predicate logic below, find a model that satisfies the formula and one that does not. Draw a syntax tree and state all free variables.
+    \begin{enumerate}
+      \item \ifassignmentsheet \point{1} \fi $\forall x (P(x,x)) \lor \forall y (Q(x,y))$
+      \item \ifassignmentsheet \points{2} \fi $\neg \forall x ((Q(f(x)) \implies P(f(f(x)))) \wedge \neg Q(x))$
+    \end{enumerate}

predicate_logic/2002_sol.tex

@@ -0,0 +1,73 @@
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.15cm]
+\Tree
+ [.$\lor $
+    [.$\forall x$
+        [.$P$ $x$ $x$ ]
+    ]
+    [.$\forall y$
+        [.$Q$ $x$ $y$ ]
+    ]
+ ]
+\end{tikzpicture}
+
+The $x$ in the right subformula is a free variable.
+
+
+\begin{multicols}{2}
+An example for a \emph{satisfying} model $\Model_{SAT}$:
+\begin{itemize}
+\item  $\mathcal{A} = \{a, b\} $
+\item  $P^{\Model_{SAT}} = \{(a,a), (b,b)\}$
+\item  $Q^{\Model_{SAT}} = \{(a,a), (a,b)\}$
+\end{itemize}
+\columnbreak
+An example for an \emph{unsatisfying} model $\Model_{UNSAT}$:
+\begin{itemize}
+\item  $\mathcal{A} = \{a, b\} $
+\item  $P^{\Model_{UNSAT}} = \{(a,a)\}$
+\item  $Q^{\Model_{UNSAT}} = \{(a,a)\}$
+\end{itemize}
+\end{multicols}
+
+
+\begin{tikzpicture}[every tree node/.style={draw,circle},sibling distance=.25cm]
+\Tree
+[.$\lnot$
+  [.$\forall x$
+    [.$\land$
+      [.$\imp$
+        [.$Q$
+          [.$f$ $x$ ]
+        ]
+        [.$P$
+          [.$f$
+            [.$f$ $x$ ]
+          ]
+        ]
+      ]
+      [.$\lnot$
+        [.$Q$ $x$ ]
+      ]
+    ]
+  ]
+]
+
+
+\end{tikzpicture}
+\begin{multicols}{2}
+An example for a \emph{satisfying} model $\Model_{SAT}$:
+\begin{itemize}
+\item $\mathcal{A} = \{a, b\} $
+\item $f^{\Model_{SAT}} = \{ x \rightarrow x \}$
+\item $P^{\Model_{SAT}} = \true$
+\item $Q^{\Model_{SAT}} = \false$
+\end{itemize}
+\columnbreak
+An example for an \emph{unsatisfying} model $\Model_{UNSAT}$:
+\begin{itemize}
+\item  $\mathcal{A} = \{a, b\} $
+\item  $f^{\Model_{UNSAT}} = \{ x \rightarrow x \}$
+\item  $P^{\Model_{UNSAT}} = \true$
+\item  $Q^{\Model_{UNSAT}} = \false$
+\end{itemize}
+\end{multicols}

predicate_logic/predicate_logic.tex

@@ -0,0 +1,159 @@
+\begin{questionSection}{Predicates and Quantifiers}
+\question{predicate_logic/0001.tex}
+         {predicate_logic/0001_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0002.tex}
+         {predicate_logic/0002_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0003.tex}
+         {predicate_logic/0003_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0004.tex}
+         {predicate_logic/0004_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0005.tex}
+         {no_solution}
+         {3cm}
+\question{predicate_logic/1022.tex}
+         {no_solution}
+         {3cm}
+\question{predicate_logic/1001.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1002.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1003.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1004.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1005.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1006.tex}
+         {no_solution}
+         {3cm}
+
+\end{questionSection}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{questionSection}{Syntax of Predicate Logic}
+\question{predicate_logic/0006.tex}
+         {predicate_logic/0006_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0007.tex}
+         {predicate_logic/0007_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0008.tex}
+         {predicate_logic/0008_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0009.tex}
+         {predicate_logic/0009_sol.tex}
+         {3cm}
+
+\question{predicate_logic/1007.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1008.tex}
+         {no_solution}
+         {3cm}
+\end{questionSection}
+\begin{questionSection}{Free and Bound Variables}
+\question{predicate_logic/0010.tex}
+         {predicate_logic/0010_sol.tex}
+         {3cm}
+
+\question{predicate_logic/1009.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1010.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1011.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1012.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1013.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1014.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/0011.tex}
+         {predicate_logic/0011_sol.tex}
+         {3cm}
+\end{questionSection}
+\begin{questionSection}{Semantics of Predicate Logic}
+\question{predicate_logic/0012.tex}
+         {predicate_logic/0012_sol.tex}
+         {3cm}
+
+\question{predicate_logic/0013.tex}
+         {predicate_logic/0013_sol.tex}
+         {3cm}
+
+
+\question{predicate_logic/0014.tex}
+         {predicate_logic/0014_sol.tex}
+         {3cm}
+
+
+\question{predicate_logic/0015.tex}
+         {predicate_logic/0015_sol.tex}
+         {3cm}
+
+
+\question{predicate_logic/0016.tex}
+         {predicate_logic/0016_sol.tex}
+         {3cm}
+\question{predicate_logic/1015.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1016.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1018.tex}
+         {no_solution}
+         {3cm}
+\question{predicate_logic/1019.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1020.tex}
+         {no_solution}
+         {3cm}
+
+\question{predicate_logic/1021.tex}
+         {no_solution}
+         {3cm}
+  \question{predicate_logic/2001.tex}
+           {predicate_logic/2001_sol.tex}
+           {4cm}
+  \question{predicate_logic/2002.tex}
+           {predicate_logic/2002_sol.tex}
+           {4cm}
+\end{questionSection}

util/chapter.tex

@@ -2,10 +2,10 @@
 %\chapterproplogictrue
 %\chaptersatsolvertrue
 %\chapterndproptrue
-%\chapterpredlogictrue
+\chapterpredlogictrue
 %\chapterndpredtrue
 %\chaptersmttrue
-\chapterbddtrue
+%\chapterbddtrue
 %\chaptereqcheckingtrue
 %\chaptersymbenctrue
 %\chaptertemporaltrue

util/math_macros.tex

@@ -1,4 +1,11 @@
-\input{util/ltl_macros}
+%\input{util/ltl_macros}
+
+\newcommand{\dom}{\ensuremath\mathcal{A}}
+\newcommand{\boolDom}{\ensuremath\mathbb{B}}
+\newcommand{\N}{\ensuremath\mathbb{N}}
+%\newcommand{\Z}{\ensuremath\mathbb{Z}}
+\newcommand{\Q}{\ensuremath\mathbb{Q}}
+\newcommand{\R}{\ensuremath\mathbb{R}}
 
 \renewcommand{\phi}{\varphi}
 \renewcommand{\implies}{\rightarrow}

util/toggle.tex

@@ -1,2 +1,2 @@
-\annotatetrue
-\solutiontrue
+%\solutiontrue
+%\annotatetrue