\begin{slide}{Regelsysteme}

\begin{itemize} \itemsep 0pt
\item
  $R$ eine Menge von Regeln, 
  definiert Relation (einmalige Anwendung irgendeiner Regel irgendwo):

  $\to_R := \{ ( t,s) \mid\exists (l,r)\in R, p\in\Pos(t): t \to_{(l,r),p} s \}$

\item
  transitive Hülle $\to_R^+$ (mehrmalige Regelanwendung)
\end{itemize}

liefert nichtdeterministisches Berechnungsmodell
(vgl. Grammatiken/Wortersetzungssysteme)

Fragen:
\begin{itemize} \itemsep 0pt
\item
  jede Rechnung endet? (Termination) nach welcher Zeit?
\item
  jede Rechnung endet mit genau einem Resultat?
\end{itemize}

dabei: Resultat $=$ Term, auf den keine Regel anwendbar ist
$=$ Normalform.

\end{slide}

