diff --git a/src/fundamentals-of-ai-and-kr/module2/img/allen_intervals.png b/src/fundamentals-of-ai-and-kr/module2/img/allen_intervals.png new file mode 100644 index 0000000..07a2bc7 Binary files /dev/null and b/src/fundamentals-of-ai-and-kr/module2/img/allen_intervals.png differ diff --git a/src/fundamentals-of-ai-and-kr/module2/main.tex b/src/fundamentals-of-ai-and-kr/module2/main.tex index f17b50d..56cc9c5 100644 --- a/src/fundamentals-of-ai-and-kr/module2/main.tex +++ b/src/fundamentals-of-ai-and-kr/module2/main.tex @@ -10,5 +10,6 @@ \input{sections/_ontologies.tex} \input{sections/_descriptive_logic.tex} \input{sections/_semantic_web.tex} + \input{sections/_time_reasoning.tex} \end{document} \ No newline at end of file diff --git a/src/fundamentals-of-ai-and-kr/module2/sections/_ontologies.tex b/src/fundamentals-of-ai-and-kr/module2/sections/_ontologies.tex index 6ac7cd9..7c9d3b3 100644 --- a/src/fundamentals-of-ai-and-kr/module2/sections/_ontologies.tex +++ b/src/fundamentals-of-ai-and-kr/module2/sections/_ontologies.tex @@ -58,11 +58,11 @@ \item[Necessity] \marginnote{Necessity} Members of a category enjoy some properties - (e.g. $(\text{x} \in \texttt{Car}) \rightarrow \texttt{hasWheels(x)}$). + (e.g. $(\text{x} \in \texttt{Car}) \Rightarrow \texttt{hasWheels(x)}$). \item[Sufficiency] \marginnote{Sufficiency} Sufficient conditions to be part of a category\\ - (e.g. $\texttt{hasPlate(x)} \land \texttt{hasWheels(x)} \rightarrow \texttt{x} \in \texttt{Car}$). + (e.g. $\texttt{hasPlate(x)} \land \texttt{hasWheels(x)} \Rightarrow \texttt{x} \in \texttt{Car}$). \item[Category-level properties] \marginnote{Category-level properties} Category themselves can enjoy properties\\ @@ -70,7 +70,7 @@ \item[Disjointness] \marginnote{Disjointness} Given a set of categories $S$, the categories in $S$ are disjoint iff they all have different objects: - \[ \texttt{disjoint($S$)} \iff (\forall c_1, c_2 \in S, c_1 \neq c_2 \rightarrow c_1 \cap c_2 = \emptyset) \] + \[ \texttt{disjoint($S$)} \iff (\forall c_1, c_2 \in S, c_1 \neq c_2 \Rightarrow c_1 \cap c_2 = \emptyset) \] \item[Exhaustive decomposition] \marginnote{Exhaustive decomposition} Given a category $c$ and a set of categories $S$, $S$ is an exhaustive decomposition of $c$ iff @@ -92,7 +92,7 @@ Objects (meronyms) are part of a whole (holonym). Properties: \begin{descriptionlist} - \item[Transitivity] $\texttt{partOf(x, y)} \land \texttt{partOf(y, z)} \rightarrow \texttt{partOf(x, z)}$ + \item[Transitivity] $\texttt{partOf(x, y)} \land \texttt{partOf(y, z)} \Rightarrow \texttt{partOf(x, z)}$ \item[Reflexivity] $\texttt{partOf(x, x)}$ \end{descriptionlist} diff --git a/src/fundamentals-of-ai-and-kr/module2/sections/_time_reasoning.tex b/src/fundamentals-of-ai-and-kr/module2/sections/_time_reasoning.tex new file mode 100644 index 0000000..128fc63 --- /dev/null +++ b/src/fundamentals-of-ai-and-kr/module2/sections/_time_reasoning.tex @@ -0,0 +1,214 @@ +\chapter{Quantitative time reasoning} + + +\section{Propositional logic} + +\begin{description} + \item[State] \marginnote{State} + The current state of the world can be represented as a set of propositions that are true according the observation of an agent. + + The union of a countable sequence of states represents the evolution of the world. Each proposition is distinguished by its time step. + + \begin{example} + A child has a bow and an arrow, then shoots the arrow. + \[ + \begin{split} + \text{KB}^0 &= \{ \texttt{hasBow}^0, \texttt{hasArrow}^0 \} \\ + \text{KB}^1 &= \{ \texttt{hasBow}^0, \texttt{hasArrow}^0, \texttt{hasBow}^1, \lnot\texttt{hasArrow}^1 \} + \end{split} + \] + \end{example} + + \item[Action] \marginnote{Action} + An action indicates how a state evolves into the next one. + It is described using effect axioms in the form: + \[ \texttt{action}^t \Rightarrow (\texttt{preconditions}^t \iff \texttt{effects}^{t+1}) \] + + \begin{description} + \item[Frame problem] \marginnote{Frame problem} + The effect axioms of an action do not tell what remains unchanged in the next state. + + \begin{description} + \item[Frame axioms] \marginnote{Frame axioms} + The frame axioms of an action describe the unaffected propositions of an action. + \end{description} + \end{description} + + \begin{example} + The action of shooting an arrow can be described as: + \[ + \begin{split} + \texttt{SHOOT}^t &\Rightarrow \{ \texttt{hasArrow}^t \iff \lnot\texttt{hasArrow}^{t+1} \} \\ + \texttt{SHOOT}^t &\Rightarrow \{ \texttt{hasBow}^t \iff \texttt{hasBow}^{t+1} \} + \end{split} + \] + \end{example} + + Note that with $m$ actions and $n$ propositions, the number of frame axioms will be of order $O(mn)$. + Inference for $t$ time steps will have complexity $O(nt)$. +\end{description} + + + +\section{Situation calculus (Green's formulation)} +Situation calculus uses first order logic instead of propositional logic. + +\begin{description} + \item[Situation] \marginnote{Situation} + The initial state is a situation. + Applying an action in a situation is a situation: + \[ s \text{ is a situation and } \texttt{a} \text{ is an action} \iff \texttt{result}(\texttt{a}, s) \text{ is situation} \] + (Note: in FAIRK module 1, \texttt{result} is denoted as \texttt{do}). + + \item[Fluent] \marginnote{Fluent} + Function that varies depending on the situation + (i.e. tells if a property holds in a given situation). + + \begin{example} + $\texttt{hasBow}(s)$ where $s$ is a situation. + \end{example} + + \item[Action] \marginnote{Action} + Actions are described using: + \begin{descriptionlist} + \item[Possibility axioms] \marginnote{Possibility axioms} + Indicates the preconditions $\phi_\texttt{a}$ of an action \texttt{a} in a given situation $s$: + \[ \phi_\texttt{a}(s) \Rightarrow \texttt{poss}(\texttt{a}, s) \] + + \item[Successor state axiom] \marginnote{Successor state axiom} + The evolution of a fluent $F$ follows the axiom: + \[ F^{t+1} \iff (\texttt{ActionCauses$(F)$} \vee (F^{t} \land \lnot\texttt{ActionCauses$(\lnot F)$})) \] + In other words, a fluent is true if an action makes it true or does not change if the action does not involve it. + + Adding the notion of possibility, an action can be described as: + \[ + \begin{split} + \texttt{poss}&(\texttt{a}, s) \Rightarrow \Big( F(\texttt{result}(\texttt{a}, s)) \iff \\ + & (\texttt{a} = \texttt{ActionCauses$(F)$}) \,\vee\, \\ + & (F(s) \,\land\, \texttt{a} \neq \lnot\texttt{ActionCauses$(\lnot F)$}) + \Big) + \end{split} + \] + + \item[Unique action axiom] \marginnote{Unique action axiom} + Only a single action can be executed in a situation to avoid non-determinism. + \end{descriptionlist} +\end{description} + + + +\section{Event calculus (Kowalski's formulation)} + +Event calculus reifies fluents and events (actions) as terms (instead of predicates). + +\begin{description} + \item[Event calculus ontology] \marginnote{Event calculus ontology} + A fixed set of predicates: + \begin{descriptionlist} + \item[$\texttt{holdsAt}(F, T)$] The fluent $F$ holds at time $T$. + \item[$\texttt{happens}(\texttt{E}, T)$] The event \texttt{E} (i.e. execution of an action) happened at time $T$. + \item[$\texttt{initiates}(\texttt{E}, F, T)$] The event \texttt{E} causes the fluent $F$ to start holding at time $T$. + \item[$\texttt{terminates}(\texttt{E}, F, T)$] The event \texttt{E} causes the fluent $F$ to cease holding at time $T$. + \item[$\texttt{clipped}(T_i, F, T_j)$] The fluent $F$ has been made false between the times $T_i$ and $T_j$ ($T_i < T_j$). + \item[$\texttt{initially}(F)$] The fluent $F$ holds at time 0. + \end{descriptionlist} + + \item[Domain-independent axioms] \marginnote{Domain-independent axioms} + A fixed set of axioms: + \begin{description} + \item[Truthness of a fluent] \phantom{} + \begin{enumerate} + \item A fluent holds if an event initiated it in the past and has not been clipped. + \[ + \begin{split} + \texttt{holdsAt}(F, T_j) \Leftarrow\, &\texttt{happens}(\texttt{E}, T_i) \land (T_i < T_j) \,\land\\ + &\texttt{initiates}(\texttt{E}, F, T_i) \land \lnot\texttt{clipped}(T_i, F, T_j) + \end{split} + \] + + \item A fluent holds if it was initially true and has not been clipped. + \[ \texttt{holdsAt}(F, T) \Leftarrow\, \texttt{initially}(F) \land \lnot\texttt{clipped}(0, F, T) \] + \end{enumerate} + Note: the negations make the definition of these axioms in Prolog unsafe. + + \item[Clipping of a fluent] + \[ \texttt{clipped}(T_i, F, T_j) \Leftarrow \texttt{happens}(\texttt{E}, T) \land (T_i < T < T_j) \land \texttt{terminates}(\texttt{E}, F, T) \] + \end{description} + + \item[Domain-dependent axioms] \marginnote{Domain-dependent axioms} + Domain-specific axioms defined using the predicates\\\texttt{initially}, \texttt{initiates} and \texttt{terminates}. +\end{description} + +\begin{description} + \item[Deductive reasoning] + Event calculus only allows deductive reasoning: + it takes as input the domain-dependant axioms and a set of events, and computes a set of true fluents. + If a new event is observed, the query need to be recomputed again. +\end{description} + + +\begin{example} + A room with a light and a button can be described as: + \begin{descriptionlist} + \item[Fluents] \texttt{lightOn} $\cdot$ \texttt{lightOff} + \item[Events] \texttt{PUSH\_BUTTON} + \end{descriptionlist} + + Domain-dependent axioms are: + \begin{descriptionlist} + \item[Initial state] \texttt{initially}(\texttt{lightOff}) + \item[Effects of \texttt{PUSH\_BUTTON} on \texttt{lightOn}] \phantom{} + \begin{itemize} + \item $\texttt{initiates}(\texttt{PUSH\_BUTTON}, \texttt{lightOn}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOff}, T)$ + \item $\texttt{terminates}(\texttt{PUSH\_BUTTON}, \texttt{lightOn}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOn}, T)$ + \end{itemize} + \item[Effects of \texttt{PUSH\_BUTTON} on \texttt{lightOff}] \phantom{} + \begin{itemize} + \item $\texttt{initiates}(\texttt{PUSH\_BUTTON}, \texttt{lightOff}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOn}, T)$ + \item $\texttt{terminates}(\texttt{PUSH\_BUTTON}, \texttt{lightOff}, T) \Leftarrow \texttt{holdsAt}(\texttt{lightOff}, T)$ + \end{itemize} + \end{descriptionlist} + + A set of events could be: + \[ \texttt{happens}(\texttt{PUSH\_BUTTON}, 3) \cdot \texttt{happens}(\texttt{PUSH\_BUTTON}, 5) \cdot \texttt{happens}(\texttt{PUSH\_BUTTON}, 6) \] +\end{example} + + +\subsection{Reactive event calculus} +\marginnote{Reactive event calculus} + +Allows to add events dynamically without the need to recompute the result. + + + +\section{Allen's logic of intervals} + +Event calculus only captures instantaneous events that happen in given points in time. + +\begin{description} + \item[Allen's logic of intervals] \marginnote{Allen's logic of intervals} + Reasoning on time intervals. + + \begin{description} + \item[Interval] \marginnote{Interval} + An interval $i$ starts at a time $\texttt{begin}(i)$ and ends at a time $\texttt{end}(i)$. + + \item[Temporal operators] \marginnote{Temporal operators} + \begin{itemize} + \item $\texttt{meet}(i, j) \iff \texttt{end}(i) = \texttt{begin}(j)$ + \item $\texttt{before}(i, j) \iff \texttt{end}(i) < \texttt{begin}(j)$ + \item $\texttt{after}(i, j) \iff \texttt{before}(j, i)$ + \item $\texttt{during}(i, j) \iff \texttt{begin}(j) < \texttt{begin}(i) < \texttt{end}(i) < \texttt{end}(j)$ + \item $\texttt{overlap}(i, j) \iff \texttt{begin}(i) < \texttt{begin}(j) < \texttt{end}(i) < \texttt{end}(j)$ + \item $\texttt{starts}(i, j) \iff \texttt{begin}(i) = \texttt{begin}(j)$ + \item $\texttt{finishes}(i, j) \iff \texttt{end}(i) = \texttt{end}(j)$ + \item $\texttt{equals}(i, j) \iff \texttt{starts}(i, j) \land \texttt{ends}(i, j)$ + \end{itemize} + + \begin{figure}[H] + \centering + \includegraphics[width=0.5\textwidth]{img/allen_intervals.png} + \caption{Visual representation of temporal operators} + \end{figure} + \end{description} +\end{description} \ No newline at end of file