From 3cde7dad633f8977b6eb6f38ae6df797579703a5 Mon Sep 17 00:00:00 2001
From: Giovanni Ciatto <giovanni.ciatto@unibo.it>
Date: Tue, 15 Mar 2022 10:35:32 +0100
Subject: [PATCH] fix: minor aspects

---
 ise-lab-knowledge-representation.tex | 34 ++++++++++++++++++++++++----
 1 file changed, 30 insertions(+), 4 deletions(-)

diff --git a/ise-lab-knowledge-representation.tex b/ise-lab-knowledge-representation.tex
index f09ee7e..b933497 100644
--- a/ise-lab-knowledge-representation.tex
+++ b/ise-lab-knowledge-representation.tex
@@ -14,7 +14,7 @@
 % version
 \newcommand{\versionmajor}{1}
 \newcommand{\versionminor}{0}
-\newcommand{\versionpatch}{0}
+\newcommand{\versionpatch}{1}
 \newcommand{\version}{\versionmajor.\versionminor.\versionpatch}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \title[\currentLab{} -- Knowledge Representation]{Knowledge Representation with Horn Clauses}
@@ -130,7 +130,8 @@ \section{Premises}
             \item[ie] an algorithm for decising the \alert{unsatisfiability} of FOL formul\ae{} in \alert{Skolemized form}
             %
             \begin{itemize}
-                \item Skolem form $\approx$ all variables are \alert{universally} quantified at the beginning of the formula
+                \item[ie] all variables are \alert{universally} quantified at the beginning of the formula
+                \item[cf] \uurl{https://mathworld.wolfram.com/SkolemizedForm.html} 
             \end{itemize}
 
             \item SL = Selective Linear
@@ -308,7 +309,7 @@ \subsection{Terms}
             \item $\variable{X}$ is a variable
             \item $\functor{s}(\variable{X})$, $\functor{s}(\functor{z})$, etc. are structures
             \item $\mathcal{F} = \{ \functor{s}, \functor{z} \}$ \hfill {\footnotesize(where $\functor{s}$ is a 1-ary functor, while $\functor{z}$ is 0-ary)}
-            \item $\mathcal{V} = \{ \functor{X} \}$
+            \item $\mathcal{V} = \{ \variable{X} \}$
         \end{itemize}
     \end{exampleblock}
 \end{frame}
@@ -761,6 +762,25 @@ \subsection{Horn Clauses}
     \end{exampleblock}
 \end{frame}
 
+\begin{frame}{Skip to Exercises} 
+    \begin{block}{You may already start some exercises}
+        \begin{enumerate}
+            \item exercise about terms on slide \ref{slide:first-exercise-on-terms}
+            \item exercise about Herbrand universe on slide \ref{slide:second-exercise-on-terms}
+            \item exercise about clauses on slide \ref{slide:first-exercise-on-clauses}
+            \item exercise about theories on slide \ref{slide:second-exercise-on-clauses}
+        \end{enumerate}
+    \end{block}
+
+    \begin{alertblock}{Prerequisites}
+        \begin{itemize}
+            \item consider reading slide \ref{slide:prolog} (relevant Prolog-related aspects)
+            \item consider reading slide \ref{slide:tuprolog-overview} (relevant \twopkt{}-related aspects)
+        \end{itemize}
+        before proceeding with exercises
+    \end{alertblock}
+\end{frame}
+
 %===============================================================================
 \section{Flexibility of Logic Representation}
 %===============================================================================
@@ -1038,6 +1058,7 @@ \section{About Horn Clauses in Prolog}
 %===============================================================================
 
 \begin{frame}{Prolog Overview}
+\label{slide:prolog}
     \begin{itemize}
         \item Most relevant language in the \alert{logic programming} playground
 
@@ -1125,6 +1146,7 @@ \section{Practice}
 \subsection{\tuprolog{} and \twopkt{}}
 
 \begin{frame}{\twopkt{} Overview}
+\label{slide:tuprolog-overview}
     \begin{itemize}
         \item Multi-platform, Kotlin-based reboot of \tuprolog{}
         %
@@ -1224,6 +1246,7 @@ \subsection{Exercises on terms}
 \startExercise{}
 
 \begin{frame}{\currentExercise{} -- Terms construction}
+    \label{slide:first-exercise-on-terms}
 
     \begin{block}{Goal}
         Understand the basics of terms construction in \twopkt{}
@@ -1234,6 +1257,8 @@ \subsection{Exercises on terms}
 \startExercise{}
 
 \begin{frame}{\currentExercise{} -- Herbrand Universe}
+    \label{slide:second-exercise-on-terms}
+
     \begin{block}{Goal}
         \begin{itemize}
             \item Implement the algorithm for constructing the Herbrand Universe \ldots
@@ -1262,7 +1287,7 @@ \subsection{Exercises on Horn clauses}
 \startExercise{}
 
 \begin{frame}{\currentExercise{} -- Clauses construction}
-
+    \label{slide:first-exercise-on-clauses}
     \begin{block}{Goal}
         Understand the basics of clauses and theories construction in \twopkt{}
     \end{block}
@@ -1272,6 +1297,7 @@ \subsection{Exercises on Horn clauses}
 \startExercise{}
 
 \begin{frame}{\currentExercise{} -- Theory Analysis}
+    \label{slide:second-exercise-on-clauses}
     \begin{block}{Goal}
         \begin{itemize}
             \item Write an algorithm aimed at inspecting a theory, in order to compute: