Add FAIKR2 propositional and first order logic

src/fundamentals-of-ai-and-kr/module2/ainotes.cls

@@ -0,0 +1 @@
+../../ainotes.cls

src/fundamentals-of-ai-and-kr/module2/main.tex

@@ -0,0 +1,11 @@
+\documentclass[11pt]{ainotes}
+
+\title{Fundamentals of Artificial Intelligence and Knowledge Representation\\(Module 2)}
+\date{2023 -- 2024}
+
+\begin{document}
+
+    \makenotesfront
+    \input{sections/_logic.tex}
+
+\end{document}

src/fundamentals-of-ai-and-kr/module2/sections/_logic.tex

@@ -0,0 +1,3 @@
+\chapter{Propositional and first order logic}
+
+See \href{https://github.com/NotXia/unibo-ai-notes/tree/pdfs/languages-and-algorithms-for-ai/module2}{\texttt{Languages and Algorithms for AI (module 2)}}.

src/languages-and-algorithms-for-ai/module2/main.tex

@@ -7,5 +7,6 @@
 
     \makenotesfront
     \include{sections/_propositional_logic.tex}
+    \include{sections/_first_order_logic.tex}
 
 \end{document}

src/languages-and-algorithms-for-ai/module2/sections/_first_order_logic.tex

@@ -0,0 +1,44 @@
+\chapter{First order logic}
+
+
+\section{Syntax}
+\marginnote{Syntax}
+The symbols of propositional logic are:
+\begin{descriptionlist}
+    \item[Constants]
+        Known elements of the domain. Do not represent truth values.
+        
+    \item[Variables]
+        Unknown elements of the domain. Do not represent truth values.
+    
+    \item[Function symbols] 
+        Function $f^{(n)}$ applied on $n$ constants to obtain another constant.
+
+    \item[Predicate symbols]
+        Function $P^{(n)}$ applied on $n$ constants to obtain a truth value.
+
+    \item[Connectives] $\forall$ $\exists$ $\land$ $\vee$ $\rightarrow$ $\lnot$ $\leftrightarrow$ $\bot$ $($ $)$
+\end{descriptionlist}
+
+Using the basic syntax, the following constructs can be defined:
+\begin{descriptionlist}
+    \item[Term] Denotes elements of the domain.
+        \[ t := \texttt{constant} \,|\, \texttt{variable} \,|\, f^{(n)}(t_1, \dots, t_n) \]
+
+    \item[Proposition] Denotes truth values.
+        \[
+            P := \bot \,|\, P \land P \,|\, P \vee P \,|\,  P \rightarrow P \,|\, P \leftrightarrow P \,|\, 
+                \lnot P \,|\, \forall x. P \,|\, \exists x. P \,|\, (P) \,|\, P^{(n)}(t_1, \dots, t_n) 
+        \]
+\end{descriptionlist}
+
+
+\begin{description}
+    \item[Well-formed formula] \marginnote{Well-formed formula}
+        The definition of well-formed formula in first order logic extends the one of
+        propositional logic by adding the following conditions:
+        \begin{itemize}
+            \item If S is well-formed, $\exists X. S$ is well-formed. Where $X$ is a variable.
+            \item If S is well-formed, $\forall X. S$ is well-formed. Where $X$ is a variable.
+        \end{itemize}
+\end{description}

src/languages-and-algorithms-for-ai/module2/sections/_propositional_logic.tex

@@ -3,14 +3,13 @@
 \section{Syntax}
 \begin{description}
     \item[Syntax] \marginnote{Syntax}
-        Rules and symbols to define well formed sentences.
+        Rules and symbols to define well-formed sentences.
 \end{description}
 
 The symbols of propositional logic are:
 \begin{descriptionlist}
     \item[Proposition symbols] $p_0$, $p_1$, \dots
-    \item[Connectives] $\land$, $\vee$, $\rightarrow$, $\lnot$, $\leftrightarrow$, $\bot$
-    \item[Auxiliary symbols] $($ and $)$
+    \item[Connectives] $\land$ $\vee$ $\rightarrow$ $\leftrightarrow$ $\lnot$ $\bot$ $($ $)$
 \end{descriptionlist}
 
 \begin{description}
@@ -24,28 +23,31 @@ The symbols of propositional logic are:
         \end{itemize}
 
         Note that the implication $S_1 \rightarrow S_2$ can be written as $\lnot S_1 \vee S_2$.
+
+        The BNF definition of a formula is:
+        \[
+            F := \texttt{atomic\_proposition} \,|\, F \land F \,|\, F \vee F \,|\,  
+                F \rightarrow F \,|\, F \leftrightarrow F \,|\, \lnot F \,|\, (F) 
+        \]
+        % \[ 
+        %     \begin{split}
+        %         \texttt{<formula>} :=\,\, &\texttt{atomic\_proposition} \,|\,\\
+        %             &\lnot \texttt{<formula>} \,|\, \\
+        %             &\texttt{<formula>} \land \texttt{<formula>} \,|\, \\
+        %             &\texttt{<formula>} \vee \texttt{<formula>} \,|\, \\
+        %             &\texttt{<formula>} \rightarrow \texttt{<formula>} \,|\, \\
+        %             &\texttt{<formula>} \leftrightarrow \texttt{<formula>} \,|\, \\
+        %             &(\texttt{<formula>}) \\
+        %     \end{split}
+        % \]
 \end{description}
 
-\subsection{Propositional logic BNF}
-\[ 
-    \begin{split}
-        \texttt{<formula>} :=\,\, &\texttt{atomic\_proposition} \,|\,\\
-            &\lnot \texttt{<formula>} \,|\, \\
-            &\texttt{<formula>} \land \texttt{<formula>} \,|\, \\
-            &\texttt{<formula>} \vee \texttt{<formula>} \,|\, \\
-            &\texttt{<formula>} \rightarrow \texttt{<formula>} \,|\, \\
-            &\texttt{<formula>} \leftrightarrow \texttt{<formula>} \,|\, \\
-            &(\texttt{<formula>}) \\
-    \end{split}
-\]
-
-
 
 \section{Semantics}
 
 \begin{description}
     \item[Semantics] \marginnote{Semantics}
-        Rules to associate a meaning to well formed sentences.
+        Rules to associate a meaning to well-formed sentences.
         \begin{descriptionlist}
             \item[Model theory] What is true.
             \item[Proof theory] What is provable.
@@ -55,33 +57,21 @@ The symbols of propositional logic are:
 \begin{description}
     \item[Interpretation] \marginnote{Interpretation}
         Given a propositional formula $F$ of $n$ atoms $ \{ A_1, \dots, A_n \}$,
-        an interpretation $I$ of $F$ is an assignment of truth values to $\{ A_1, \dots, A_n \}$.
+        an interpretation $\mathcal{I}$ of $F$ is is a pair $(D, I)$ where:
+        \begin{itemize}
+            \item $D$ is the domain. Truth values in the case of propositional logic.
+            \item $I$ is the interpretation mapping that assigns
+                to the atoms $\{ A_1, \dots, A_n \}$ an element of $D$.
+        \end{itemize}
 
         Note: given a formula $F$ of $n$ distinct atoms, there are $2^n$ district interpretations.
 
         \begin{description}
             \item[Model] \marginnote{Model}
-                If $F$ is true under the interpretation $I$, 
-                we say that $I$ is a model of $F$ ($I \models F$).
+                If $F$ is true under the interpretation $\mathcal{I}$, 
+                we say that $\mathcal{I}$ is a model of $F$ ($\mathcal{I} \models F$).
         \end{description}
 
-
-    \item[Truth table] \marginnote{Truth table}
-        Useful to define the semantics of connectives.
-        \begin{itemize}
-            \item $\lnot S$ is true iff $S$ is false.
-            \item $S_1 \land S_2$ is true iff $S_1$ is true and $S_2$ is true.
-            \item $S_1 \vee S_2$ is true iff $S_1$ is true or $S_2$ is true.
-            \item $S_1 \rightarrow S_2$ is true iff $S_1$ is false or $S_2$ is true.
-            \item $S_1 \leftrightarrow S_2$ is true iff $S_1 \rightarrow S_2$ is true and $S_1 \leftarrow S_2$ is true.
-        \end{itemize}
-
-
-    \item[Evaluation] \marginnote{Evaluation order}
-        The connectives of a propositional formula are evaluated in the order:
-        \[ \leftrightarrow, \rightarrow, \vee, \land, \lnot \]
-        Formulas in parenthesis have higher priority.
-
     \item[Valid formula] \marginnote{Valid formula}
         A formula $F$ is valid (tautology) iff it is true in all the possible interpretations.
         It is denoted as $\models F$.
@@ -100,21 +90,40 @@ The symbols of propositional logic are:
         In other words, there is at least an interpretation where $F$ is true.
 
     \item[Decidability] \marginnote{Decidability}
-         A propositional formula is decidable if there is a terminating method to decide if it is valid.
+        A logic is decidable if there is a terminating method to decide if a formula is valid.
+
+        Propositional logic is decidable.
+
+    \item[Truth table] \marginnote{Truth table}
+        Useful to define the semantics of connectives.
+        \begin{itemize}
+            \item $\lnot S$ is true iff $S$ is false.
+            \item $S_1 \land S_2$ is true iff $S_1$ is true and $S_2$ is true.
+            \item $S_1 \vee S_2$ is true iff $S_1$ is true or $S_2$ is true.
+            \item $S_1 \rightarrow S_2$ is true iff $S_1$ is false or $S_2$ is true.
+            \item $S_1 \leftrightarrow S_2$ is true iff $S_1 \rightarrow S_2$ is true and $S_1 \leftarrow S_2$ is true.
+        \end{itemize}
+
+
+    \item[Evaluation] \marginnote{Evaluation order}
+        The connectives of a propositional formula are evaluated in the order:
+        \[ \leftrightarrow, \rightarrow, \vee, \land, \lnot \]
+        Formulas in parenthesis have higher priority.
 
    \item[Logical consequence] \marginnote{Logical consequence} 
-         Let $\Gamma = \{F_1, \dots, F_n\}$ be a set of formulas and $G$ a formula.
+        Let $\Gamma = \{F_1, \dots, F_n\}$ be a set of formulas (premises) and $G$ a formula (conclusion).
         $G$ is a logical consequence of $\Gamma$ ($\Gamma \models G$)
-         if in all the possible interpretations $I$, 
+        if in all the possible interpretations $\mathcal{I}$, 
         if $F_1 \land \dots \land F_n$ is true, $G$ is true.
 
    \item[Logical equivalence] \marginnote{Logical equivalence}
        Two formulas $F$ and $G$ are logically equivalent ($F \equiv G$) iff the truth values of $F$ and $G$
        are the same under the same interpretation.
-        In other words, $F \models G$ and $G \models F$.
+       In other words, $F \equiv G \iff F \models G \land G \models F$.
 
        Common equivalences are:
        \begin{descriptionlist}
+            \footnotesize
             \item[Commutativity]: $(P \land Q) \equiv (Q \land P)$ and $(P \vee Q) \equiv (Q \vee P)$
             \item[Associativity]: $((P \land Q) \land R) \equiv (P \land (Q \land R))$
                 and $((P \vee Q) \vee R) \equiv (P \vee (Q \vee R))$
@@ -128,56 +137,15 @@ The symbols of propositional logic are:
        \end{descriptionlist}
 \end{description}
 
-\begin{theorem}[Deduction] \marginnote{Deduction theorem}
-    Given a set of formulas $\{ F_1, \dots, F_n \}$ and a formula $G$:
-    \[ (F_1 \land \dots \land F_n) \models G \,\iff\, \models (F_1 \land \dots \land F_n) \rightarrow G \]
-
-    \begin{proof} \phantom{}
-        \begin{description}
-            \item[$\rightarrow$])
-                By hypothesis $(F_1 \land \dots \land F_n) \models G$.
-
-                So, for each interpretation $I$ in which $(F_1 \land \dots \land F_n)$ is true, $G$ is also true.
-                Therefore, $I \models (F_1 \land \dots \land F_n) \rightarrow G$.
-
-                Moreover, for each interpretation $I'$ in which $(F_1 \land \dots \land F_n)$ is false,
-                $(F_1 \land \dots \land F_n) \rightarrow G$ is true.
-                Therefore, $I' \models (F_1 \land \dots \land F_n) \rightarrow G$.
-
-                In conclusion, $\models (F_1 \land \dots \land F_n) \rightarrow G$.
-
-            \item[$\leftarrow$]) 
-                By hypothesis $\models (F_1 \land \dots \land F_n) \rightarrow G$.
-                Therefore, for each interpretation where $(F_1 \land \dots \land F_n)$ is true,
-                $G$ is also true.
-
-                In conclusion, $(F_1 \land \dots \land F_n) \models G$.
-        \end{description}
-    \end{proof}
-\end{theorem}
-
-\begin{theorem}[Refutation] \marginnote{Refutation theorem}
-    Given a set of formulas $\{ F_1, \dots, F_n \}$ and a formula $G$:
-    \[ (F_1 \land \dots \land F_n) \models G \,\iff\, F_1 \land \dots \land F_n \land \lnot G \text{ is inconsistent} \]
-
-    Note: this theorem is not accepted in intuitionistic logic.
-
-    \begin{proof}
-        By definition, $(F_1 \land \dots \land F_n) \models G$ iff for every interpretation where 
-        $(F_1 \land \dots \land F_n)$ is true, $G$ is also true.
-        This requires that there are no interpretations where $(F_1 \land \dots \land F_n)$ is true and $G$ false.
-        In other words, it requires that $(F_1 \land \dots \land F_n \land \lnot G)$ is inconsistent.
-    \end{proof}
-\end{theorem}
-
 
 \subsection{Normal forms}
+
 \begin{description}
     \item[Negation normal form (NNF)] \marginnote{Negation normal form}
-        A formula is in negation normal form iff negations appears only in front of atoms (i.e. not parenthesis).
+        A formula is in negation normal form iff negations appear only in front of atoms (i.e. not parenthesis).
         
     \item[Conjunctive normal form (CNF)] \marginnote{Conjunctive normal form}
-        A formula $F$ is in conjunctive normal form iff 
+        A formula $F$ is in conjunctive normal form iff:
         \begin{itemize}
             \item it is in negation normal form;
             \item it has the form $F := F_1 \land F_2 \dots \land F_n$, where each $F_i$ (clause) is a disjunction of literals.
@@ -189,19 +157,87 @@ The symbols of propositional logic are:
         \end{example}
 
     \item[Disjunctive normal form (DNF)] \marginnote{Disjunctive normal form}
-        A formula $F$ is in disjunctive normal form iff 
+        A formula $F$ is in disjunctive normal form iff:
         \begin{itemize}
             \item it is in negation normal form;
             \item it has the form $F := F_1 \vee F_2 \dots \vee F_n$, where each $F_i$ is a conjunction of literals.
         \end{itemize}
 \end{description}
 
-\section{Natural deduction}
 
+
+\section{Reasoning}
+
+\begin{description}
+    \item[Reasoning method] \marginnote{Reasoning method}
+        Systems to work with symbols.
+        
+        Given a set of formulas $\Gamma$, a formula $F$ and a reasoning method $E$,
+        we denote with $\Gamma \vdash^E F$ the fact that $F$ can be deduced from $\Gamma$
+        using the reasoning method $E$.
+
+        \begin{description}
+            \item[Sound] \marginnote{Soundness}
+                A reasoning method $E$ is sound iff:
+                \[ (\Gamma \vdash^E F) \rightarrow (\Gamma \models F) \]
+
+            \item[Complete] \marginnote{Completeness}
+                A reasoning method $E$ is complete iff:
+                \[ (\Gamma \models F) \rightarrow (\Gamma \vdash^E F) \]
+        \end{description}
+
+    \item[Deduction theorem] \marginnote{Deduction theorem}
+        Given a set of formulas $\{ F_1, \dots, F_n \}$ and a formula $G$:
+        \[ (F_1 \land \dots \land F_n) \models G \,\iff\, \models (F_1 \land \dots \land F_n) \rightarrow G \]
+        
+        \begin{proof} \phantom{}
+            \begin{description}
+                \item[$\rightarrow$])
+                    By hypothesis $(F_1 \land \dots \land F_n) \models G$.
+        
+                    So, for each interpretation $\mathcal{I}$ in which $(F_1 \land \dots \land F_n)$ is true, 
+                    $G$ is also true.
+                    Therefore, $\mathcal{I} \models (F_1 \land \dots \land F_n) \rightarrow G$.
+        
+                    Moreover, for each interpretation $\mathcal{I}'$ in which $(F_1 \land \dots \land F_n)$ is false,
+                    $(F_1 \land \dots \land F_n) \rightarrow G$ is true.
+                    Therefore, $\mathcal{I}' \models (F_1 \land \dots \land F_n) \rightarrow G$.
+        
+                    In conclusion, $\models (F_1 \land \dots \land F_n) \rightarrow G$.
+        
+                \item[$\leftarrow$]) 
+                    By hypothesis $\models (F_1 \land \dots \land F_n) \rightarrow G$.
+                    Therefore, for each interpretation where $(F_1 \land \dots \land F_n)$ is true,
+                    $G$ is also true.
+        
+                    In conclusion, $(F_1 \land \dots \land F_n) \models G$.
+            \end{description}
+        \end{proof}
+
+    \item[Refutation theorem] \marginnote{Refutation theorem}
+        Given a set of formulas $\{ F_1, \dots, F_n \}$ and a formula $G$:
+        \[ (F_1 \land \dots \land F_n) \models G \,\iff\, F_1 \land \dots \land F_n \land \lnot G \text{ is inconsistent} \]
+        
+        Note: this theorem is not accepted in intuitionistic logic.
+        
+        \begin{proof}
+            By definition, $(F_1 \land \dots \land F_n) \models G$ iff for every interpretation where 
+            $(F_1 \land \dots \land F_n)$ is true, $G$ is also true.
+            This requires that there are no interpretations where $(F_1 \land \dots \land F_n)$ is true and $G$ false.
+            In other words, it requires that $(F_1 \land \dots \land F_n \land \lnot G)$ is inconsistent.
+        \end{proof}
+\end{description}
+
+
+
+
+\subsection{Natural deduction}
 \begin{description}
     \item[Proof theory] \marginnote{Proof theory}
         Set of rules that allows to derive conclusions from premises by exploiting syntactic manipulations.
+\end{description}
 
+\begin{description}
     \item[Natural deduction] \marginnote{Natural deduction for propositional logic}
         Set of rules to introduce or eliminate connectives.
         We consider a subset $\{ \land, \rightarrow, \bot \}$ of functionally complete connectives.