diff --git a/src/fundamentals-of-ai-and-kr/module1/img/_moving_block_example_green.pdf b/src/fundamentals-of-ai-and-kr/module1/img/_moving_block_example_green.pdf
new file mode 100644
index 0000000..d97e742
Binary files /dev/null and b/src/fundamentals-of-ai-and-kr/module1/img/_moving_block_example_green.pdf differ
diff --git a/src/fundamentals-of-ai-and-kr/module1/img/_moving_block_example_kowalsky.pdf b/src/fundamentals-of-ai-and-kr/module1/img/_moving_block_example_kowalsky.pdf
new file mode 100644
index 0000000..1d36f90
Binary files /dev/null and b/src/fundamentals-of-ai-and-kr/module1/img/_moving_block_example_kowalsky.pdf differ
diff --git a/src/fundamentals-of-ai-and-kr/module1/sections/_planning.tex b/src/fundamentals-of-ai-and-kr/module1/sections/_planning.tex
index 8c83ec1..e50c2c8 100644
--- a/src/fundamentals-of-ai-and-kr/module1/sections/_planning.tex
+++ b/src/fundamentals-of-ai-and-kr/module1/sections/_planning.tex
@@ -83,8 +83,224 @@ Produces a totally ordered list of actions.
 
 The direction of the search can be:
 \begin{descriptionlist}
-    \item[Forward] 
+    \item[Forward] \marginnote{Forward search}
         Starting from the initial state, the search terminates when a state containing a superset of the goal is reached.
-    \item[Backward] 
+    \item[Backward] \marginnote{Backward search}
         Starting from the goal, the search terminates when a state containing a subset of the initial state is reached.
-    \end{descriptionlist}
\ No newline at end of file
+
+        Goal regression is used to reduce the goal into sub-goals.
+        Given a (sub-)goal $G$ and a rule (action) $R$ with delete-list (states that are false after the action) \texttt{d\_list}
+        and add-list (states that are true after the action) \texttt{a\_list}, regression of $G$ through $R$ is define as:
+        \[
+            \begin{split}
+                \texttt{regr[$G$, $R$]} &= \texttt{true} \text{ if } G \in \texttt{a\_list} \text{ (i.e. regression possible)} \\
+                \texttt{regr[$G$, $R$]} &= \texttt{false} \text{ if } G \in \texttt{d\_list} \text{ (i.e. regression not possible)} \\
+                \texttt{regr[$G$, $R$]} &= G \text{ otherwise} \text{ (i.e. $R$ does not influence $G$)} \\
+            \end{split}  
+        \]
+
+        \begin{example}[Moving blocks]
+            Given the action \texttt{unstack(X, Y)} with:
+            \[
+                \begin{split}
+                    \texttt{d\_list} &= \{ \texttt{handempty}, \texttt{on(X, Y)}, \texttt{clear(X)} \} \\
+                    \texttt{a\_list} &= \{ \texttt{holding(X)}, \texttt{clear(Y)} \}
+                \end{split}
+            \]
+            We have that:
+            \[
+                \begin{split}
+                    \texttt{regr[holding(b), unstack(b, Y)]} &= \texttt{true} \\
+                    \texttt{regr[handempty, unstack(X, Y)]}  &= \texttt{false} \\
+                    \texttt{regr[ontable(c), unstack(X, Y)]} &= \texttt{ontable(c)} \\
+                    \texttt{regr[clear(c), unstack(X, Y)]} &= \begin{cases}
+                        \texttt{true} & \text{if \texttt{Y}=\texttt{c}} \\
+                        \texttt{clear(c)} & \text{otherwise}
+                    \end{cases}
+                \end{split}  
+            \]
+        \end{example}
+\end{descriptionlist}
+
+
+\subsection{Deductive planning}
+\marginnote{Deductive planning}
+Formulates the planning problem using first order logic to represent states, goals and actions.
+Plans are generated as theorem proofs.
+
+\subsubsection{Green's formulation}
+\marginnote{Green's formulation}
+Green's formulation is based on \textbf{situation calculus}.
+To find a plan, the goal is negated and it is proven that it leads to an inconsistency.
+
+The main concepts are:
+\begin{descriptionlist}
+    \item[Situation]
+        Properties (fluents) that hold in a given state \texttt{s}.
+        \begin{example}[Moving blocks]
+            To denote that \texttt{ontable(c)} holds in a state \texttt{s}, we use the axiom:
+            \[ \texttt{ontable(c, s)} \]
+        \end{example}
+        The operator \texttt{do} allows to evolve the state such that:
+        \[ \texttt{do(A, S)} = \texttt{S'} \]
+        \texttt{S'} is the new state obtained by applying the action \texttt{A} in the state \texttt{S}.
+
+    \item[Actions]
+        Define the pre-condition and post-condition fluents of an action in the form:
+        \[ \texttt{pre-conditions} \rightarrow \texttt{post-conditions} \]
+        Applying the equivalence $A \rightarrow B \equiv \lnot A \vee B$, actions can be described by means of disjunctions.
+        \begin{example}[Moving blocks]
+            The action \texttt{stack(X, Y)} has pre-conditions \texttt{holding(X)} and \texttt{clear(Y)}, and
+            post-conditions \texttt{on(X, Y)}, \texttt{clear(X)} and \texttt{handfree}.
+            Its representation in Green's formulation is:
+            \[
+                \begin{split}
+                    \texttt{holding(X, S)} \land \texttt{clear(Y, S)} &\rightarrow \\
+                    &\texttt{on(X, Y, do(stack(X, Y), s))} \land \\
+                    &\texttt{clear(X, do(stack(X, Y), s))} \land \\
+                    &\texttt{handfree(do(stack(X, Y), s))} \\
+                \end{split}
+            \]
+        \end{example}
+
+    \item[Frame axioms]
+        Besides the effects of actions, each state also have to define for all non-changing fluents their frame axioms.
+        If the problem is complex, the number of frame axioms becomes unreasonable.
+        \begin{example}[Moving blocks]
+            \[ \texttt{on(U, V, S)}, \texttt{diff(U, X)} \rightarrow \texttt{on(U, V, do(move(X, Y, Z), S))} \]
+        \end{example}
+\end{descriptionlist}
+
+
+\begin{example}[Moving blocks]
+    The initial state is described by the following axioms:\\[0.5em]
+    \begin{minipage}{.3\linewidth}
+        \centering
+        \texttt{on(a, d, s0)} \\
+        \texttt{on(b, e, s0)} \\
+        \texttt{on(c, f, s0)} \\
+        \texttt{clear(a, s0)} \\
+        \texttt{clear(b, s0)} \\
+    \end{minipage}
+    \begin{minipage}{.3\linewidth}
+        \centering
+        \texttt{clear(c, s0)} \\
+        \texttt{clear(g, s0)} \\
+        \texttt{diff(a, b)} \\
+        \texttt{diff(a, c)} \\
+        \texttt{diff(a, d)} \dots \\
+    \end{minipage}
+    \begin{minipage}{.3\linewidth}
+        \centering
+        \includegraphics[width=\linewidth]{img/_moving_block_example_green.pdf}
+    \end{minipage}\\[0.5em]
+
+    For simplicity, we only consider the action \texttt{move(X, Y, Z)} that moves \texttt{X} from \texttt{Y} to \texttt{Z}.
+    It is defined as:
+    \[ 
+        \begin{split}
+            \texttt{clear(X, S)}&, \texttt{clear(Z, S)}, \texttt{on(X, Y, S)}, \texttt{diff(X, Z)} \rightarrow \\
+            &\texttt{clear(Y, do(move(X, Y, Z), S))}, \texttt{on(X, Z, do(move(X, Y, Z), S))}
+        \end{split}
+    \]
+    This action can be translated into the following effect axioms:
+    \[ 
+        \begin{split}
+            \lnot\texttt{clear(X, S)} &\vee \lnot\texttt{clear(Z, S)} \vee \lnot\texttt{on(X, Y, S)} \vee \lnot\texttt{diff(X, Z)} \vee \\
+            &\texttt{clear(Y, do(move(X, Y, Z), S))}
+        \end{split}
+    \]
+    \[ 
+        \begin{split}
+            \lnot\texttt{clear(X, S)} &\vee \lnot\texttt{clear(Z, S)} \vee \lnot\texttt{on(X, Y, S)} \vee \lnot\texttt{diff(X, Z)} \vee \\
+            &\texttt{on(X, Z, do(move(X, Y, Z), S))}
+        \end{split}
+    \]
+\end{example}
+
+Given the goal \texttt{on(a, b, s1)}, we prove that $\lnot\texttt{on(a, b, s1)}$ leads to an inconsistency.
+We decide to make the following substitutions: 
+\[ \{ \texttt{X}/\texttt{a}, \texttt{Z}/\texttt{b}, \texttt{s1}/\texttt{do(move(a, Y, b), S)} \} \]
+The premise of \texttt{move} leads to an inconsistency (when applying \texttt{move} its premise is false):
+\begin{center}
+    \begin{tabular}{c|c|c|c}
+        $\lnot\texttt{clear(a, S)}$ & $\lnot\texttt{clear(b, S)}$ & $\lnot\texttt{on(a, Y, S)}$ & $\lnot\texttt{diff(a, b)}$ \\
+        False with $\{ \texttt{S}/\texttt{s0} \}$ & False with $\{ \texttt{S}/\texttt{s0} \}$ 
+            & False with $\{ \texttt{S}/\texttt{s0}, \texttt{Y}/\texttt{d} \}$ & False
+    \end{tabular}
+\end{center}
+Therefore, the substitution $\{ \texttt{s1}/\texttt{do(move(a, Y, b), S)} \}$ defines the plan to reach the goal \texttt{on(a, b, s1)}.
+
+
+\subsubsection{Kowalsky's formulation}
+\marginnote{Kowalsky's formulation}
+Kowalsky's formulation avoids the frame axioms problem by using a set of fixed predicates:
+\begin{descriptionlist}
+    \item[\texttt{holds(rel, s/a)}] 
+        Describes the relations \texttt{rel} that are true in a state \texttt{s} or after the execution of an action \texttt{a}.
+    \item[\texttt{poss(s)}]
+        Indicates if a state \texttt{s} is possible.
+    \item[\texttt{pact(a, s)}]  
+        Indicates if an action \texttt{a} can be executed in a state \texttt{s}.
+\end{descriptionlist}
+Actions can be described as:
+\[ \texttt{poss(S)} \land \texttt{pact(A, S)} \rightarrow \texttt{poss(do(A, S))} \]
+
+In the Kowalsky's formulation, each action requires a frame assertion (in Green's formulation, each state requires frame axioms).
+
+\begin{example}[Moving blocks]
+    An initial state can be described by the following axioms:\\[0.5em]
+    \begin{minipage}{.35\linewidth}
+        \centering
+        \texttt{holds(on(a, b), s0)} \\
+        \texttt{holds(ontable(b), s0)} \\
+        \texttt{holds(ontable(c), s0)} \\
+    \end{minipage}
+    \begin{minipage}{.35\linewidth}
+        \centering
+        \texttt{holds(clear(a), s0)} \\
+        \texttt{holds(clear(c), s0)} \\
+        \texttt{holds(handempty, s0)} \\
+        \texttt{poss(s0)} \\
+    \end{minipage}
+    \begin{minipage}{.2\linewidth}
+        \centering
+        \includegraphics[width=0.6\linewidth]{img/_moving_block_example_kowalsky.pdf}
+    \end{minipage}\\[0.5em]
+\end{example}
+
+\begin{example}[Moving blocks]
+    The action \texttt{unstack(X, Y)} has:
+    \begin{descriptionlist}
+        \item[Pre-conditions] \texttt{on(X, Y)}, \texttt{clear(X)} and \texttt{handempty}
+        \item[Effects] \phantom{}
+        \begin{description}
+            \item[Add-list] \texttt{holding(X)} and \texttt{clear(Y)}
+            \item[Delete-list] \texttt{on(X, Y)}, \texttt{clear(X)} and \texttt{handempty}
+        \end{description}
+    \end{descriptionlist}
+
+    Its description in Kowalsky's formulation is:
+    \begin{descriptionlist}
+        \item[Pre-conditions] 
+            \[ 
+                \begin{split}
+                    \texttt{holds(on(X, Y), S)}&, \texttt{holds(clear(X), S)}, \texttt{holds(handempty, S)} \rightarrow \\
+                    &\texttt{pact(unstack(X, Y), S)} 
+                \end{split}
+            \]
+        
+        \item[Effects] (use add-list)
+            \[ \texttt{holds(holding(X), do(unstack(X, Y), S))} \]
+            \[ \texttt{holds(clear(Y), do(unstack(X, Y), S))} \]
+        
+        \item[Frame condition] (uses delete-list)
+            \[ 
+                \begin{split}
+                    \texttt{holds(V, S)}&, \texttt{V} \neq \texttt{on(X, Y)}, \texttt{V} \neq \texttt{clear(X)}, \texttt{V} \neq \texttt{handempty}
+                    \rightarrow \\
+                    & \texttt{holds(V, do(unstack(X, Y), S))}
+                \end{split}
+            \]
+    \end{descriptionlist}
+\end{example}
\ No newline at end of file