% $Id: introduction.tex 60862 2018-10-15 12:34:31Z torsten $
% $HeadURL: https://svn.cs.uni-potsdam.de/svn/reposWV/Lehre/ASP/trunk/Slides/introduction.tex $
% ----------------------------------------------------------------------
\lecture{Introduction}{introduction}
% ----------------------------------------------------------------------
\part{Introduction}
% ----------------------------------------------------------------------
\section{Syntax}
% ----------------------------------------------------------------------
\begin{frame}{Syntax}
\vfill
\begin{center}{%
\begin{picture}(300,120)(-150,-60)
\put(-80,+40){\makebox(0,0){\framebox(80,20){Problem}}}
\put(-80,-40){\makebox(0,0){\framebox(80,20){\alert{Logic Program}}}}
\put(+80,+40){\makebox(0,0){\framebox(80,20){Solution}}}
\put(+80,-40){\makebox(0,0){\framebox(80,20){Stable Models}}}
\put(-80,+30){\vector(0,-1){60}}
\put(-40,-40){\vector(+1,0){80}}
\put(+80,-30){\vector(0,+1){60}}
\put(-110,  0){\makebox(0,0){{Modeling}}}
\put(+120,  0){\makebox(0,0){{Interpreting}}}
\put(   0,-55){\makebox(0,0){{Solving}}}
\end{picture}}
\end{center}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Normal logic programs}
  \label{eqn:rule}
  \begin{itemize}
  \item <1->
    A \alert{logic program}, $\PRG$, over a set $\mathcal{A}$ of atoms is a finite \alert{set} of rules
  \item <1->
    A (normal) \alert{rule}, $r$, is of the form
    \[
      \alt<2>{\tt a_0\texttt{ :- } a_1,\dots,a_m,\texttt{ not }{a_{m+1}},\dots,\texttt{ not }{a_n}.}%
                  {a_0 \leftarrow   a_1,\dots,a_m,          \naf{a_{m+1}},\dots,          \naf{a_n}}
    \]
    where $0\leq m\leq n$ and each $a_i\in{\mathcal{A}}$ is an atom for $0\leq i\leq n$
    \pause
  \item <3->
    \structure{Notation}
    \begin{align*}
      \head{r}\phantom{^+}    &=\, a_0
      \\
      \body{r}\phantom{^+}    &=\, \{a_1,\dots,a_m,\naf{a_{m+1}},\dots,\naf{a_n}\}
      \\
      \pbody{r}               &=\, \{a_1,\dots,a_m\}
      \\
      \nbody{r}               &=\, \{a_{m+1},\dots,a_n\}
      \only<4>{%
      \\
      \atom{\PRG}\phantom{^+} &=\, \textstyle\bigcup_{r\in\PRG}\left(\{\head{r}\}\cup\pbody{r}\cup\nbody{r}\right)
      \\
      \body{\PRG}\phantom{^+} &=\, \{\body{r}\mid r\in\PRG\}
      \\
      \head{\PRG}\phantom{^+} & =\, \{\head{r}\mid r\in\PRG\}}
    \end{align*}%
  \item <5-> A \alert{literal} is an atom or a negated atom
  \item <6-> A program $\PRG$ is \alert{positive} if $\nbody{r}=\emptyset$ for all $r\in\PRG$
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Examples}
  \begin{itemize}
  \item<1-> \structure{Example rules}
    \begin{itemize}
    \item<1-> $a \leftarrow b, \naf{c}$
      \smallskip
    \item<1-> $a \leftarrow \naf{c}, b$
      \medskip
    \item<2-> $a \leftarrow           $
    \item<2-> $a \leftarrow b         $
    \item<2-> $a \leftarrow    \naf{c}$
      \medskip
    \item<3-> $\mathit{bachelor}(\mathit{joe}) \leftarrow \mathit{male}(\mathit{joe}), \naf{\mathit{married}(\mathit{joe})}$
    \end{itemize}
    \bigskip
  \item<4-> \structure{Example literals}
    \begin{itemize}
    \item<4-> $a,b,c,\mathit{bachelor}(\mathit{joe}), \mathit{male}(\mathit{joe}),\mathit{married}(\mathit{joe})$
      \smallskip
    \item<4-> $\naf{c}, \naf{\mathit{married}(\mathit{joe})}$
    \end{itemize}
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}[c]{Notational convention}

We sometimes use the following notation interchangeably
\\
in order to stress the respective view:

\bigskip{}

\begin{center}
  \begin{tabular}{|l|ccccccc|}
    \hline
                 &             &             &            &            &                 & default               & classical         \\
                 & true, false & if          & and        & or         & iff             &          negation     &           negation\\
                 \hline\hline
    source code  &             &\texttt{:-}  & \texttt{,} & \texttt{;} &                 & \texttt{not}          & \texttt{-}\\
    logic program&             &$\leftarrow$ & $,$        & $;$        &                 & $\sim$                & $\neg$\\
    formula      & $\bot,\top$ &$\rightarrow$& $\wedge$   & $\vee$     &$\leftrightarrow$& $\sim$                & $\neg$\\
    \hline
  \end{tabular}\end{center}
\end{frame}
% ----------------------------------------------------------------------
\section{Semantics}
% ----------------------------------------------------------------------
\begin{frame}{Semantics}
\vfill
\begin{center}{%
\begin{picture}(300,120)(-150,-60)
\put(-80,+40){\makebox(0,0){\framebox(80,20){Problem}}}
\put(-80,-40){\makebox(0,0){\framebox(80,20){Logic Program}}}
\put(+80,+40){\makebox(0,0){\framebox(80,20){Solution}}}
\put(+80,-40){\makebox(0,0){\framebox(80,20){\alert{Stable Models}}}}
\put(-80,+30){\vector(0,-1){60}}
\put(-40,-40){\vector(+1,0){80}}
\put(+80,-30){\vector(0,+1){60}}
\put(-110,  0){\makebox(0,0){{Modeling}}}
\put(+120,  0){\makebox(0,0){{Interpreting}}}
\put(   0,-55){\makebox(0,0){{Solving}}}
\end{picture}}
\end{center}
\end{frame}
% ----------------------------------------------------------------------
\input{\ASPSOURCE/Introduction/stable}
% ----------------------------------------------------------------------
\begin{frame}{Some properties}
  \bigskip
  \bigskip
  \begin{itemize}
  \item<1-> A logic program may have zero, one, or multiple stable models
    \medskip
    \medskip
  \item<3-> If $X$ is a stable model of a logic program $\PRG$,

    then $X\subseteq\head{P}$
    \medskip
  \item<3-> If $X$ is a stable model of a logic program $\PRG$,

    then $X$ is a (classical) model of $\PRG$
    \medskip
  \item<4-> If $X$ and $Y$ are stable models of a \emph{normal} program $\PRG$,

    then $X\not\subset Y$
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}[c]{Exemplars}
  \centering
  \begin{tabular}{|ll|l|}
    \hline
    \multicolumn{2}{|l|}{Logic program} & Answer sets\\
    \hline
    \hline
    \texttt{a.}          &                      & \{\texttt{a}\}\\
    \hline
    \texttt{a :- b.}     &                      & \{\}\\
    \hline
    \texttt{a :- b.}     & \texttt{b.}          & \{\texttt{a,b}\}\\
    \hline
    \texttt{a :- b.}     & \texttt{b :- a.}     & \{\}\\
    \hline
    \texttt{a :- not c.} &                      & \{\texttt{a}\}\\
    \hline
    \texttt{a :- not c.} & \texttt{c.}          & \{\texttt{c}\}\\
    \hline
    \texttt{a :- not c.} & \texttt{c :- not a.} & \{\texttt{a}\}, \{\texttt{c}\}\\
    \hline
    \texttt{a :- not a.} &                      & \\
    \hline
  \end{tabular}
\end{frame}
% ----------------------------------------------------------------------
\section{Reasoning}
% ----------------------------------------------------------------------
\begin{frame}{Reasoning modes}
\vfill
\begin{center}{%
\begin{picture}(300,120)(-150,-60)
\put(-80,+40){\makebox(0,0){\framebox(80,20){Problem}}}
\put(-80,-40){\makebox(0,0){\framebox(80,20){Logic Program}}}
\put(+80,+40){\makebox(0,0){\framebox(80,20){Solution}}}
\put(+80,-40){\makebox(0,0){\framebox(80,20){\alert{Stable Models}}}}
\put(-80,+30){\vector(0,-1){60}}
\put(-40,-40){\vector(+1,0){80}}
\put(+80,-30){\vector(0,+1){60}}
\put(-110,  0){\makebox(0,0){{Modeling}}}
\put(+120,  0){\makebox(0,0){{Interpreting}}}
\put(   0,-55){\makebox(0,0){{Solving}}}
\end{picture}}
\end{center}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Reasoning modes}
  \vfill
  \begin{itemize}
  \item Satisfiability
  \item Enumeration$^\dagger$
  \item Projection$^\dagger$
  \item Intersection$^\ddagger$
  \item Union$^\ddagger$
  \item Optimization
%  \item Sampling
    \medskip
  \item and combinations of them
  \end{itemize}
  \vfill
  {\footnotesize
  \begin{itemize}
  \item []\hfill $^\dagger$ without solution recording
  \item []\hfill $^\ddagger$ without solution enumeration
  \end{itemize}}
\end{frame}
% ----------------------------------------------------------------------
\section{Language}
% ----------------------------------------------------------------------
\begin{frame}{Extended syntax}
\vfill
\begin{center}{%
\begin{picture}(300,120)(-150,-60)
\put(-80,+40){\makebox(0,0){\framebox(80,20){Problem}}}
\put(-80,-40){\makebox(0,0){\framebox(80,20){\alert{Logic Program}}}}
\put(+80,+40){\makebox(0,0){\framebox(80,20){Solution}}}
\put(+80,-40){\makebox(0,0){\framebox(80,20){Stable Models}}}
\put(-80,+30){\vector(0,-1){60}}
\put(-40,-40){\vector(+1,0){80}}
\put(+80,-30){\vector(0,+1){60}}
\put(-110,  0){\makebox(0,0){{Modeling}}}
\put(+120,  0){\makebox(0,0){{Interpreting}}}
\put(   0,-55){\makebox(0,0){{Solving}}}
\end{picture}}
\end{center}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}[fragile]{Language constructs}
  \bigskip
  \begin{itemize}\itemsep 5pt
  \item<2-> \structure{Variables}             \hfill\alert<2>{\texttt{p(X) :- q(X)}}
  \item<3-> \structure{Conditional literals}  \hfill\texttt{p :- \alert<3>{q(X) : r(X)}}
  \item<4-> \structure{Disjunction}           \hfill\texttt{\alert<4>{p(X) ; q(X)} :- r(X)}
  \item<5-> \structure{Integrity constraints} \hfill\alert<5>{\texttt{:- q(X), p(X)}}
  \item<6-> \structure{Choice}                \hfill\texttt{\alert<6>{2 \{ p(X,Y) : q(X) \} 7} :- r(Y)}
  \item<7-> \structure{Aggregates}            \hfill\texttt{s(Y) :- r(Y), \alert<7>{2 \#sum\{ X : p(X,Y), q(X) \} 7}}
    \medskip
  \item<8-> \structure{\only<11->{Multi-objective o}\only<1-10>{O}ptimization}
    \begin{itemize}\normalsize
    \item< 9-> \structure{Weak constraints} \hfill\alert< 9>{\texttt{:$\mathtt{\sim}$ q(X), p(X,C) [C\only<11>{\alert{@42}}]}}
    \item<10-> \structure{Statements}       \hfill\alert<10>{\texttt{\#minimize \{ C\only<11>{\alert{@42}} : q(X), p(X,C) \}}}
    \end{itemize}
\end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\section{Variables}
% ----------------------------------------------------------------------
\begin{frame}[c]{Example}
  \[
    \begin{array}{l}
      d(a) \\
      d(c) \\
      d(d) \\[3pt]
      p(a,b) \\
      p(b,c) \\
      p(c,d) \\
      p(\alert<2>{X},\alert<2>{Z}) \leftarrow p(\alert<2>{X},\alert<2>{Y}), p(\alert<2>{Y},\alert<2>{Z}) \\[3pt]
      q(a) \\
      q(b) \\
      q(\alert<2>{X}) \leftarrow \naf r(\alert<2>{X}), d(\alert<2>{X}) \\[3pt]
      r(\alert<2>{X}) \leftarrow \naf q(\alert<2>{X}), d(\alert<2>{X}) \\[3pt]
      s(\alert<2>{X}) \leftarrow \naf r(\alert<2>{X}), p(\alert<2>{X},\alert<2>{Y}), q(\alert<2>{Y})
    \end{array}
  \]
  \bigskip
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Grounding instantiation}
  Let $\PRG$ be a logic program
  \begin{itemize}
  \item<1-> Let $\mathcal{T}$ be a set of \invisible<2>{(}variable-free\invisible<2>{)} \alert<1-2>{terms}\visible<2>{ (also called \alert{Herbrand universe})}
  \item<1-> Let $\mathcal{A}$ be a set of                (variable-free) \alert<1-2>{atoms} constructible from $\mathcal{T}$
    \only<2>{\\ (also called \alert{alphabet} or \alert{Herbrand base})}
    \smallskip
  \item<3-> A variable-free atom is also called \alert{ground}
    \medskip
  \item<4-> \alert<4>{Ground instances} of $r\in\PRG$\,: Set of variable-free rules obtained by
    replacing all variables in $r$ by elements from $\mathcal{T}$:
    \[
    \mathit{ground}(r)=\{r\theta\mid\theta:\mathit{var}(r)\rightarrow \mathcal{T} \text{ and } \mathit{var}(r\theta)=\emptyset\}
    \]
    where $\mathit{var}(r)$ stands for the set of all variables occurring in $r$;

    $\theta$ is a (ground) substitution
    \medskip
  \item<5-> \alert{Ground instantiation} of $\PRG$\,: \
    \(
    \mathit{ground}(\PRG)=\textstyle\bigcup_{r\in\PRG}\mathit{ground}(r)
    \)
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{An example}
  \small
  \[
  \begin{array}{@{}r@{\,}c@{\,}l}
    \PRG
    &=&
    \left\{
      \ r(a,b)\leftarrow, \ r(b,c)\leftarrow, \ t(X,Y) \leftarrow r(X,Y) \
    \right\}
    \\[1ex]
    \mathcal{T}&=&\{a,b,c\}
    \\[1ex]
    \mathcal{A}&=&\left\{
      \begin{array}{@{\,}c@{\,}}
        r(a,a),r(a,b),r(a,c), r(b,a),r(b,b),r(b,c), r(c,a),r(c,b),r(c,c),
        \\
        \!\! t(a,a),t(a,b),t(a,c), t(b,a),t(b,b),t(b,c), t(c,a),t(c,b),t(c,c)
      \end{array}
    \right\}
  \end{array}
  \]
  \pause
  \[
  \mathit{ground}(\PRG)
  =
  \left\{
    \begin{array}{l@{\,}c@{\,}l@{\,}l@{\,}c@{\,}l@{\,}l@{\,}c@{\,}l@{\,}}
      r(a,b)&\leftarrow&, &&&\\
      r(b,c)&\leftarrow&, &&&\\
      \onslide<-2>{t(a,a)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(a,a),}&\onslide<-2>{t(b,a)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(b,a),}&\onslide<-2>{t(c,a)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(c,a),}\\
                   t(a,b) &             \leftarrow & \alt<4->{,}{r(a,b),}&\onslide<-2>{t(b,b)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(b,b),}&\onslide<-2>{t(c,b)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(c,b),}\\
      \onslide<-2>{t(a,c)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(a,c),}&             t(b,c) &             \leftarrow &\onslide<-3>{r(b,c),}&\onslide<-2>{t(c,c)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(c,c)}
    \end{array}
  \right\}
  \]

  \begin{itemize}
  \item<5-> \alert{Grounding} aims at reducing the ground instantiation
  \end{itemize}

\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Safety}
  \bigskip
  \begin{itemize}
  \item A normal rule is \alert{safe}, if each of its variables also occurs in some positive body literal
    \medskip
  \item A normal program is safe, if all of its rules are safe
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}[c]{Example}
  \[
  \begin{array}{lcc}
         & \ & \only<2->{\alert<2>{\text{\ \ \textbf{Safe ?}}}}\\
    d(a) & & \only<3->{\OK}\\
    d(c) & & \only<3->{\OK}\\
    d(d) & & \only<3->{\OK}\\[3pt]
    p(a,b) & & \only<3->{\OK}\\
    p(b,c) & & \only<3->{\OK}\\
    p(c,d) & & \only<3->{\OK}\\
    p(X,Z) \leftarrow \alert<4>{p(X,Y)}, \alert<4>{p(Y,Z)} & & \only<5->{\OK}\\[3pt]
    q(a) & & \only<3->{\OK}\\
    q(b) & & \only<3->{\OK}\\
    q(X) \leftarrow \naf r(X)\only<7->{, d(X)} & & \only<6>{\KO}\only<7->{\OK}\\[3pt]
    r(X) \leftarrow \naf q(X), \alert<8>{d(X)} & & \only<9->{\OK}\\
    s(X) \leftarrow \naf r(X), \alert<10>{p(X,Y)}, \alert<10>{q(Y)} & & \only<11->{\OK}\\
  \end{array}
\]
\bigskip
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Stable models of programs with Variables}

  \bigskip

  Let $\PRG$ be a normal logic program with variables

  \bigskip
  \begin{itemize}
  \item<2->
  A set $X$ of (\alert{ground}) atoms is a \alert{stable model} of $\PRG$,
  \par\medskip
  if $\Cn{\reduct{\alert{\mathit{ground}(}\PRG\alert{)}}{X}}=X$
  \end{itemize}

\end{frame}
% ----------------------------------------------------------------------
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "asp"
%%% End:
