\documentclass[slideColor,colorBG,semrot,semlayer,semcolor,portrait,pdf,talk]{prosper}
%\documentclass[slideBW,nocolorBG,accumulate,semrot,semlayer,semcolor,portrait,ps,talk]{prosper}
\DeclareMathVersion{bold} %%%%%%%%%%% WM for prosper
\usepackage{german}
\usepackage{url}
\input{seminar.bug}
%\slideframe{none}
\slidesmag{3}
\usepackage{moreverb}
\usepackage{latexsym,pstricks,pst-node,pst-coil,epsf,dbicons}

\psset{linewidth=1pt}

\usepackage{version}
\includeversion{comments}
\renewcommand{\familydefault}{phv}

\newif\ifblackwhite 
\blackwhitefalse
%\blackwhitetrue
\ifblackwhite
  \newhsbcolor{lightred}{0 0 0}
\else
  \newrgbcolor{lightred}{1.00 0.4 0.4}
\fi

\def\headertext{\sl Nichtmonotone Vererbung und Default Logic\hfill}
\def\footertext{\theslide}

%\newpagestyle{myslides}
% {\blue\makebox[\textwidth]{\raisebox{0.8em}{\small\headertext}}\hspace*{-\textwidth}\raisebox{.3em}{\rule{\textwidth}{0.3pt}}}
% {\blue\raisebox{1.5em}{}%
%   \raisebox{-1em}{\makebox[\textwidth]{\small\footertext}\hspace*{-\textwidth}}%
%   \raisebox{.5em}{\rule{\textwidth}{0.3pt}}}
%\pagestyle{myslides}
\newgray{normalgray}{0.45}
\newgray{lightgray}{0.55}
\newgray{verylightgray}{0.65}
\newgray{superlightgray}{0.85}

\renewcommand{\nodeconnections}[1]{\hbox to 0cm{\vbox to 0cm {#1}}}

\newcommand{\fd}{\mbox{$\rightarrow$}}                      % scalar
\newcommand{\Fd}{\mbox{$\Rightarrow$}}                      % scalar
\newcommand{\bfd}{\mbox{$\bullet\!\!\!\fd$}}                % " + inheritable
\newcommand{\mvd}{\mbox{$\rightarrow\!\!\!\!\rightarrow$}}  % multivalued
\newcommand{\Mvd}{\mbox{$\Rightarrow\!\!\!\!\Rightarrow$}}  % multivalued
\newcommand{\bmvd}{\mbox{$\bullet\!\!\!\mvd$}}              % " + inheritable
\newcommand{\isa}{\ensuremath{\;\mbox{isa}\;}}
\newcommand{\subcl}{\ensuremath{\;\mbox{subcl}\;}}
\newcommand{\la}{\ensuremath{\gets}}
\newcommand{\sem}[1]{\ensuremath{[\![#1]\!]}}         % eckige Doppelklammer
\newcommand{\pl}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\closure}{\ensuremath{\mathcal{C\!\ell}}}
\newcommand{\join}{\bowtie}
\newcommand{\smallvdots}{:}
\newcommand{\TX}{T\!\!X}
\newcommand{\Th}{\mbox{Th}}
\newcommand{\st}{\ensuremath{\ |\ }} % Trennzeichen f"ur Mengen 'such that'
\newcommand{\snake}{\mathrel{{\scriptstyle\mid\!\!\sim}}}
\newcommand{\flrule}[1]{\mbox{#1}}
\newcommand{\rem}[1]{\hfill \quad\textrm{\textit{\% #1}}\ignorespaces}

\newcommand{\Var}{\mbox{Var}}
\newcommand{\DefIff}{~:\Leftrightarrow~}
\newcommand{\Iff}{~\Leftrightarrow~}
\newcommand{\Imp}{~\Rightarrow~}
\newcommand{\imp}{\rightarrow}
\renewcommand{\iff}{\leftrightarrow}

\newenvironment{expl}%
  {\begin{quote}
   \begin{tabular}[b]{l@{}l@{}l}}%
  {\end{tabular} \end{quote}}


%% aus german.sty
\makeatletter
\def\save@sf@q#1{{\ifhmode
  \edef\@SF{\spacefactor\the\spacefactor}\else
  \let\@SF\empty \fi \leavevmode #1\@SF}}
\def\@flq{\relax\ifmmode <\else \save@sf@q{\penalty\@M
    \raise .27ex\hbox{$\m@th\scriptscriptstyle <$}}\fi}
\def\flq{\protect\@flq}
\def\@frq{\relax\ifmmode >\else \save@sf@q{\penalty\@M
    \raise .27ex\hbox{$\m@th\scriptscriptstyle >$}}\fi}
\def\frq{\protect\@frq}

%% list-Umgebungen
%\def\slideitemsep{-2ex minus .2ex}
%\def\slidepartopsep{0ex minus .2ex}
%\def\slide@listi{%
%  \leftmargin\leftmargini
%  \labelwidth\leftmargini \advance\labelwidth-\labelsep
%  \parsep\parskip \divide\parsep2
%  \partopsep\slidepartopsep\relax
%  \advance\partopsep-\parskip
%  \ifdim\partopsep<\z@\partopsep\z@\fi
%  \itemsep\slideitemsep\relax
%  \ifdim\parsep<\itemsep
%    \topsep\itemsep \advance\topsep-\parsep
%  \else
%    \itemsep\parsep \topsep\z@
%  \fi}
%\def\slide@listparameters{%
%  \let\@listdepth\slide@listdepth
%  \slide@listdepth\z@
%  \def\@listi{\slide@listi}%
%  \def\@listii{\slide@listii}%
%  \def\@listiii{\slide@listiii}%
%  \let\@listiv\relax\let\@listv\relax\let\@listvi\relax}
%\slide@listparameters

\makeatother
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}

\switchToEmptyFrame

\begin{slide}{}
\vspace*{2cm}

\Large
\begin{center}
  {\bf Nichtmonotone Vererbung \\
         und \\
       Default Logic} 

\vspace*{1cm}

\large
Wolfgang May\\
Freiburg, 6.12.2001
\end{center}
\end{slide}

\switchToMainFrame
\begin{slide}{Nonmonotonic Reasoning}

\begin{itemize}
\item seit sp"ate 70er:  Konzepte und Theoretische Untersuchungen \\
\item 80er: Wissensrepr"asentation 
\item 90er: Objektorientiertes Datenmodell
\item heute: XML: Default-Attribute
\end{itemize}
\end{slide}

\overlays{3}{%
\begin{slide}{Nichtmonotone Vererbung}

\begin{tabular}{l@{\hspace*{2cm}}l}

\begin{tabular}{@{}rl}
~~$\bullet$ & V"ogel fliegen. \\
$\bullet$ & Tweety ist ein Vogel. \\\hline
          & Tweety fliegt
\end{tabular}

&  \fromSlide{2}{$\pl D \vdash \alpha$}
\\[2cm]

\begin{tabular}{@{}rl}
\fromSlide{2}{$\bullet$} & \fromSlide{2}{V"ogel fliegen.} \\
\fromSlide{2}{\rnode{left0}{\strut}~~$\bullet$} & 
   \fromSlide{2}{Pinguine fliegen nicht.\rnode{right0}{\strut}} \\
\fromSlide{2}{$\bullet$} & \fromSlide{2}{Tweety ist ein Vogel.} \\
\fromSlide{3}{$\bullet$} & \fromSlide{3}{\lightred Tweety ist ein Pinguin!} 
\\
      & \fromSlide{2}{Tweety fliegt} \fromSlide{3}{\lightred nicht!}
\end{tabular}

&  \fromSlide{3}{$\pl D {\lightred {} \cup \pl D^+} \not\vdash \alpha$}
\end{tabular}
\fromSlide{2}{\ncline[linecolor=white,offset=-3.7em]{left0}{right0}}\end{slide}
}%overlays

\overlays{5}{%
\begin{slide}{Problematik}

  {\begin{tabular}[t]{l}
    \fromSlide{3}{\rnode{left1}{\strut}}bird(X) $\to$ flies(X)\fromSlide{3}{\rnode{right1}{\strut}} \\
    penguin(X) $\to$ not\_flies(X) \\
    bird(tweety) \\
    bird(lora) \\
    \fromSlide{2}{\yellow penguin(tweety)} \\
\hline
    \fromSlide{3}{\rnode{left2}{\strut}}%
        flies(tweety)%
           \fromSlide{3}{\rnode{right2}{\strut}} \\
    \fromSlide{3}{\rnode{left3}{\strut}}%
        flies(lora)%
           \fromSlide{3}{\rnode{right3}{\strut}} \\
    \fromSlide{2}{\yellow not\_flies(tweety)} \\
    \onlySlide{2}{{\lightred inkonsistent}}
    \end{tabular}
    \hspace*{0em}
    \begin{tabular}[t]{l}
    \fromSlide{4}{\rnode{left0}{\strut}bird(X) 
          {\lightred $\land$ $\neg$ penguin} $\to$ flies(X)\rnode{right0}{\strut}} \\
    \fromSlide{4}{penguin(X) $\to$ not\_flies(X)} \\
    \fromSlide{4}{bird(tweety)} \\
    \fromSlide{4}{penguin(tweety)} \\
    \fromSlide{4}{bird(lora)} \\
    \fromSlide{4}{flies(lora)} \qquad \fromSlide{5}{\lightred(?)} \\
    \fromSlide{4}{not\_flies(tweety).} \\
    ~\\
    \fromSlide{5}{\lightred wissen wir, ob Lora kein Pinguin ist?} \\
    \fromSlide{5}{\lightred CWA}
    \end{tabular}\hspace*{-1cm}
    \fromSlide{3}{\ncline[linecolor=red]{left1}{right1}}
    \fromSlide{3}{\ncline[linecolor=red]{left2}{right2}}
    \fromSlide{3}{\ncline[linecolor=red]{left3}{right3}}
    \fromSlide{4}{\ncline[linecolor=white,offset=-6.7em]{left0}{right0}}
  }
\end{slide}
}%overlays

\begin{slide}{Inheritance Nets}

\begin{itemize}
  \item ``Direkter'', grafischer Formalismus
\end{itemize}
\vskip0.5cm
  
  ~\hfill
  \rnode{tweety}{tweety} \hfill
  \begin{tabular}[t]{c}
    \rnode{penguin}{penguin} \\[0.2cm]
    \rnode{lora}{lora}
  \end{tabular}\hfill
  \rnode{bird}{\vphantom{g}bird} \hfill
  \rnode{fly}{fly} \hfill
  ~

  \nodeconnections{\psset{nodesep=3pt}
  \ncline[doubleline=true]{->}{tweety}{penguin}
  \ncline[doubleline=true]{->}{penguin}{bird}
  \ncline[doubleline=true]{->}{lora}{bird}
  \ncline{->}{bird}{fly}
  \ncarc[arcangleA=20,arcangleB=20]{->}{penguin}{fly}\ncput{\black /}
  }
%%%%% Handbook, S.121.
\def\notpath{\ensuremath{-\!\!\!\!-\hspace*{-0.8em}%
        \raisebox{0.25ex}{$\scriptscriptstyle/$}\hspace*{0.5em}}}

  Pfad: ~~ tweety -- penguin -- bird -- fly \\
  ist ``preempted'' durch ~ tweety -- penguin \notpath\ fly \\
  Pfad: ~~ lora -- bird -- fly
\medskip
  
\begin{itemize}
\item \emph{Extension} als theoretisches Modell-Konzept
\end{itemize}
\end{slide}

\begin{slide}{Beispiel}

\hypertarget{NixonDiamond}{}%
  Konflikt:

  \begin{center}
  \begin{tabular}{ccc}
      &\rnode{nixon}{nixon} \\[1cm]
  \rnode{quaker}{quaker} && \rnode{republican}{republican} \\[1cm]
      &\rnode{pacifist}{pacifist}
  \end{tabular}
  \end{center}

  \nodeconnections{
  \ncline[doubleline=true]{->}{nixon}{quaker}
  \ncline[doubleline=true]{->}{nixon}{republican}
  \ncline{->}{quaker}{pacifist}
  \ncline{->}{republican}{pacifist}\ncput{\black/}}

\begin{itemize}
\item zwei m"ogliche \emph{Extensionen}
\end{itemize}
\invisiblehyperlink{NixonDiamondII}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}

\begin{slide}{Default Logic}
  
Erweitert First-Order Logic um zus"atzliche ``weiche''
Schlussregeln \
[R.Reiter, AI 1980]

\[d ~= ~\frac{\alpha(\bar x) : \beta(\bar x)}{w(\bar x)}
    \hspace*{2cm}
       \frac{bird(x) : fly(x)}{fly(x)} \]

\begin{itemize}
\item \emph{precondition} $p(d)=\alpha(\bar x)$
\item \emph{justification} 
       $J(d)=\beta(\bar x) = \{\beta_1(\bar x),\ldots,\beta_k(\bar x)\}$
\item \emph{consequence} $c(d)=w(\bar x)$
\item $\alpha,\beta,w$ beliebige First-Order Formeln
\item Ist $\alpha(\bar c)$ beweisbar und die Annahme $\beta(\bar c)$
  konsistent, kann $w(\bar c)$ daraus geschlossen werden.
\end{itemize}
\end{slide}

\begin{slide}{CWA: Implizites Negatives Wissen}

\begin{itemize}
\item Datenbanken: nur positive Fakten gespeichert
  \begin{itemize}
  \item CWA [Reiter 1978] ist ein negativer Default ohne Vorbedingung:
    \[  \frac{: \neg p(x_1,\ldots,x_n)}{\neg p(x_1,\ldots,x_n)} \] 
  \item negatives Wissen muss nicht explizit repr"asentiert werden.
  \end{itemize}
\item Logic Programming: Negation as failure
\end{itemize}
\end{slide}

\begin{slide}{Default Proofs}

\hypertarget{DefaultProof}{}Eingabe: 
eine Menge $D$ von Defaults und eine Menge $S$
von Formeln (``Situation'').

Ein Default Proof einer Formel $\gamma$ bzgl.\ $D$ und $S$ ist
eine Folge $d_1,\ldots,d_n$ von Defaults wenn
\begin{itemize}
\item f"ur $i=1...n$:
  \begin{itemize}
  \item $p(d_i) \in \Th(S \cup c(\{d_1,\ldots,d_{i - 1}\}))$
  \item $\Th(S \cup \{J(d_i)\})$ ist konsistent
  \end{itemize}
\item $\gamma \in \Th(S \cup c(\{d_1,\ldots,d_n\}))$
\end{itemize}

\begin{itemize}
\item Aber:
  \begin{itemize}
  \item $S \cup \{c(d_1),\ldots,c(d_n)\}$ kann inkonsistent sein
  \item $J(d_i)$ kann mit vorhergehenden oder nachfolgenden 
        $c(d_i)$ und $J(d_i)$ inkonsistent sein
  \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}{Extensionen}

\begin{itemize}
\item Gegeben:  $\Delta=(D,F)$ wobei $D$ eine Menge von Defaults und
 $F$ eine Menge von geschlossenen Formeln.
\end{itemize}

\begin{itemize}
  \item \hypertarget{GammaIntro}{}Sei $S$ eine Menge geschlossener Formeln.
  \item $\Gamma(S)$ minimal so dass
    \begin{itemize}
    \item $F \subseteq \Gamma(S)$
    \item $\Th(\Gamma(S)) = \Gamma(S)$ \ (deduktiv abgeschlossen)
    \item f"ur alle $\gamma$, f"ur die es einen Default Proof
          bzgl.\ $\Delta$ und $S$ gibt, ist $\gamma \in \Gamma(S)$
          \ \ (Abschluss gg.\ $D$).
    \item {\red $\Gamma(S)$ kann inkonsistent sein}
    \end{itemize}
 \item eine Menge $E$ geschlossener Formeln ist eine \emph{Extension}
  von $\Delta$, falls $\Gamma(E)=E$. 
\end{itemize}

\invisiblehyperlink{StrengereGamma}{Kriterium ist nicht konstruktiv.}
\end{slide}

\begin{slide}{Alternative Charakterisierung}

[Reiter AI 1980] \ $\Delta = (D,F)$.

\hypertarget{QuasiInductive}{}%
$S_0=F,S_1,S_2,\ldots$ eine Folge von Mengen von Formeln
so dass ${\lightred S}=(\bigcup_{i=0}^\infty S_i)$ und 
\[ S_{i+1} = S_i \cup c(GD(S_i,{\lightred S},D))~,\]
%
\[GD(S_i,{\lightred S},D) := \{d \st 
    \begin{array}[t]{@{}l}
      d \mbox{ ist eine Instanz eines Defaults in $D$,~} \\
        \Th(S_i) \models p(d) 
        \mbox{ und } {\lightred \Th(S \cup J(d)) \mbox{ ist konsistent}}\}
        \end{array}\]

Dann ist $\Th(S)$ eine \emph{Extension} von $\Delta$.

\begin{itemize}
\item ``{\lightred quasi}-induktive'' Charakterisierung
\end{itemize}
\invisiblehyperlink{BottomUpApproximation}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}

\begin{slide}{Eigenschaften}

  \begin{itemize}
  \item Im allgemeinen besitzt $\Delta$ mehrere Extensionen
  \item f"ur jedes $\gamma$ gibt  $S_0,S_1,\ldots$ eine ``Herleitung''   
     (\invisiblehyperlink{DefaultProof}{``Default Proof''})
  \item Fragestellungen:
    \begin{itemize}
    \item credulous: ist eine Formel/ein Faktum in irgendeiner Extension zu
      $\Delta$ enthalten?
  \item sceptical: ist eine Formel/ein Faktum in jeder Extension zu
      $\Delta$ enthalten?
    \item safe: besitzt eine Formel/ein Faktum in jeder Extension dieselbe
      Herleitung?
    \end{itemize}
  \end{itemize}
\end{slide}

\begin{slide}{Eigenschaften (Cont'd)}
%[Reiter AI 1980, 4.2/p104]
\begin{itemize}
\item Alle wesentlichen Fragen sind $\Sigma_2^P$- oder 
  $\Pi_2^P$-vollst"andig. \\
  Genauer: NP, wenn man ein SAT-Orakel verwendet
      %% Marek-Truszczynski-Book 1993
\item Gibt es eine Extension von $\Delta$, die $\gamma$ enth"alt?
  \begin{itemize}
  \item nicht semi-entscheidbar, d.h., die Menge aller Formeln die in
    irgendeiner Extension gelten ist nicht rekursiv aufz"ahlbar.
  \end{itemize}
\item Aussagenlog.\ Default-Theorien ohne Disjunktion:  NP \\\relax
  [Kautz, Selman AI 91] 
\item Sceptical semantics: ist keine Extension, \\
  erf"ullt \invisiblehyperlink{Cumulativity}{\emph{cumulative
      monotony}}\ nicht.
\end{itemize}
\end{slide}


\begin{slide}{Approximation durch Bottom-up-Iteration}

\hypertarget{BottomUpApproximation}{}%
$S_0=F,S_1,S_2,\ldots$ eine Folge von Mengen von Formeln
so dass $S=(\bigcup_{i=0}^\infty S_i)$ und 
\[ S_{i+1} = S_i \cup C_i \mbox{~~wobei } 
      C_i {\lightred {}\subseteq{}}
           c(GD({\lightred S_i},D))~,\]

\[GD({\yellow S_i},D) := \{d \st 
    \begin{array}[t]{@{}l}
      d \mbox{ ist eine Instanz eines Defaults in $D$,~} \\
        \Th({\yellow{S_i}}) \models p(d) 
        \mbox{ und } {\lightred \Th({\yellow S_i} \cup J(d)) 
               \mbox{ ist konsistent}}\}
        \end{array}\]

Betrachte dann $\Th(S)$.
\invisiblehyperlink{QuasiInductive}%
 {\vbox to 3cm{\hbox to\textwidth{}}}
\end{slide}

\overlays{2}{
\begin{slide}{Bottom-Up}
  
Risiko: Justification wird in einem sp"ateren Schritt ung"ultig

Abhilfe:

\begin{itemize}
\item  Mitf"uhren der verwendeten Justifications 
       [Brewka AI 1991]
\item  geeignete Struktur der Defaults
       \hypertarget{NormaleDefaultsIntro}{}
\end{itemize}

\fromSlide{2}{%
\redheadline{Normale Defaults}

Form: \quad
      $\displaystyle\frac{\alpha:w}{w}$ \qquad
      $\displaystyle\frac{bird(x) : fly(x)}{fly(x)}$

\medskip
\begin{itemize}
\item Jede normale Default-Theorie hat (mindestens) eine Extension.
   %% einsichtig: immer einen d \in GD anwenden bis GD=leer
\item \invisiblehyperlink{SemiMonotony}%
 {Jede Extension l"a"st sich bottom-up berechnen}
\end{itemize}}
\end{slide}
}

\begin{slide}{Vererbung und Datenbanken}
  \begin{itemize}
  \item Default Logic: Mengen von Formeln
  \item Deduktive, objektorientierte Datenbanken
    \begin{itemize}
    \item Menge von (nur positiven) Fakten
    \item Regeln  \ \ \textit{head $\gets$ body}
    \item Vererbung innerhalb der Klassenhierarchie
    \end{itemize}
  \item bottom-up Auswertung, $T_P$-Operator ersetzt Theoriebildung
  \item {\yellow dazu passen nur spezielle ``Horn-style'' Defaults}
    \begin{itemize}
    \item {\yellow $\alpha,\beta$ vorzugsweise Literale (oder einfache
        Formeln)}
    \item {\yellow $w$ Atome}
    \item Horn Default-Theorien sind polynomial [Kautz, Selman AI 91] 
    \end{itemize}
  \end{itemize}
\invisiblehyperlink{Kritik}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}

\begin{slide}{Beispiel}
  
 \[\begin{array}{ll}
   penguin\subcl bird  \\
   tweety \isa penguin \\[0.2cm]
   \displaystyle d_1: \
         \frac{X\isa penguin : X[flies\fd false]}{X[flies\fd false]} \quad&
   \displaystyle d_2: \ 
         \frac{X\isa bird : X[flies\fd true]}{X[flies\fd true]}
 \end{array}
 \]

 \begin{itemize}
 \item Zwei m"ogliche Extensionen
   \begin{itemize}
   \item Anwendung von $d_1$: $tweety[flies\fd false]$ \\
   \item Anwendung von $d_2$: $tweety[flies\fd true]$ \\
         intuitiv nicht beabsichtigt \\
         Preemption wird nicht ber"ucksichtigt!
   \end{itemize}
 \end{itemize}
\end{slide}

\begin{slide}{Pr"aferenzen}

\begin{itemize}
\item ``Ranked'' Defaults
\item Spezifischere Defaults automatisch bevorzugen \\\relax
      [Poole IJCAI 85]
\item hier: Klassenhierarchie \\
    ``Wenn es keine dazwischenliegende Klasse gibt''
\end{itemize}
\end{slide}

\overlays{2}{%
\begin{slide}{Defaults f"ur Vererbung}

Default Schemata:
 \[\begin{array}{c}
    X\isa C, C[M\bfd V]: 
       X[M\fd V] {\yellow \land \neg \exists SC: (X\isa SC \land SC\subcl C)}
    \\\hline 
    X[M\fd V]
    \\
    \fromSlide{2}{\yellow\neg (\exists SC: 
                   (X\isa SC \land SC\subcl C \land \neg SC[M\bfd V]))}
   \end{array}
\]

Analog f"ur Vererbung zu Subklassen.

\begin{itemize}
\item Bottom-up-Approximation \\
  \untilSlide*{1}{%
    \begin{itemize}
      \item Risiko: Zwischenklassen, die erst in einem sp"ateren Schritt
        abgeleitet werden und dem Default nicht entsprechen
    \end{itemize}}
  \fromSlide*{2}{%
    \begin{itemize}
      \item Risiko: Zwischenklassen, die erst in einem sp"ateren Schritt
        abgeleitet werden und dem Default nicht entsprechen
      \item {\yellow kein Problem bei statischer Klassenhierarchie}
    \end{itemize}}
\end{itemize}
\end{slide}}

\overlays{2}{%
\begin{slide}{Konflikte}

\hypertarget{NixonDiamondII}{}%
Konflikt: \emph{konsistente Teilmenge} anwenden.
\smallskip

\fromSlide{2}{%
Nixon Diamond:

  $P=$\{\begin{tabular}[t]{l}
        \flrule{quaker[policy\bfd pacifist]}, 
         \flrule{republican[policy\bfd hawk]}, \\
        \flrule{nixon\isa quaker}, \flrule{nixon\isa republican}\}.
      \end{tabular}
\medskip

$S_0 = T_P^\omega(P) = P$

\[\begin{array}{@{}l@{}l}
  GD(S_0,D) = & 
     \left\{
       \frac{\flrule{\small nixon\isa quaker, quaker[policy\bfd pacifist]:
                           nixon[policy\fd pacifist]}}
                   {\flrule{\small nixon[policy\fd pacifist]}},
     \right.\\[0.3cm]
   &\left.~~
      \frac{\flrule{\small nixon\isa republican, quaker[policy\bfd hawk]:
                           nixon[policy\fd hawk]}}
                   {\small \flrule{nixon[policy\fd hawk]}}
    \right\}
  \end{array}\]
}

\invisiblehyperlink{NixonDiamond}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}
}

\begin{slide}{Komplexit"at}

\begin{itemize}
\item es gen"ugt, in jedem Schritt einen anwendbaren
  Default anzuwenden
\item ohne Objektgenerierung: eine Extension wird in {\yellow
    polynomialer} Zeit berechnet
\item credulous/sceptical/safe: alle Extensionen m"ussen berechnet werden
\end{itemize}

Fazit:

\begin{itemize}
\item Anwendung von Defaults auf Vererbung in objektorientierten
  Datenbanken sinnvoll
\item auch f"ur XML vielversprechend
\end{itemize}
\end{slide}

\begin{slide}{Kritik}

\hypertarget{Kritik}{}%
\begin{itemize}
\item ``sceptical'' Semantik zu restriktiv: \\
  bereits ein einziger Default (z.B.\
  $\displaystyle\frac{:\neg a}{a}$) kann dazu f"uhren, dass keine 
  Extension existiert
\item ``sceptical'' Semantik ist \emph{keine} Extension
\item ``sceptical'' Semantik ist nicht
       \invisiblehyperlink{Cumulativity}{kumulativ}, 
       erf"ullt \invisiblehyperlink{Distribution}{``Or/Distribution''}\
       nicht.
\end{itemize}
\invisiblehyperlink{SucheSemantiken}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}

\begin{slide}{Weitere Aspekte}
\hypertarget{WeitereAspekteI}{}%
\begin{itemize}
\item Suche nach ``besseren'' Semantiken
\item \invisiblehyperlink{LPDefaultLogic}{Logic Programming mit 
           Negation und Default Logic}
  \begin{itemize}
  \item "Ubersetzung
  \end{itemize}
\item \invisiblehyperlink{MetaProperties}{Metatheoretische 
     Eigenschaften nichtmonotoner Systeme}
  \begin{itemize}
  \item Default-Logic verh"alt sich ziemlich ``unerw"unscht'' \\
    (\invisiblehyperlink{Cumulativity}{nicht kumulativ}, 
     erf"ullt \invisiblehyperlink{Distribution}{``Or''}\ nicht)
  \item Default-Logic ist nicht \invisiblehyperlink{Rationality}{``Rational''}
  \item Anwendung f"ur Vererbung in Bottom-up Evaluierung f"ur
    Grundinstanzen ist problemlos
  \end{itemize}
\end{itemize}

\invisiblehyperlink{Questions}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}

\begin{slide}{Die Suche nach ``besseren'' Semantiken}

\hypertarget{SucheSemantiken}{}%
\begin{itemize}
\item gesucht: \invisiblehyperlink{Cumulativity}{kumulative Semantik}
\end{itemize}

Betrachte \invisiblehyperlink{GammaIntro}{$\Gamma(S)$}\relax\ im 
Nixon-Diamond

\begin{itemize}
\item $\Gamma(\emptyset) = P\cup\{\flrule{nixon\isa pacifist},\
                            \flrule{nixon\isa hawk}\} = E_{cred}$
\item $\Gamma(\Gamma(\emptyset)) = P = E_{scept}$
\item alternierend
\end{itemize}

Interpretationsm"oglichkeiten:
\begin{itemize}
\item Dreiwertige Semantik wie f"ur LP: 
  dreiwertige Extensionen [Przymusinski AI 1991] \\
  (LP: 3-wertige Default-Semantik+CWA "aquivalent zu WFS)
\end{itemize}

\end{slide}

\begin{slide}{Stationary Default Extensions}

Andere Interpretationsm"oglichkeit:

``Stationary Default Extensions''
[Przymusinska/-ski FI 94]

\begin{itemize}
\item $\Gamma$ ist antimonoton, \
   $\Gamma\circ\Gamma$ ist monoton
\item Bedingung: $\Gamma(\Gamma(E)) = E$
\item Extensionen $\subsetneq$ station"are Extensionen
\item kleinste station"are Extension iterativ berechenbar:
  $\emptyset, \Gamma^2(\emptyset), 
   \Gamma^4(\emptyset), \ldots, \Gamma^{2n}(\emptyset), \ldots$ \\
\item endlich falls $\Delta$ endlich und keine Funktionssymbole
\item $n$ Defaults, $m$ Justifications $\to$ $O(n^2\cdot m)$ 
  Erf"ullbarkeitstests/$\Gamma$-Schritt, \\
  sinnvoll f"ur Sprachen wo Erf"ullbarkeit polynomiell
%  z.B.\ in Kombination mit Horn-Regeln 
\item ``sceptical'' erf"ullt \invisiblehyperlink{Cumulativity}{Kumulativit"at}
\end{itemize}
\end{slide}


\overlays{2}{%
\begin{slide}{St"arkere zweiwertige Semantiken}
  
  In vielen F"allen ist station"are Semantik zu streng: \\
  ``Ungerade'' \invisiblehyperlink{GammaIntro}{$\Gamma$-Anwendung}\relax\
  akzeptiert zu viel. \\
  ($\Gamma$ ist noch gro"sz"ugiger als die bottom-up Approximation)

\fromSlide{2}{\begin{itemize}
\item $\Gamma$ basiert auf \invisiblehyperlink{DefaultProof}{Default Proofs}
\item Default Proof kann inkonsistent sein 
\item Default Proof kann inkonsistente Justifications benutzt haben
  \begin{itemize}
  \item einzeln inkonsistent zum Ergebnis
  \item es gibt keine Extension, in der die verwendeten Justifications
     \emph{gleichzeitig} zutreffen
  \end{itemize}
\end{itemize}}
\invisiblehyperlink{WeitereAspekteII}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}
}

\begin{slide}{St"arkere zweiwertige Semantiken}

\hypertarget{StrengereGamma}{}%
Strengere $\Gamma_i$-Operatoren [Brewka, Gottlob FI 1997]
\begin{itemize}
\item Bedingung: $\Gamma(\Gamma_i(E)) = E$
\item $\invisiblehyperlink{GammaIntro}{$\Gamma_1(S)$} = \{p\st
   \mbox{es gibt einen 
    \invisiblehyperlink{DefaultProof}{Default Proof}\ f"ur \ $p$}\}$
\item $\Gamma_2$: Default Proof ist konsistent
\item $\Gamma_3$: Justifications sind konsistent
\item $\Gamma_4$: Default Proof muss mit einer Extension konsistent,
       d.h., nachvollziehbar sein
\end{itemize}

\begin{itemize}
\item Betrachte Fixpunkte von $\Gamma\Gamma_i$.
\item $\begin{array}[t]{lcl}
      WFS & = & (\Gamma\Gamma_1)^\omega(\emptyset) \ \subseteq \
                  (\Gamma\Gamma_2)^\omega(\emptyset) \\
          & \subseteq & (\Gamma\Gamma_3)^\omega(\emptyset) \ \subseteq \
             (\Gamma\Gamma_4)^\omega(\emptyset) \ = \ safe 
          \end{array}$
\end{itemize}
\end{slide}

\begin{slide}{Gammas-Hierarchie}

\[\begin{array}{cc}
   \bigcup(\mbox{Extensionen}) = \Gamma_4 \le 
                \Gamma_3 \le \Gamma_2 \le \Gamma_1 = \Gamma \\
   \Gamma_4 \le \bigcup(\mbox{bottom-up}^\omega) \le \Gamma_2 \\[0.5cm]

   WFS_{\Gamma_1}(\Delta) \subseteq
     WFS_{\Gamma_2}(\Delta) \subseteq
     WFS_{\Gamma_3}(\Delta) \subseteq
     WFS_{\Gamma_4}(\Delta) = Safe(\Delta)
 \end{array} \]
\bigskip

F"ur normale Default-Theorien:

  $\Gamma_2 = \Gamma_3 = \Gamma_4 = \bigcup(\mbox{bottom-up})^\omega
      = \bigcup(\mbox{Extensionen})$
\end{slide}

\begin{slide}{Gammas-Hierarchie}

\begin{itemize}
\item $\Gamma = \Gamma_1$: alles was irgendwie begr"undet werden kann.
\item $\Gamma_2$: abgeleitete Formeln m"ussen konsistent sein.
\item $\Gamma_3$: Justifications m"ussen mit abgeleiteten Formeln
  konsistent sein.
\item bottom-up Iteration: Default-Proof muss in einer Extension
  nachvollziehbar sein -- allerdings k"onnen Justifications sp"ater
  verloren gehen.
\item $\Gamma_4$: Default-Proof muss in einer Extension
  nachvollziehbar sein.
\item $\bigcup(\mbox{Extensionen}) = \Gamma_4$
\item f"ur normale Defaults: $\bigcup(\mbox{bottom-up})$,
  $\Gamma_2$, $\Gamma_3$, $\Gamma_4$ und $\bigcup(\mbox{Extensionen})$
  "aquivalent.
\end{itemize}
\end{slide}

\begin{slide}{Weitere Aspekte}

\hypertarget{WeitereAspekteII}{}%
\begin{itemize}
\item \invisiblehyperlink{LPDefaultLogic}{Logic Programming mit 
           Negation und Default Logic}
  \begin{itemize}
  \item "Ubersetzung
  \end{itemize}
\item \invisiblehyperlink{MetaProperties}{Metatheoretische 
     Eigenschaften nichtmonotoner Systeme}
  \begin{itemize}
  \item Default-Logik verh"alt sich ziemlich ``unerw"unscht''
    \invisiblehyperlink{Cumulativity}{(nicht kumulativ, erf"ullt ``Or'' nicht)}
  \item Default-Logic ist nicht \invisiblehyperlink{Rationality}{``Rational''}
  \item Anwendung f"ur Vererbung in Bottom-up Evaluierung f"ur
    Grundinstanzen ist problemlos
  \end{itemize}
\end{itemize}

\invisiblehyperlink{StrengereGamma}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}

\switchToEmptyFrame

\begin{slide}{Questions}
\vspace*{3cm}

\Huge\bf \hypertarget{Questions}{Questions ??}

\invisiblehyperlink{WeitereAspekteI}%
 {\vbox to 6cm{\hbox to\textwidth{}}}
\end{slide}

\switchToMainFrame

\begin{slide}{LP mit Negation und Default Logic}

\hypertarget{LPDefaultLogic}{}%
Formulierung von LP in Default-Logic $P \mapsto \Delta(P)$ \\\relax
  [Przymusinski 1988, Bidoit, Froidevaux I\&C 1991] \\
  \[ p(\bar x) \ :- \ a_1(\bar x)\land\ldots\land a_n(\bar x),
                  \neg b_1(\bar x)\land\ldots\land \neg b_m(\bar x). \]
  \[\frac{a_1(\bar x)\land\ldots\land a_n(\bar x):
                  \neg b_1(\bar x)\land\ldots\land \neg b_m(\bar x)}
         {p(\bar x)} \]
Beispiel:
\[ \frac{move(X,Y):\neg win(Y)}{win(X)} \]

\begin{itemize}
\item stabile Modelle entsprechen Extensionen
\item kleinstes station"ares Modell entspricht der WFS \\
      polynomiell
\end{itemize}
\end{slide}

\begin{slide}{Default-Theorien als Logic Programs}

umgekehrte Richtung ...

\begin{itemize}
\item "Ubersetzung von Default-Theorien in LPs [Li, You JCI 1991]
\end{itemize}  

\end{slide}

\begin{slide}{Defaults vs. Implikation}

\begin{itemize}
\item Implikation: $(X \isa bird) \imp fly(X)$ \\

  Konsequenz: $\neg fly(tweety) \imp \neg(tweety \isa bird)$
\bigskip

\item Default:
      $\displaystyle \frac{bird(x) : fly(x)}{fly(x)}$
\medskip

  Konsequenz: $\neg fly(tweety)$ bedeutet nur, dass der Default 
     auf Tweety nicht anwendbar ist \\\relax
  [vgl.\ Poole AI 1988 (Theorist)]
\end{itemize}
\end{slide}

\begin{slide}{Generating Defaults}

\begin{itemize}
\item $S$ eine Menge geschlossener Formeln.
  \[GD(S,D) := \{d \st 
    \begin{array}[t]{@{}l}
      d \mbox{ ist eine Instanz eines Defaults in $D$,~} \\
        {\lightred \Th(S) \models p(d)}
        \mbox{ und } {\lightred \Th(S \cup J(d)) \mbox{ ist konsistent}}\}
        \end{array}\]
  \begin{itemize}
  \item $GD(S,D)$ kann Konflikte enthalten.
  \end{itemize}
\end{itemize}
\end{slide}

\overlays{2}{%
\begin{slide}{Gammas-Hierarchie}

\begin{itemize}
\item Skeptical reasoning in Reiter's Default Logik: 
   $\Pi_2^P$-vollst"andig.
\item $\Gamma = \Gamma_1$, $\Gamma_2$, $\Gamma_3$, $\Gamma_4$: 
   WFS $\Pi_2^P$-hart.
\item $\Gamma_4$: WFS $\Sigma_3^P$-vollst"andig.
\end{itemize}
\bigskip

\fromSlide{2}{%
wobei

\begin{itemize}
\item $\Pi_2^P$: polynomiell nichtdeterministisch l"osbar, wenn man
    ein NP-Orakel hat
\item $\Sigma_2^P$: Probleme, deren Komplement in $\Pi_2^P$ ist.
\end{itemize}
}
\end{slide}
}

\begin{slide}{Beispiel f"ur station"are Extension}

[Przymusinska, Przymusinski FI 1994]

\[\begin{array}{l@{\hspace*{1cm}}c}
  sleep \gets \neg work. & \displaystyle \frac{:\neg work}{sleep} \\[0.4cm]
  work \gets \neg tired. & \displaystyle \frac{:\neg tired}{work} \\[0.4cm]
  tired \gets \neg sleep. & \displaystyle \frac{:\neg sleep}{tired} \\[0.4cm]
  paid.                    \\[0.4cm]
  angry \gets work, \neg paid & \displaystyle \frac{work:\neg paid}{angry} 
\end{array}\]
analog: Nixon Diamond
\end{slide}  

\begin{slide}{Beispiel f"ur station"are Extension (Cont'd)}

\begin{itemize}
\item mehrere Extensionen $\{paid, \neg angry, sleep\}$,
      $\{paid, \neg angry, work\}$, $\{paid, \neg angry, tired\}$
\item Sceptical Semantics: $E_{scept} = \{paid, \neg angry\}$
\item ist keine Extension
\item $\Gamma(\emptyset) = \{paid, \neg angry, sleep, work, tired\}$
\item $\Gamma(\{paid, \neg angry, sleep, work, tired\}) = E_{scept}$
\item $\Gamma^2(E_{scept}) = E_{scept}$
\end{itemize}
\end{slide}

\overlays{2}{%
\begin{slide}{Beispiel zu WFS-2}

\[ D = \left\{ \frac{:b}{b}~,~\frac{:a}{a}~,~\frac{:\neg a}{\neg a}\right\} \]

\fromSlide*{2}{%
  $\Gamma(\emptyset) = \Th(\{b,a,\neg a\}) = Lang$ \\
  $\Gamma_2(\emptyset) = \Th(\{b,a\}) \cup \Th(\{b,\neg a\})$ \\
  enth"alt $\neg b$ nicht. \\
  Damit ist die Annahme von $b$ konsistent:\\
  $\Gamma(\Gamma_2(\emptyset)) = \Th(\{b\})$ \\
  Fixpunkt.
}
\end{slide}
}

\overlays{2}{%
\begin{slide}{Beispiel zu Gamma-Hierarchie}

\[ D = \left\{ \frac{:a}{a}~,~\frac{:\neg a}{\neg a}~,~
               \frac{:b}{c}~,~\frac{:a}{d}~,~\frac{\neg a:b}{\neg b}
             \right\} \]
\fromSlide*{2}{%
\[ \begin{array}{c||c|c|c|c}
    & i=1 & i=2 & i=3 & i=4 \\\hline\hline
   \Gamma_i(\emptyset) 
     & Lang
     & \begin{array}{l} \Th(\{a,c,d\})\cup{} \\
                        \Th(\{\neg a,c,d,\neg b\})
       \end{array}
     & \begin{array}{l} \Th(\{a,c,d\})\cup{} \\
                        \Th(\{\neg a,c\})
       \end{array}
     & \Th(\{a,c,d\}) 
   \\\hline
   \Gamma\Gamma_i(\emptyset) 
     & \Th(\emptyset)
     & \Th(\emptyset)
     & \Th(\{c\})
     & \Th(\{a,c,d\})
  \end{array} \]
}
\end{slide}
}

\overlays{2}{%
\begin{slide}{WFS$_i$ f"ur Logic Programming}

\[ P = \{ \begin{array}[t]{l@{\hspace*{1cm}}l@{\hspace*{1cm}}l}
            a \gets \neg d & c \gets \neg b & b \gets \neg b,d \\
            d \gets \neg a & f \gets \neg d \}
          \end{array} \]

\begin{itemize}
 \item Stabiles Modell: $\{a,c,f\}$ 
 \item $WFS(P) = WFS_2(P) = \Th(\emptyset)$ 
 \item $WFS_3(P) = \Th(\{c\})$  \ \ \ 
   \fromSlide{2}{($b$-Regel ist self-defeating)}  
 \item $WFS_4(P) = \Th(\{a,c,f\})$  \ \ \ 
\end{itemize}
\end{slide}
}

\begin{slide}{Metatheoretische Eigenschaften}

[Kraus,Lehmann,Magidor AI 1990]

\hypertarget{MetaProperties}{}%
Eigenschaften von Konsequenzrelationen:\\
Was soll man aus einer Menge von ``$\alpha \snake \beta$'' 
schlie"sen?

Ganz notwendig:
\medskip

\begin{itemize}
\item Reflexivity: ~ $\alpha \snake \alpha$
\item Left Logical Equivalence: ~ 
      $\displaystyle\frac{\models \alpha\iff\beta~,~\alpha\snake\gamma}
                         {\beta\snake\gamma}$
\item Right Weakening: ~
      $\displaystyle\frac{\models \alpha\imp\beta~,~\gamma\snake\alpha}
                         {\gamma\snake\beta}$
\end{itemize}
\end{slide}

\overlays{2}{%
\begin{slide}{Kumulativit"at}

\hypertarget{Cumulativity}{}%
System $\mathbf C$ (Cumulative): Eigenschaften aus [Gabbay 1985]
\begin{itemize}
\item Cut: ~
      $\displaystyle\frac{\alpha\land\beta\snake\gamma~,~\alpha\snake\beta}
                         {\alpha\snake\gamma}$\\
  \fromSlide{2}{Um $\alpha\snake\gamma$ zu zeigen, kann man
            tempor"ar $\beta$ dazunehmen, wenn ...}
\item Weak Monotonicity/Cautious Monotonicity/Cumulative Monotonicity: ~
      $\displaystyle\frac{\alpha\snake\beta~,~\alpha\snake\gamma}
                         {\alpha\land\beta\snake\gamma}$ \\
  \fromSlide{2}{Wenn man $\beta$ erf"ahrt und es vorher schon 
         geglaubt hat, bleiben alle Schl"usse g"ultig}
\end{itemize}

\fromSlide{2}{Beide zusammen:\\
  Wenn $\alpha\snake\beta$, dann stimmen die Schl"usse aus $\alpha$ 
  und $\alpha\land\beta$ "uberein.}
\end{slide}
}

\begin{slide}{Metatheoretische Eigenschaften (Cont'd)}

\begin{itemize}
\item ``Sceptical'' Default Semantik:
  \begin{itemize}
  \item erf"ullt Cut [Makinson NMR 89]
  \item nicht kumulativ [Makinson NMR 89]; auch nicht f"ur normale Defaults
  \item erf"ullt ``Or'' nicht
  \end{itemize}
\item $WFS$ ist kumulativ, $WFS_2$, $WFS_3$ und $WFS_4$ sind nicht
  kumulativ.
\end{itemize}
\end{slide}

\begin{slide}{System C (Cont'd)}

Abgeleitete Regeln f"ur System $\mathbf C$:

\begin{itemize}
\item Equivalence: ~
      $\displaystyle\frac{\alpha\snake\beta~,~
                          \beta\snake\alpha~,~
                          \alpha\snake\gamma}
                         {\beta\snake\gamma}$
\item And: ~
      $\displaystyle\frac{\alpha\snake\beta~,~
                          \alpha\snake\gamma}
                         {\alpha\snake\beta\land\gamma}$
\item Modus Ponens Cumulative: ~
      $\displaystyle\frac{\alpha\snake\beta\imp\gamma~,~
                          \alpha\snake\beta}
                         {\alpha\snake\gamma}$
\medskip
\item schwache Transitivit"at: ~
      $\displaystyle\frac{\alpha\lor\beta\snake\alpha~,~
                          \alpha\snake\gamma}
                         {\alpha\lor\beta\snake\gamma}$
\end{itemize}
\end{slide}                       

\overlays{2}{%
\begin{slide}{System CM}

System $\mathbf{CM}$ (Schw"acher als Classical Monotonic Logic):\\
(abgelehnt f"ur nichtmonotone Systeme)

\begin{itemize}
\item Monotonicity: ~
      $\displaystyle\frac{\models\alpha\imp\beta~,~
                          \beta\snake\gamma}
                         {\alpha\snake\gamma}$ \\
   \fromSlide{2}{$penguin\imp bird~,~bird\snake flies$}
\item Easy Half of Deduction Theorem: ~
      $\displaystyle\frac{\alpha\snake\beta\imp\gamma}
                         {\alpha\land\beta\snake\gamma}$
\item Transitivit"at: ~
      $\displaystyle\frac{\alpha\snake\beta~,~
                          \beta\snake\gamma}
                         {\alpha\snake\gamma}$
\end{itemize}


\begin{itemize}
\item Contraposition: ~
      $\displaystyle\frac{\alpha\snake\beta}
                         {\neg\beta\snake\neg\alpha}$
\end{itemize}
\end{slide}                       
}

\begin{slide}{Pr"aferentielle Systeme}

\hypertarget{Distribution}{}%
System $\mathbf P$ (Preferential): $\mathbf C$ und

\begin{itemize}
\item Or: ~
      $\displaystyle\frac{\alpha\snake\gamma~,~\beta\snake\gamma}
                         {\alpha\lor\beta\snake\gamma}$
\end{itemize}

Ableitbar:
\begin{itemize}
\item Hard Half of Deduction Theorem: ~
      $\displaystyle\frac{\alpha\land\beta\snake\gamma}
                         {\alpha\snake\beta\imp\gamma}$
\item Proof by Cases/Distribution: ~
      $\displaystyle\frac{\alpha\land\beta\snake\gamma~,~
                          \alpha\land\neg\beta\snake\gamma}
                         {\alpha\snake\gamma}$
\end{itemize}

\end{slide}

\begin{slide}{Pr"aferentielle Modelle und H"ulle}
  
[Shoham LICS 87; Kraus, Lehmann, Magidor AI 90] \\
Partiell geordnete Menge von Strukturen/Theorien (``Welten''), die
angibt, welche ``mehr normal'' als andere sind.
  
\begin{itemize}
\item $\alpha \snake \beta$ gilt, wenn alle Welten, die $\alpha$
  erf"ullen und ``am normalsten'' (minimal) sind, auch $\beta$ erf"ullen.
\item Def: $\alpha \snake \beta \in {\mathbf K}^p$ wenn 
  es in allen pr"aferentielle Modellen zu $\mathbf K$ gilt.
\item Die pr"aferentielle Folgerungsrelation ist co-NP [Lehmann,
  Magidor AI 1992]
\end{itemize}  

\end{slide}

\begin{slide}{Rationalit"at}
  
\hypertarget{Rationality}{}Zus"atzlich Aussagen, was \emph{nicht}
    geschlossen werden soll:

\begin{itemize}
\item Negation Rationality: ~
      $\displaystyle\frac{\alpha\land\gamma\not\snake\beta,~
                          \alpha\land\neg\gamma\not\snake\beta}
                         {\alpha\not\snake\beta}$ \\
\item Disjunctive Rationality: ~
      $\displaystyle\frac{\alpha\not\snake\gamma,~
                          \beta\not\snake\gamma}
                         {\alpha\lor\beta\not\snake\gamma}$ \\
\item Rational Monotonicity:\
      $\displaystyle\frac{\alpha\land\beta\not\snake\gamma,~
                          \alpha\not\snake\neg\beta}
                         {\alpha\not\snake\gamma}$ 
      ~ "aq. ~
      $\displaystyle\frac{\alpha\snake\gamma,~
                          \alpha\not\snake\neg\beta}
                         {\alpha\land\beta\snake\gamma}$ \\


\item R.M. impliziert mit System $\mathbf C$ D.R., und das wiederum N.R.
   %% KLM90, p198
\item ``Rational'': Systeme, die Rational Monotonicity erf"ullen.
\item wenn ein Faktum, dessen Negation vorher nicht abgeleitet werden
  konnte, dazugelernt wird, wird kein vorheriger Schluss widerrufen
\end{itemize}
\end{slide}

\begin{slide}{Rationalit"at (Cont'd)}

f"ur rationale Systeme gelten schw"achere Formen der bei 
$\mathbf CM$ genannten Regeln:

\begin{itemize}
\item Weak Transitivity: ~
      $\displaystyle\frac{\alpha\snake\beta~,~
                          \beta\snake\gamma~,~
                          \beta\not\snake\neg\alpha}
                         {\alpha\snake\gamma}$
\item Weak Contraposition: ~
      $\displaystyle\frac{\alpha\land\gamma\snake\beta~,~
                          \gamma\not\snake\beta}
                         {\gamma\land\neg\beta\snake\neg\alpha}$
\end{itemize}
\end{slide}

\begin{slide}{Rationale Konsequenzrelationen}
  
[Lehmann, Magidor AI 1992]

\begin{itemize}
\item Ranking von Formeln: beschreibt, wie sehr ``Ausnahme'' eine
  Formel ist.
\item  Rationale Konsequenzrelationen k"onnen durch ``Ranked Models''
  repr"asentiert werden:
\item ``Ranked Models'' sind pr"aferentielle Modelle, deren Ordnung
  bestimmte Bedingungen erf"ullt \\
  (kleinerer Rank $\to$ weniger unnormal).
\item trotzdem ist \emph{Ranked Entailment} nur \emph{Preferential
  entailment}: \\
  Schnitt aller rationalen Extensionen ist nur ${\mathbf  K}^p$.
\end{itemize}
\end{slide}

\begin{slide}{Rationale H"ulle}
  
[Lehmann, Magidor AI 1992]

\begin{itemize}
\item Ordnung auf rationalen Extensionen (nach Normalit"at)
\item falls minimale rationale Extension $\bar{\mathbf K}$
  existiert, ist das die rationale H"ulle \\
  (existiert wenn ein sinnvolles Ranking der Formeln m"oglich ist, z.B.
  f"ur alle endlichen $\mathbf K$)
\item $\alpha \snake\beta \in \bar{\mathbf K}$ falls
  \begin{itemize}
  \item $rank(\alpha) < rank(\alpha\land\neg\beta)$, oder
  \item $rank(\alpha)$ existiert nicht (dann ist $\alpha$ inkonsistent
    zu $\mathbf K$)
  \end{itemize}
\end{itemize}
\end{slide}

\begin{slide}{Rationale H"ulle: Komplexit"at}
  
[Lehmann, Magidor AI 1992]

\begin{itemize}
\item $\bar{\mathbf K}$ iterativ berechenbar aus $\mathbf K$, indem
  man solange $E(C)$ (Menge aller Ausnahmeformeln) bildet, bis man bei
  $\alpha$ ankommt. Dann wird gepr"uft ob $\beta$ noch mehr Ausnahme ist.
\item Test, ob eine Formel eine Ausnahme beschreibt: reduzierbar auf
   SAT in der zugrundeliegenden Logik.
\item Man braucht $O(n^2)$ Iterationen.
\item Horn-Fall: polynomial.
\end{itemize}
\end{slide}


\begin{slide}{Default-Logic und Kumulativit"at}
  
Default-Logic erf"ult Kumulativit"at nicht\\\relax
[Makinson LPNMR 89]  %% aus Brewka-Uebersicht

\[\frac{:p}{p} \qquad,\qquad \frac{p\lor q:\neg p}{\neg p} \]

\begin{itemize}
\item hat genau eine Extension: $\Th\{p\}$, enth"alt also auch 
  $p\lor q$
\item nimmt man $p\lor q$ als Pr"amisse an, bekommt man eine zweite
  Extension $\Th(\{\neg p,q\})$ enth"alt.
\end{itemize}

Anderes, normales Beispiel [Makinson Handbook 1994]:

\[\frac{:a}{a}\quad,\quad
  \frac{a:b}{b}\quad,\quad
  \frac{b:\neg a}{\neg a} \]
\end{slide}

\begin{slide}{Default-Logic und Kumulativit"at}
Beispiel mit normalen Defaults [Brewka AI 91]

\[\begin{array}{l}
    F= \{dog \lor bird \imp pet~,~dog \imp \neg bird~,~ sings\} \\
    \displaystyle 
    D= \left\{ \frac{pet:dog}{dog} ~,~
                 \frac{sings:bird}{bird} \right\}
  \end{array}\]

Extension: $\Th(F\cup\{bird\})$ contains $pet$.
  
Nimmt man $pet$ zu den Fakten dazu, erh"alt man eine
zus"atzliche Extension $\Th(F\cup\{dog\})$
\end{slide}

\begin{slide}{Default-Logic und OR}

aus [Poole KR89]  %% aus Brewka-Uebersicht

\[\frac{:usable(X) \land \neg broken(X)}{usable(X)} \]

Pr"amisse: $broken(left\_arm)\lor broken(right\_arm)$
\smallskip

Die einzige Extension enth"alt 

\[usable(left\_arm)\land usable(right\_arm) \]

(jedes $usable(X)$ kann einzeln abgeleitet werden)
\smallskip

\begin{itemize}
\item 
  L"osung: Buchf"uhrung "uber verwendete Justifications
  [Lukaszewicz CI 1988, Brewka AI 1991, Delgrande 1994]
\item womit man auch das Problem des bottom-up Verfahrens l"ost
\end{itemize}
\end{slide}

\begin{slide}{Default-Logic und OR}

[Poole Handbook 1994]

\[ \frac{employed(X):get\_paid(X)\land works(X)}{get\_paid(X)} \]

Fakten: $employed(david)$, $employed(john)$,
        $\neg works(david) \lor \neg works(john)$

\smallskip

Hier ist es sinnvoll, dass die Extension

\[ get\_paid(david) \land get\_paid(john) \]

ableitet.
\end{slide}

\begin{slide}{Default-Logic und Proof-by-cases}

aus [Makinson Handbook 94] 

\[\frac{a:c}{c} \quad,\quad \frac{\neg a:c}{c}\]

Es gilt $a \snake c$ und $\neg a\snake c$ aber nicht 
$true\snake c$.
\end{slide}

\begin{slide}{Cumulative Default Logic}

Buchf"uhrung "uber verwendete Justifications [Brewka AI 1991]:

Formel $\phi$ kann unter Verwendung der Justifications 
$\gamma_1,\ldots,\gamma_n$ begr"undet werden:
\[ \langle \phi, \{r_1,\ldots,r_n\}\rangle \]

$S_0=F,S_1,S_2,\ldots$ eine Folge von Mengen von ({\red annotierten}) 
Formeln so dass ${\lightred S}=(\bigcup_{i=0}^\infty S_i)$ und
\[ \begin{array}{l}
   S_{i+1} = S_i \cup 
     \{\begin{array}[t]{l}
       \langle C, R\cup \beta \cup \{c(d)\}\rangle \st
        d \in D,
       \Th(S_i) \models p(d) \mbox{ und } \\
       \Th(S \cup Supp(S) \cup J(d) {\red\cup \beta \cup \{c(d)\}}) 
         \mbox{ ist konsistent}\}
       \end{array}
     \end{array}\]

Dann ist $\Th(S)$ eine \emph{CDL-Extension} von $\Delta$.

Kumulativ, und es existiert immer eine CDL-Extension.  
\end{slide}

\begin{slide}{Lokalit"at normaler Defaults}

\hypertarget{SemiMonotony}{}%
Form: \ $\displaystyle\frac{\alpha:w}{w}$

\begin{itemize}
\item Jede Extension l"a"st sich bottom-up berechnen
\item Semi-Monotonie: $D\subseteq D'$, $E$ eine Extension von
   $(D,F)$. Dann hat $(D',F)$ eine Extension $E'$ so dass
   \begin{itemize}
   \item $E \subseteq E'$
   \item $GD(E,D) \subseteq GD(E',D')$
   \end{itemize}
   \begin{itemize}
     \item[$\Rightarrow$] ``Lokalit"at''
   \end{itemize}
\item Vollst"andigkeit von Top-Down Default Proofs \\\relax
      [Reiter AI 1980].
\end{itemize}
\invisiblehyperlink{NormaleDefaultsIntro}%
 {\vbox to 2cm{\hbox to\textwidth{}}}
\end{slide}

\begin{slide}{Seminormale Defaults}

Es gibt Dinge, die nicht als normale Defaults ausdr"uckbar sind:

\[\frac{has\_motive(X):suspect(X)\land guilty(X)}
         {suspect(X)} \]

\end{slide}

\begin{slide}{Komplexit"at: Basic Notions}

\begin{itemize}
\item SAT f"ur propositional Logic ist NP-vollst"andig
\item SAT f"ur first-order ist nicht rekursiv aufz"ahlbar
\item $QBF(2,\exists) = SAT(\exists\ldots\exists\forall\ldots\forall\phi)$ 
  ist $\Sigma_2^P$-vollst"andig \\
  (d.h., NP-vollst., wenn man auf ein $\Sigma_1^P$- oder NP-Orakel
  zur"uckgreifen kann).
\item $\Sigma_{k+1}^P = NP^{\Sigma_k^P}$, $\Sigma_0^P = P$
\item $\Sigma_1^P=NP$
\end{itemize}
\end{slide}

\begin{slide}{Komplexit"at von Default Reasoning}
  $\Sigma_P^2$ oder $\Pi_P^2$-vollst"andig sind f"ur endliche
  aussagenlogische Default-Theorien:
\begin{itemize}
\item Existenz einer [konsistenten] Extension.
\item gilt $\gamma$ in [einer$|$allen] [konsistenten] Extensionen
  [nicht]?
\item dasselbe bereits f"ur normale Defaults ohne Prerequisites.
\item ``Sceptical'' f"ur normale Defaults ist $P^{NP[\log n]}$-vollst"andig \\
  (LFP-Berechnung der station"aren Semantik muss nur bis $\Gamma^2$
   ausgef"uhrt werden) [Gottlob IC 1995] 
\end{itemize}

Default-Theorien ohne Disjunktion:  NP \\\relax
[Kautz, Selman AI 91] 

Horn Default Theorien: linear time [Kautz, Selman AI 91] 
\end{slide}

\begin{slide}{Beweistheorie}

Gibt es eine Extension von $\Delta$, die $\gamma$ enth"alt?

\begin{enumerate}
\item zeige $\gamma$ mit $F\cup c(D)$ \\
  ($R$ Grundinstanzen der verwendeten Defaults)
\item zeige alle Preconditions der verwendeten Defaults
  (rekursiv, $R^+$ alle verwendeten Grundinstanzen)
\item teste Konsistenz von $F \cup J(R^+)$
  {\red (SAT, nicht r.a.)}
\end{enumerate}

Es gibt keine Prozedur, um das im allgemeinen Fall zu berechnen.
\end{slide}

\begin{slide}{Beweistheorie}

F"ur normale Defaults existiert eine vollst"andige Beweistheorie  
[Reiter AI 1980]:

\begin{itemize}
\item $F,\gamma$ in Horn-Form
\item jedes $c(D)$ in Horn-Form: \\
   Menge $(C,\{\delta\})$ von Paaren von annotierten Klauseln \\
  ($\delta=\emptyset$ f"ur $C\in F$)
\item Resolution: ~
  $(C_1,D_1)$ $(C_2,D_2)$ zu $(R,D_1\cup D_2)$
\end{itemize}
\end{slide}

\begin{slide}{Beweistheorie}

Lineare Resolution 

\begin{itemize}
\item Startklausel: $R_0 = {}$ eine negierte Klausel in $\gamma$
\item $R_{i-1}$ mit einem $C_i$ zu $R_i$, wobei $C_i$
  \begin{itemize}
  \item ein $(C,\{d\})$ vom Input
  \item eine negierte Klausel in $\gamma$
  \item ein vorhergehendes $R_j$.
  \end{itemize}
\item $R_n =(\Box,D)$ f"ur eine Menge $D_0$ von Defaults
\end{itemize}

\begin{itemize}
\item Gezeigt: Aus $c(D_0)$ l"asst sich $\gamma$ ableiten.
\item rekursiv: Herleitungen f"ur die Preconditions in $D_k$ suchen,
  ergibt $D_{k+1}$.
\item Zuletzt bleibt zu zeigen: $F \cup \bigcup_k c(D_k)$ ist
  erf"ullbar (SAT(Horn) ist polynomial)
\end{itemize}
\end{slide}
\end{document}
