Commit 870458b6 authored by Ulrich Rabenstein's avatar Ulrich Rabenstein

talk init

parent ee1fe9d4
\documentclass{beamer}
\sloppy
\usepackage{times}
\usepackage{microtype}
\usepackage[T1]{fontenc}
\usepackage{graphicx,xspace,relsize}
\usepackage{lipsum}
\usepackage{tikz}
\usepackage{url}
\usepackage{wrapfig}
\usepackage[utf8]{inputenc}
\renewcommand{\baselinestretch}{.99}
\title{Double-Negation Translation of Intuitionistic Modal Logics in Coq}
\author{Miriam Polzer \& Ulrich Rabenstein}
\begin{document}
\begin{frame}
\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
\end{frame}
\begin{frame}
Natural Deduction \\
KClbox
\end{frame}
\begin{frame}
IM Tautologien (impl, and, or)
\end{frame}
\begin{frame}
Motivation der translations (man braucht mehr als ¬¬) \\
kol, ggr, kur (triangle) and dneg-closed \\
def von adequatness (als Ziel) \\
äquivalenz von adeq. (mit Bild?)
\end{frame}
\begin{frame}
Ulrich: \\
adequate_eq_ggr
\end{frame}
\begin{frame}
envelopes \\
evtl. beispiele \\
theorem 5
\end{frame}
\begin{frame}
theorem 6
\end{frame}
\begin{frame}
Coq \\
Permutations \\
Taktiken früher einbauen \\
...
\end{frame}
\begin{frame}
Ausblick (siehe Mail)
\end{frame}
\begin{frame}
Wenn noch Zeit ist: Semantik
\end{frame}
\begin{frame}
Quellen
\end{frame}
\end{document}
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