Commit 474a959a authored by Miriam Polzer's avatar Miriam Polzer

presentation

parent 5b9180c4
......@@ -28,17 +28,39 @@
\maketitle
\end{frame}
\begin{frame}
Miri: \\
Einführung, was ist KIbox?
Syntax der Logik
Welche Eigenschaften braucht KIbox?
TODO @Miriam renaming der ND Regeln in Coq
%\begin{frame}
% Miri: \\
% Einführung, was ist KIbox?
% Syntax der Logik
% Welche Eigenschaften braucht KIbox?
% TODO @Miriam renaming der ND Regeln in Coq
%\end{frame}
\begin{frame}{Intuitionistic Modal Logic $\KIbox \oplus Z$}
$\phi ::= \top \ |\ \bot\ |\ n\ |\ \phi_1 \rightarrow \phi_2\ |\ \phi_1 \lor \phi_2\ |\
\phi_1 \land \phi_2\ |\ \Box \phi $ \hfill $n \in Vars$
\vspace{2cm}
Now we need a proof system satisfying:
\begin{itemize}
\item All intuitionistic tautologies
\item Closure under substitution and MP
\item Closure under generalization: If $A$ valid, then $\Box A$ valid.
\item $\Box (A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B)$
\item Axiom $Z$
\end{itemize}
\end{frame}
\begin{frame}
Natural Deduction \\
KClbox
%\begin{frame}
% Natural Deduction \\
% KClbox
%\end{frame}
\begin{frame}{Natural Deduction for $\KIbox \oplus Z$}
\end{frame}
\begin{frame}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment