
\begin{slide}{Inferenz-Systeme}

ein \emph{Inferenz-System} $I$ besteht aus
\begin{itemize}
\item Regeln (besteht aus Prämissen, Konklusion)

  Schreibweise $\frac{P_1, \ldots, P_n}{K}$

\item Axiomen ($=$ Regeln ohne Prämissen)
\end{itemize}

eine \emph{Ableitung} für $F$ bzgl. $I$ ist ein Baum:
\begin{itemize}
\item jeder Knoten ist mit einer Formel beschriftet
\item jeder Knoten (mit Vorgängern) entspricht Regel von $I$
\item Wurzel ist mit $F$ beschriftet
\end{itemize}
Schreibweise: $I \vdash F$


\end{slide}

\newcommand{\ZZ}{\mathbb{Z}}

\begin{slide}{Inferenz-Systeme (Beispiel 1)}

  \begin{itemize}
  \item Grundbereich $=$ Zahlenpaare $\ZZ\times\ZZ$
  \item Axiom: 
\[ \frac{}{(13,5)}
\]
  \item Regel-Schemata: 
\[
\frac{(x,y)}{(x-y,y)},\quad
\frac{(x,y)}{(x,y-x)}
\] 
  \end{itemize}
  
kann man $(1,1)$ ableiten? \quad $(-1,5)$? $(2,4)$?

\end{slide}

\begin{slide}{Inferenz-Systeme (Beispiel 2)}

  \begin{itemize}
  \item
    Grundbereich: Zeichenketten aus $\{0,1\}^*$
  \item Axiom: \[ \frac{}{01} \]
  \item Regel-Schemata (für jedes $u,v$): 
\[
\frac{0u, v0}{u1v}, 
\quad \frac{1u,v1}{u0v}, 
\quad \frac{u}{\operatorname{reverse}(u)}
\]
  \end{itemize}
  
Leite $11001$ ab. Wieviele Wörter der Länge $k$ sind ableitbar?

\end{slide}


\newcommand{\wert}{\operatorname{\mathsf{wert}}}
\newcommand{\BB}{\mathbb{B}}

\begin{slide}{Inferenz von Werten}

  \begin{itemize}
  \item 
Grundbereich: Aussagen der Form $\wert(f,b)$
mit $f \in $Formeln, $b\in\BB = \{0,1\}$
\item
Axiome: $\wert(\mathsf{T},1), \wert(\mathsf{F},0)$
\item 
Regeln: 
\( \displaystyle
\frac{\wert(X,1),\wert(Y,1)}{\wert(X\wedge Y,1)},
\frac{\wert(X,0)}{\wert(X\wedge Y,0)},
\frac{\wert(Y,0)}{\wert(X\wedge Y,0)},
\dots
\)
\end{itemize}
Beispiel: leite $\wert((T\wedge F)\wedge (T\wedge T),0)$ ab.

\bigskip

Durch ein Inferenzsystem kann man die Semantik von
Ausdrücken (Programmen) spezifizieren.

(hier: dynamische Semantik)

\end{slide}


\begin{slide}{Inferenz mit Umgebungen}

Motivation: Inferenzsystem für (aussagenlogische) Formeln mit Variablenbindung
\begin{itemize}
\item 
  Grundbereich: Aussagen der Form $\wert(E,F,B)$ 

  (in Umgebung $E$ hat Formel $F$ den Wert $B$)
\item
  Regeln für Operatoren \( \displaystyle
\frac{\wert(E,X,1),\wert(E,Y,1)}{\wert(E,X\wedge Y,1)}, \ldots\)
\item Regeln für Umgebungen
  \( \displaystyle \frac{}{\wert(E[v:=b],v,b)}, \quad
  \frac{\wert(E,v',b')}{\wert(E[v:=b],v',b')}
  \) für $v \neq v'$
\item Regeln für Bindung:
\(\displaystyle
\frac{\wert(E,X,b), \wert (E[v:=b],Y,c)}{\wert(E,\mathtt{let~} v=X \mathtt{~in~} Y,c)}
\)

\end{itemize}

\end{slide}

