diff --git a/src/ainotes.cls b/src/ainotes.cls index 5d97ee4..3eefd8a 100644 --- a/src/ainotes.cls +++ b/src/ainotes.cls @@ -19,6 +19,7 @@ \usepackage{acro} \usepackage{subcaption} \usepackage{eurosym} +\usepackage{bussproofs} % Deductive tree \geometry{ margin=3cm, lmargin=1.5cm, rmargin=4.5cm, marginparwidth=3cm } \hypersetup{ colorlinks, citecolor=black, filecolor=black, linkcolor=black, urlcolor=black, linktoc=all } diff --git a/src/languages-and-algorithms-for-ai/module2/ainotes.cls b/src/languages-and-algorithms-for-ai/module2/ainotes.cls new file mode 120000 index 0000000..146fd3c --- /dev/null +++ b/src/languages-and-algorithms-for-ai/module2/ainotes.cls @@ -0,0 +1 @@ +../../ainotes.cls \ No newline at end of file diff --git a/src/languages-and-algorithms-for-ai/module2/main.tex b/src/languages-and-algorithms-for-ai/module2/main.tex new file mode 100644 index 0000000..572a39d --- /dev/null +++ b/src/languages-and-algorithms-for-ai/module2/main.tex @@ -0,0 +1,11 @@ +\documentclass[11pt]{ainotes} + +\title{Languages and Algorithms for\\Artificial Intelligence\\(Module 2)} +\date{2023 -- 2024} + +\begin{document} + + \makenotesfront + \include{sections/_propositional_logic.tex} + +\end{document} \ No newline at end of file diff --git a/src/languages-and-algorithms-for-ai/module2/sections/_propositional_logic.tex b/src/languages-and-algorithms-for-ai/module2/sections/_propositional_logic.tex new file mode 100644 index 0000000..13332df --- /dev/null +++ b/src/languages-and-algorithms-for-ai/module2/sections/_propositional_logic.tex @@ -0,0 +1,284 @@ +\chapter{Propositional logic} + +\section{Syntax} +\begin{description} + \item[Syntax] \marginnote{Syntax} + 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 $)$ +\end{descriptionlist} + +\begin{description} + \item[Well-formed formula] \marginnote{Well-formed formula} + The definition of a well-formed formula is recursive: + \begin{itemize} + \item An atomic proposition is a well-formed formula. + \item If $S$ is well-formed, $\lnot S$ is well-formed. + \item If $S_1$ and $S_2$ are well-formed, $S_1 \land S_2$ is well-formed. + \item If $S_1$ and $S_2$ are well-formed, $S_1 \vee S_2$ is well-formed. + \end{itemize} + + Note that the implication $S_1 \rightarrow S_2$ can be written as $\lnot S_1 \vee S_2$. +\end{description} + +\subsection{Propositional logic BNF} +\[ + \begin{split} + \texttt{} :=\,\, &\texttt{atomic\_proposition} \,|\,\\ + &\lnot \texttt{} \,|\, \\ + &\texttt{} \land \texttt{} \,|\, \\ + &\texttt{} \vee \texttt{} \,|\, \\ + &\texttt{} \rightarrow \texttt{} \,|\, \\ + &\texttt{} \leftrightarrow \texttt{} \,|\, \\ + &(\texttt{}) \\ + \end{split} +\] + + + +\section{Semantics} + +\begin{description} + \item[Semantics] \marginnote{Semantics} + Rules to associate a meaning to well formed sentences. + \begin{descriptionlist} + \item[Model theory] What is true. + \item[Proof theory] What is provable. + \end{descriptionlist} +\end{description} + +\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 \}$. + + 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$). + \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$. + + \item[Invalid formula] \marginnote{Invalid formula} + A formula $F$ is invalid iff it is not valid {\tiny(\texttt{:o})}. + + In other words, there is at least an interpretation where $F$ is false. + + \item[Inconsistent formula] \marginnote{Inconsistent formula} + A formula $F$ is inconsistent (unsatisfiable) iff it is false in all the possible interpretations. + + \item[Consistent formula] \marginnote{Consistent formula} + A formula $F$ is consistent (satisfiable) iff it is not inconsistent. + + 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. + + \item[Logical consequence] \marginnote{Logical consequence} + Let $\Gamma = \{F_1, \dots, F_n\}$ be a set of formulas and $G$ a formula. + $G$ is a logical consequence of $\Gamma$ ($\Gamma \models G$) + if in all the possible interpretations $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$. + + Common equivalences are: + \begin{descriptionlist} + \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))$ + \item[Double negation elimination]: $\lnot(\lnot P) \equiv P$ + \item[Contraposition]: $(P \rightarrow Q) \equiv (\lnot Q \rightarrow \lnot P)$ + \item[Implication elimination]: $(P \rightarrow Q) \equiv (\lnot P \vee Q)$ + \item[Biconditional elimination]: $(P \leftrightarrow Q) \equiv ((P \rightarrow Q) \land (Q \rightarrow P))$ + \item[De Morgan]: $\lnot(P \land Q) \equiv (\lnot P \vee \lnot Q)$ and $\lnot(P \vee Q) \equiv (\lnot P \land \lnot Q)$ + \item[Distributivity of $\land$ over $\vee$]: $(P \land (Q \vee R)) \equiv ((P \land Q) \vee (P \land R))$ + \item[Distributivity of $\vee$ over $\land$]: $(P \vee (Q \land R)) \equiv ((P \vee Q) \land (P \vee R))$ + \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). + + \item[Conjunctive normal form (CNF)] \marginnote{Conjunctive normal form} + 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. + \end{itemize} + + \begin{example} \phantom{}\\ + $(\lnot P \vee Q) \land (\lnot P \vee R)$ is in CNF.\\ + $\lnot(P \vee Q) \land (\lnot P \vee R)$ is not in CNF (not in NNF). + \end{example} + + \item[Disjunctive normal form (DNF)] \marginnote{Disjunctive normal form} + 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} + +\begin{description} + \item[Proof theory] \marginnote{Proof theory} + Set of rules that allows to derive conclusions from premises by exploiting syntactic manipulations. + + \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. + + Natural deduction can be represented using a tree like structure: + \begin{prooftree} + \AxiomC{[hypothesis]} + \noLine + \UnaryInfC{\vdots} + \noLine + \UnaryInfC{premise} + \RightLabel{rule name}\UnaryInfC{conclusion} + \end{prooftree} + + The conclusion is true when the hypothesis are able to prove the premise. + Another tree can be built on top of premises to prove them. + + \begin{descriptionlist} + \item[Introduction] \marginnote{Introduction rules} + Usually used to prove the conclusion by splitting it.\\ + \begin{minipage}{.4\linewidth} + \begin{prooftree} + \AxiomC{$\psi$} + \AxiomC{$\varphi$} + \RightLabel{$\land$I}\BinaryInfC{$\varphi \land \psi$} + \end{prooftree} + \end{minipage} + \begin{minipage}{.4\linewidth} + \begin{prooftree} + \AxiomC{[$\varphi$]} + \noLine + \UnaryInfC{\vdots} + \noLine + \UnaryInfC{$\psi$} + \RightLabel{$\rightarrow$I}\UnaryInfC{$\varphi \rightarrow \psi$} + \end{prooftree} + \end{minipage} + + \item[Elimination] \marginnote{Elimination rules} + Usually used to exploit hypothesis and derive a conclusion.\\ + \begin{minipage}{.25\linewidth} + \begin{prooftree} + \AxiomC{$\varphi \land \psi$} + \RightLabel{$\land$E}\UnaryInfC{$\varphi$} + \end{prooftree} + \end{minipage} + \begin{minipage}{.25\linewidth} + \begin{prooftree} + \AxiomC{$\varphi \land \psi$} + \RightLabel{$\land$E}\UnaryInfC{$\psi$} + \end{prooftree} + \end{minipage} + \begin{minipage}{.3\linewidth} + \begin{prooftree} + \AxiomC{$\varphi$} + \AxiomC{$\varphi \rightarrow \psi$} + \RightLabel{$\rightarrow$E}\BinaryInfC{$\psi$} + \end{prooftree} + \end{minipage} + + \item[Ex falso sequitur quodlibet] \marginnote{Ex falso sequitur quodlibet} + From contradiction, anything follows. + This can be used when we have two contradicting hypothesis. + \begin{prooftree} + \AxiomC{$\bot$} + \RightLabel{$\bot$}\UnaryInfC{$\varphi$} + \end{prooftree} + + \item[Reductio ad absurdum] \marginnote{Reductio ad absurdum} + Assume the opposite and prove a contradiction (not accepted in intuitionistic logic). + \begin{prooftree} + \AxiomC{[$\lnot \varphi$]} + \noLine + \UnaryInfC{\vdots} + \noLine + \UnaryInfC{$\bot$} + \RightLabel{RAA}\UnaryInfC{$\varphi$} + \end{prooftree} + \end{descriptionlist} +\end{description} \ No newline at end of file