% $Id: introduction.tex 36758 2013-07-10 07:16:04Z 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}{Problem solving in ASP: 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}
  \begin{itemize}
  \item <1->
    A % (normal)
               \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
    \[
    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 <2->
    \structure{Notation}
    \begin{eqnarray*}
      \head{r}   &=& a_0
      \\
      \body{r}   &=& \{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\}
      \\
      \atom{\PRG} &=& \textstyle\bigcup_{r\in\PRG}\left(\{\head{r}\}\cup\pbody{r}\cup\nbody{r}\right)
      \\
      \body{\PRG} &=& \{\body{r}\mid r\in\PRG\} 
    \end{eqnarray*}%
  \item <3-> A program $\PRG$ is \alert{positive} if $\nbody{r}=\emptyset$ for all $r\in\PRG$
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\begin{frame}[c]{Rough 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}{Problem solving in ASP: 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}
%------------------------------------------------------------
\begin{frame}[c]{Formal Definition\\
  \normalsize Stable models of positive programs}
  \begin{itemize}
  \item<2-> A set of atoms $X$ is \alert{closed under} a positive program $\Pi$ iff
    \\for any $r\in\Pi$, $\head{r}\in X$ whenever $\pbody{r}\subseteq X$
    \begin{itemize}
    \item $X$ corresponds to a model of $\Pi$ (seen as a formula)
    \end{itemize}
    \medskip
  \item<3-> The \alert{smallest} set of atoms which is closed under a positive
    program $\Pi$ is denoted by $\Cn{\Pi}$
    \begin{itemize}
    \item $\Cn{\Pi}$ corresponds to the $\subseteq$-smallest model of $\Pi$ (ditto)
    \end{itemize}
    \medskip
  \item<4-> The set $\Cn{\Pi}$ of atoms is the \alert{stable model} of a \emph{positive} program $\Pi$
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\begin{frame}{Some ``logical'' remarks}
  \begin{itemize}
  \item <1-> Positive rules are also referred to as \alert<1-2>{definite clauses}
    \begin{itemize}
    \item Definite clauses are disjunctions with \alert<1>{exactly one} positive atom:
      \[
      a_0\vee\neg a_1\vee\dots\vee\neg a_m
      \]
    \item A set of definite clauses has a (unique) \alert<3>{smallest model}
    \end{itemize}
    \medskip
  \item<2-> \alert<2>{Horn clauses} are clauses with \alert<2>{at most} one positive atom
    \begin{itemize}
    \item Every definite clause is a Horn clause but not vice versa
    \item Non-definite Horn clauses can be regarded as integrity constraints
      \smallskip
    \item A set of Horn clauses has a \alert<3>{smallest model} or none
    \end{itemize}
    \medskip
  \item<3-> This \alert<3>{smallest model} is the intended semantics of such sets of clauses
    \begin{itemize}
    \item Given a positive program $\Pi$,
    $\Cn{\Pi}$ corresponds to the smallest model of the set of
    definite clauses corresponding to $\Pi$
  \end{itemize}
\end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\begin{frame}{Basic idea}
\pause
\begin{columns}
  \begin{column}<1-7>[t]{0.6\linewidth}
    Consider the logical formula \alert<2>{$\Phi$}
    and its three (classical) models:
    \visible<3>{%
    \begin{picture}(0,0)(0,80)
      \alert{%
      \put(-50,50){\vector(2,-1){67}}
      \(
      \begin{array}{|rcl|}
        \hline
        p&\mapsto&1\\
        q&\mapsto&1\\
        r&\mapsto&0\\
        \hline
      \end{array}
      \)}
    \end{picture}}
    \[
    \alert<3>{\{p,q\}}, \{q,r\}, \text{ and }\{p,q,r\}  
    \]
  \end{column}
  \begin{column}<1-7>[t]{0.35\linewidth}
    \(\arrayrulewidth=.1pt
    \begin{array}[t]{l|c|}
      \cline{2-2}
      \alert<2,4>{\Phi}&    
      q
      \ \wedge \
      (q\wedge\neg r\to p)\\
      \cline{2-2}
    \end{array}
    \)
  \end{column}
\end{columns}

\bigskip

\uncover<5->{%
\begin{columns}
  \begin{column}<5-8>[t]{0.6\linewidth}
    Formula \alert<5>{$\Phi$} has one stable model,\\ often called \alert<5>{answer set}: 
    \[
    \alert<5>{\{p,q\}}
    \]
  \end{column}
  \begin{column}[t]{0.35\linewidth}
  \uncover<6-8>{%
    \(\arrayrulewidth=.1pt
    \begin{array}[t]{l|rcl|}
      \cline{2-4}
      \alert<6>{\Pi_\Phi}&
       q&\leftarrow&\\
      &\alert<8>{p}&\alert<8>{\leftarrow}& \alert<8>{q,\ \naf{r}}\\
      \cline{2-4}
    \end{array}
    \)}
\end{column}}
\end{columns}

\vfill

\uncover<7->{%
Informally, a set $X$ of atoms is a \alert{stable model} of a logic program $\Pi$
\begin{itemize}
\item if $X$ is a (classical) model of $\Pi$ 
  and
\item if all atoms in $X$ are \alert{justified} by some rule in $\Pi$
\end{itemize}
\pause
{\small (rooted in intuitionistic logics HT~(Heyting,~1930) and G3~(G\"odel,~1932))}
}
\end{frame}
%------------------------------------------------------------
\begin{frame}{Formal Definition\\
    \normalsize Stable model of normal programs}
  
  \begin{itemize}
  \item <1-> The \alert{reduct}, $\reduct{\Pi}{X}$, of a program $\Pi$ relative to
    a set $X$ of atoms is defined by
    \[
    \reduct{\Pi}{X}
    =
    \{\head{r}\leftarrow\pbody{r} \mid r\in \Pi \text{ and } \nbody{r}\cap X=\emptyset\}
    \]

  \item <2-> A set $X$ of atoms is a \alert{stable model} of a program $\Pi$,
    if $\Cn{\reduct{\Pi}{X}}=X$
    \bigskip
    \bigskip
  \item<3-> \structure{Note} $\Cn{\reduct{\Pi}{X}}$ is the $\subseteq$--smallest (classical) model of \reduct{\Pi}{X}
% \item<3-> \structure{Intuition:} $X$ is \alert{stable} under \emph{``applying rules from $\Pi$''}
  \item<3-> \structure{Note} Every atom in $X$ is justified by an \emph{``applying rule from $\Pi$''}
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\begin{frame}{A closer look at ${\reduct{\Pi}{X}}$}

  \bigskip
  \begin{itemize}
  \item<1-> 
    In other words, given a set $X$ of atoms from $\Pi$,
    
    \bigskip
    
    $\reduct{\Pi}{X}$ is obtained from $\Pi$ by \alert<1>{deleting} 
    \begin{enumerate}
    \item each \alert<1>{rule} having \alert<2>{\naf{a}} in its body with $a\in X$
      
      and then
    \item all \alert<1>{negative atoms} of the form \alert<2>{\naf{a}}  \\
      in the bodies of the remaining rules
    \end{enumerate}
    \bigskip
  \item<2-> \structure{Note} Only \alert<2>{negative body literals} are evaluated wrt $X$ 
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\section{Examples}
%------------------------------------------------------------
\begin{frame}{A first example}
\[
\Pi
=
\left\{
    p \leftarrow p, \ 
    q \leftarrow \only<-7>{\naf{p}}\only<8>{\alert{\neg p}}
\right\}
\]  
\pause
\newcommand{\PIip}{%
    \begin{array}[t]{lll}
      p &\leftarrow&p
      \\
       &&
    \end{array}}
\newcommand{\PIop}{%
    \begin{array}[t]{lll}
      p &\leftarrow&p
      \\
      q &\leftarrow&
    \end{array}}
\[
\begin{array}{c|cl|ccr}
       X                   &\ &\uncover<3->{\Pi^X}&\ &\Cn{\Pi^X}             &                              \\\hline
\{\phantom{p         ,q}\} &  &\uncover<3->{\PIop}&  &\uncover<3->{\{q\}}    &\uncover<4->{\KO}             \\\hline
\{         p\phantom{,q}\} &  &\uncover<3->{\PIip}&  &\uncover<3->{\emptyset}&  \only<5-7>{\KO}\only<8>{\OK}\\\hline
\{\phantom{p,}        q \} &  &\uncover<3->{\PIop}&  &\uncover<3->{\{q\}}    &\uncover<6->{\OK}             \\\hline
\{         p         ,q \} &  &\uncover<3->{\PIip}&  &\uncover<3->{\emptyset}&\uncover<7->{\KO} 
\end{array}
\]

\end{frame}
%------------------------------------------------------------
\begin{frame}{A second example}
\[
\Pi
=
\left\{
    p \leftarrow \only<-6>{\naf{q}}\only<7>{\alert{\neg q}}, \ 
    q \leftarrow \only<-6>{\naf{p}}\only<7>{\alert{\neg p}}
\right\}
\]  
\pause
% \newcommand{\PI}{%
%     \begin{array}[t]{lll}
%       p &\leftarrow& \naf{q}
%       \\
%       q &\leftarrow& \naf{p}
%     \end{array}}
\newcommand{\PIipiq}{%
    \begin{array}[t]{lll}
      &&
      \\
      &&
    \end{array}}
\newcommand{\PIipoq}{%
    \begin{array}[t]{lll}
      p &\leftarrow&
      \\
      &&
    \end{array}}
\newcommand{\PIopiq}{%
    \begin{array}[t]{lll}
      &&
      \\
      q &\leftarrow&
    \end{array}}
\newcommand{\PIopoq}{%
    \begin{array}[t]{lll}
      p &\leftarrow&
      \\
      q &\leftarrow&
    \end{array}}
\[
\begin{array}{c|cl|ccr}
       X                   &\ &{\Pi^X}&\ &\Cn{\Pi^X} &              \\\hline
\{\phantom{p         ,q}\} &  &\PIopoq&  &\{p,q\}    &\uncover<3->{\KO}\\\hline
\{         p\phantom{,q}\} &  &\PIipoq&  &\{p\}      &\uncover<4->{\OK}\\\hline
\{\phantom{p,}        q \} &  &\PIopiq&  &\{q\}      &\uncover<5->{\OK}\\\hline
\{         p         ,q \} &  &\PIipiq&  &\emptyset  &    \only<6>{\KO}\only<7>{\OK}
\end{array}
\]
\end{frame}
%------------------------------------------------------------
\begin{frame}{A third example}
\[
\Pi
=
\left\{
    p \leftarrow \only<-4>{\naf{p}}\only<5>{\alert{\neg p}}
\right\}
\]  
\pause\bigskip
% \newcommand{\PI}{%
%     \begin{array}[t]{lll}
%       p &\leftarrow& \naf{p}
%     \end{array}}
\newcommand{\PIip}{%
    \begin{array}[t]{l}
    \end{array}}
\newcommand{\PIop}{%
    \begin{array}[t]{l}
      p \leftarrow \
    \end{array}}
\[
\begin{array}{l|cl|ccr}
             X  &\ &\Pi^X&\ &\Cn{\Pi^X} &                  \\\hline
\{\phantom{p}\} &  &\PIop&  &\{p\}      &\uncover<3->{\KO} \\\hline
\{         p \} &  &\PIip&  &\emptyset  &    \only<4>{\KO}\only<5>{\OK}
\end{array}
\]
\bigskip
\end{frame}
%------------------------------------------------------------
\begin{frame}{Some properties}
\bigskip\bigskip
  \begin{itemize}
  \item<1-> A logic program may have zero, one, or multiple stable models!

  \item<2-> If $X$ is a  stable model of a logic program $\Pi$,

    then $X$ is a model of $\Pi$ (seen as a formula)
  \item<2-> If $X$ and $Y$ are stable models of a \emph{normal} program $\Pi$,

    then $X\not\subset Y$
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\section{Variables}
%------------------------------------------------------------
\begin{frame}{Programs with Variables}
  Let $\Pi$ 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} constructable from $\mathcal{T}$
    \visible<2>{\\ (also called \alert{alphabet} or \alert{Herbrand base})}
  \item<3-> \alert<3>{Ground Instances} of $r\in\Pi$: 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<4-> \alert{Ground Instantiation} of $\Pi$: \quad
    \(
    \mathit{ground}(\Pi)=\textstyle\bigcup_{r\in\Pi}\mathit{ground}(r)
    \)
  \end{itemize}
\end{frame}
%------------------------------------------------------------
\begin{frame}{An example}
  \small
  \[
  \begin{array}{@{}r@{\,}c@{\,}l}
    \Pi
    &=&
    \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}(\Pi)
  =
  \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&\onslide<-2>{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<-2>{r(b,c),}&\onslide<-2>{t(c,c)}&\onslide<-2>{\leftarrow}&\onslide<-2>{r(c,c)} \\
    \end{array}
  \right\}
  \]

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

\end{frame}
%------------------------------------------------------------
\begin{frame}{Stable models of programs with Variables}
  
  \bigskip

  Let $\Pi$ 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 $\Pi$,
  \par\medskip
  if $\Cn{\reduct{\alert{\mathit{ground}(}\Pi\alert{)}}{X}}=X$
  \end{itemize}

\end{frame}
% ----------------------------------------------------------------------
\section{Language constructs}
%------------------------------------------------------------
\begin{frame}{Problem solving in ASP: 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}
%\pause
  \begin{itemize}
  \item<2,8> \alert<8>{Variables} (over the Herbrand Universe)
    \begin{itemize}
    \item \alert<2>{\texttt{p(X) :- q(X)}} \ \ over constants \ \alert<2>{$\{\mathtt{a},\mathtt{b},\mathtt{c}\}$}
      stands for
      \\\qquad
      \alert<2>{\texttt{p(a) :- q(a), p(b) :- q(b), p(c) :- q(c)}}
    \end{itemize}
  \item<3,8> \alert<8>{Conditional Literals}
    \begin{itemize}
    \item \texttt{p :- \alert<3>{q(X) : r(X)}} \ \ given \ \texttt{\alert<3>{r(a)}, \alert<3>{r(b)}, \alert<3>{r(c)}}
      stands for
      \\\qquad
      \texttt{p :- \alert<3>{q(a), q(b), q(c)}}
     \end{itemize}
  \item<4> \alert<8>{Disjunction}
    \begin{itemize}
    \item \texttt{\alert<4>{p(X) | q(X)} :- r(X)}
    \end{itemize}
  \item<5,8> \alert<8>{Integrity Constraints}
    \begin{itemize}
    \item \alert<5>{\texttt{ :- q(X), p(X)}}
    \end{itemize}
  \item<6,8> \alert<8>{Choice}
    \begin{itemize}
    \item \texttt{\alert<6>{2 \{ p(X,Y) : q(X) \} 7} :- r(Y)}
    \end{itemize}
  \item<7,8> \alert<8>{Aggregates}
    \begin{itemize}
    \item \texttt{s(Y) :- r(Y), \alert<7>{2 \#count \{ p(X,Y) : q(X) \} 7}}
    \item also: \texttt{\#sum, \#avg, \#min, \#max, \#even, \#odd}
    \end{itemize}
  \end{itemize}
\end{frame}
% ----------------------------------------------------------------------
\section{Reasoning modes}
%------------------------------------------------------------
\begin{frame}{Problem solving in ASP: 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}
%------------------------------------------------------------
%%% Local Variables: 
%%% mode: latex
%%% TeX-PDF-mode: t 
%%% TeX-master: "asp"
%%% End: 
