diff --git a/main.tex b/main.tex index 5b4dd2a..cd870d7 100644 --- a/main.tex +++ b/main.tex @@ -100,7 +100,7 @@ \fi \ifchapterpredlogic - \setsectionnum{4} + \setsectionnum{6} \section{Predicate Logic} \input{predicate_logic/predicate_logic.tex} \pagebreak diff --git a/predicate_logic/0001.tex b/predicate_logic/0001.tex new file mode 100644 index 0000000..b1816b3 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/0001_sol.tex b/predicate_logic/0001_sol.tex new file mode 100644 index 0000000..5c6addb --- /dev/null +++ b/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} diff --git a/predicate_logic/0002.tex b/predicate_logic/0002.tex new file mode 100644 index 0000000..0648bb8 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/0002_sol.tex b/predicate_logic/0002_sol.tex new file mode 100644 index 0000000..7be7eff --- /dev/null +++ b/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} diff --git a/predicate_logic/0003.tex b/predicate_logic/0003.tex new file mode 100644 index 0000000..241a19b --- /dev/null +++ b/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} diff --git a/predicate_logic/0003_sol.tex b/predicate_logic/0003_sol.tex new file mode 100644 index 0000000..f848fae --- /dev/null +++ b/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} diff --git a/predicate_logic/0004.tex b/predicate_logic/0004.tex new file mode 100644 index 0000000..98b42ce --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/0004_sol.tex b/predicate_logic/0004_sol.tex new file mode 100644 index 0000000..78975a9 --- /dev/null +++ b/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} diff --git a/predicate_logic/0005.tex b/predicate_logic/0005.tex new file mode 100644 index 0000000..2f09c18 --- /dev/null +++ b/predicate_logic/0005.tex @@ -0,0 +1,5 @@ +\item \lect 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. \ No newline at end of file diff --git a/predicate_logic/0005_sol.tex b/predicate_logic/0005_sol.tex new file mode 100644 index 0000000..0da33aa --- /dev/null +++ b/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$ diff --git a/predicate_logic/0006.tex b/predicate_logic/0006.tex new file mode 100644 index 0000000..61517cb --- /dev/null +++ b/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. \ No newline at end of file diff --git a/predicate_logic/0006_sol.tex b/predicate_logic/0006_sol.tex new file mode 100644 index 0000000..c8c0231 --- /dev/null +++ b/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)$ \ No newline at end of file diff --git a/predicate_logic/0007.tex b/predicate_logic/0007.tex new file mode 100644 index 0000000..d451176 --- /dev/null +++ b/predicate_logic/0007.tex @@ -0,0 +1 @@ +\item \lect Give the definition of the syntax of predicate logic. diff --git a/predicate_logic/0007_sol.tex b/predicate_logic/0007_sol.tex new file mode 100644 index 0000000..15b14c3 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/0008.tex b/predicate_logic/0008.tex new file mode 100644 index 0000000..d6a59bb --- /dev/null +++ b/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)$$ diff --git a/predicate_logic/0008_sol.tex b/predicate_logic/0008_sol.tex new file mode 100644 index 0000000..884ad88 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/0009.tex b/predicate_logic/0009.tex new file mode 100644 index 0000000..e9b31e8 --- /dev/null +++ b/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))).$$ \ No newline at end of file diff --git a/predicate_logic/0009_sol.tex b/predicate_logic/0009_sol.tex new file mode 100644 index 0000000..71f4d8a --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/0010.tex b/predicate_logic/0010.tex new file mode 100644 index 0000000..3cf98e7 --- /dev/null +++ b/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}. \ No newline at end of file diff --git a/predicate_logic/0010_sol.tex b/predicate_logic/0010_sol.tex new file mode 100644 index 0000000..c58641b --- /dev/null +++ b/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$ \ No newline at end of file diff --git a/predicate_logic/0011.tex b/predicate_logic/0011.tex new file mode 100644 index 0000000..d236c92 --- /dev/null +++ b/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}. \ No newline at end of file diff --git a/predicate_logic/0011_sol.tex b/predicate_logic/0011_sol.tex new file mode 100644 index 0000000..f7cae76 --- /dev/null +++ b/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$ \ No newline at end of file diff --git a/predicate_logic/0012.tex b/predicate_logic/0012.tex new file mode 100644 index 0000000..7acf612 --- /dev/null +++ b/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).$$ \ No newline at end of file diff --git a/predicate_logic/0012_sol.tex b/predicate_logic/0012_sol.tex new file mode 100644 index 0000000..2efc8d2 --- /dev/null +++ b/predicate_logic/0012_sol.tex @@ -0,0 +1,2 @@ +$\mathcal{M}: \mathcal{A} = \{a, b\}$ \\ +$P^\mathcal{M} = \{(a,a), (a,b)\}$ \ No newline at end of file diff --git a/predicate_logic/0013.tex b/predicate_logic/0013.tex new file mode 100644 index 0000000..276dee0 --- /dev/null +++ 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. \ No newline at end of file diff --git a/predicate_logic/0013_sol.tex b/predicate_logic/0013_sol.tex new file mode 100644 index 0000000..e84aa9e --- /dev/null +++ b/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$ diff --git a/predicate_logic/0014.tex b/predicate_logic/0014.tex new file mode 100644 index 0000000..c923f95 --- /dev/null +++ b/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)\}$ \ No newline at end of file diff --git a/predicate_logic/0014_sol.tex b/predicate_logic/0014_sol.tex new file mode 100644 index 0000000..12f3f9e --- /dev/null +++ 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. \ No newline at end of file diff --git a/predicate_logic/0015.tex b/predicate_logic/0015.tex new file mode 100644 index 0000000..a54c376 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/predicate_logic/0015_sol.tex b/predicate_logic/0015_sol.tex new file mode 100644 index 0000000..a79aa16 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/0016.tex b/predicate_logic/0016.tex new file mode 100644 index 0000000..456188d --- /dev/null +++ b/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} diff --git a/predicate_logic/0016_sol.tex b/predicate_logic/0016_sol.tex new file mode 100644 index 0000000..a3da55e --- /dev/null +++ b/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. diff --git a/predicate_logic/1001.tex b/predicate_logic/1001.tex new file mode 100644 index 0000000..d9bfdea --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/1002.tex b/predicate_logic/1002.tex new file mode 100644 index 0000000..08faa49 --- /dev/null +++ b/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.} diff --git a/predicate_logic/1003.tex b/predicate_logic/1003.tex new file mode 100644 index 0000000..dcd5fb1 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/predicate_logic/1004.tex b/predicate_logic/1004.tex new file mode 100644 index 0000000..813782b --- /dev/null +++ b/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. \ No newline at end of file diff --git a/predicate_logic/1005.tex b/predicate_logic/1005.tex new file mode 100644 index 0000000..60c99f0 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/predicate_logic/1006.tex b/predicate_logic/1006.tex new file mode 100644 index 0000000..501fe4f --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/1007.tex b/predicate_logic/1007.tex new file mode 100644 index 0000000..d1f0bfc --- /dev/null +++ b/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$. \ No newline at end of file diff --git a/predicate_logic/1008.tex b/predicate_logic/1008.tex new file mode 100644 index 0000000..5f613f8 --- /dev/null +++ b/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$. \ No newline at end of file diff --git a/predicate_logic/1009.tex b/predicate_logic/1009.tex new file mode 100644 index 0000000..2b1b588 --- /dev/null +++ b/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. diff --git a/predicate_logic/1010.tex b/predicate_logic/1010.tex new file mode 100644 index 0000000..ed264cc --- /dev/null +++ b/predicate_logic/1010.tex @@ -0,0 +1 @@ +\item \self In the context of predicate logic, give a definition of \textit{substitution} of variables. diff --git a/predicate_logic/1011.tex b/predicate_logic/1011.tex new file mode 100644 index 0000000..68b56ad --- /dev/null +++ b/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. \ No newline at end of file diff --git a/predicate_logic/1012.tex b/predicate_logic/1012.tex new file mode 100644 index 0000000..8fd5aeb --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/1013.tex b/predicate_logic/1013.tex new file mode 100644 index 0000000..0829278 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/1014.tex b/predicate_logic/1014.tex new file mode 100644 index 0000000..8133c87 --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/1015.tex b/predicate_logic/1015.tex new file mode 100644 index 0000000..64431ff --- /dev/null +++ b/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} \ No newline at end of file diff --git a/predicate_logic/1016.tex b/predicate_logic/1016.tex new file mode 100644 index 0000000..9296f57 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/predicate_logic/1017.tex b/predicate_logic/1017.tex new file mode 100644 index 0000000..bf6f97a --- /dev/null +++ b/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. diff --git a/predicate_logic/1017_sol.tex b/predicate_logic/1017_sol.tex new file mode 100644 index 0000000..6e938f2 --- /dev/null +++ b/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$. diff --git a/predicate_logic/1018.tex b/predicate_logic/1018.tex new file mode 100644 index 0000000..5ca192a --- /dev/null +++ b/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))$$ diff --git a/predicate_logic/1019.tex b/predicate_logic/1019.tex new file mode 100644 index 0000000..fa48922 --- /dev/null +++ b/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))$$ \ No newline at end of file diff --git a/predicate_logic/1020.tex b/predicate_logic/1020.tex new file mode 100644 index 0000000..924d935 --- /dev/null +++ b/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)))$$ diff --git a/predicate_logic/1021.tex b/predicate_logic/1021.tex new file mode 100644 index 0000000..6f8b560 --- /dev/null +++ b/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} diff --git a/predicate_logic/1022.tex b/predicate_logic/1022.tex new file mode 100644 index 0000000..297438f --- /dev/null +++ b/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. diff --git a/predicate_logic/1023.tex b/predicate_logic/1023.tex new file mode 100644 index 0000000..fb37a73 --- /dev/null +++ b/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.} diff --git a/predicate_logic/2001.tex b/predicate_logic/2001.tex new file mode 100644 index 0000000..7f324a1 --- /dev/null +++ b/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} diff --git a/predicate_logic/2001_sol.tex b/predicate_logic/2001_sol.tex new file mode 100644 index 0000000..555f850 --- /dev/null +++ b/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.$$ diff --git a/predicate_logic/2002.tex b/predicate_logic/2002.tex new file mode 100644 index 0000000..b547cfd --- /dev/null +++ b/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} diff --git a/predicate_logic/2002_sol.tex b/predicate_logic/2002_sol.tex new file mode 100644 index 0000000..77f1ee8 --- /dev/null +++ b/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} diff --git a/predicate_logic/predicate_logic.tex b/predicate_logic/predicate_logic.tex new file mode 100644 index 0000000..8cff5f9 --- /dev/null +++ b/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} + {predicate_logic/0005_sol.tex} + {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} diff --git a/util/chapter.tex b/util/chapter.tex index b0f4048..4fa482d 100644 --- a/util/chapter.tex +++ b/util/chapter.tex @@ -2,10 +2,10 @@ %\chapterproplogictrue %\chaptersatsolvertrue %\chapterndproptrue -%\chapterpredlogictrue +\chapterpredlogictrue %\chapterndpredtrue %\chaptersmttrue -\chapterbddtrue +%\chapterbddtrue %\chaptereqcheckingtrue %\chaptersymbenctrue %\chaptertemporaltrue diff --git a/util/math_macros.tex b/util/math_macros.tex index 9293a6b..991cb21 100644 --- a/util/math_macros.tex +++ b/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} diff --git a/util/toggle.tex b/util/toggle.tex index 5d3d391..94aa6cd 100644 --- a/util/toggle.tex +++ b/util/toggle.tex @@ -1,2 +1,2 @@ -\annotatetrue -\solutiontrue \ No newline at end of file +%\solutiontrue +%\annotatetrue