|
jan@42381
|
1 |
\documentclass[%
|
|
jan@42381
|
2 |
%handout, % prints handouts (=no animations, for printed version)
|
|
jan@42381
|
3 |
%mathserif
|
|
jan@42381
|
4 |
%xcolor=pst,
|
|
jan@42381
|
5 |
14pt
|
|
jan@42381
|
6 |
% fleqn
|
|
jan@42381
|
7 |
]{beamer}
|
|
jan@42381
|
8 |
|
|
jan@42381
|
9 |
\usepackage{beamerthemedefault}
|
|
jan@42381
|
10 |
|
|
jan@42381
|
11 |
\useoutertheme[subsection=false]{smoothbars}
|
|
jan@42381
|
12 |
\useinnertheme{circles}
|
|
jan@42381
|
13 |
|
|
jan@42381
|
14 |
\setbeamercolor{block title}{fg=black,bg=gray}
|
|
jan@42381
|
15 |
\setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}
|
|
jan@42381
|
16 |
\setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}
|
|
jan@42381
|
17 |
\setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}
|
|
jan@42381
|
18 |
\setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}
|
|
jan@42381
|
19 |
\setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}
|
|
jan@42381
|
20 |
|
|
jan@42401
|
21 |
%activate hyperlinks at the end
|
|
jan@42381
|
22 |
%\usepackage{hyperref}
|
|
jan@42381
|
23 |
|
|
jan@42381
|
24 |
\usepackage[english]{babel}
|
|
jan@42381
|
25 |
\usepackage[utf8]{inputenc}
|
|
jan@42381
|
26 |
\usepackage{array}
|
|
jan@42381
|
27 |
\usepackage{setspace}
|
|
jan@42381
|
28 |
|
|
jan@42381
|
29 |
\definecolor{tug}{rgb}{0.96862,0.14509,0.27450}
|
|
jan@42381
|
30 |
|
|
jan@42381
|
31 |
\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
|
|
jan@42381
|
32 |
\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
|
|
jan@42381
|
33 |
|
|
jan@42381
|
34 |
\setbeamertemplate{headline}[text line]{
|
|
jan@42381
|
35 |
\begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}
|
|
jan@42381
|
36 |
\insertnavigation{0.85\paperwidth}
|
|
jan@42381
|
37 |
\raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt
|
|
jan@42381
|
38 |
\hskip-1pt\rule{\paperwidth}{0.3pt}
|
|
jan@42381
|
39 |
\end{beamercolorbox}
|
|
jan@42381
|
40 |
}
|
|
jan@42381
|
41 |
|
|
jan@42381
|
42 |
\setbeamertemplate{navigation symbols}{}
|
|
jan@42381
|
43 |
|
|
jan@42381
|
44 |
\definecolor{gray}{rgb}{0.8,0.8,0.8}
|
|
jan@42381
|
45 |
\setbeamercolor{footline}{fg=black,bg=gray}
|
|
jan@42381
|
46 |
|
|
jan@42381
|
47 |
% Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl
|
|
jan@42381
|
48 |
\setbeamertemplate{footline}[text line]{
|
|
jan@42381
|
49 |
\hskip-1pt
|
|
jan@42381
|
50 |
\begin{beamercolorbox}[wd=\paperwidth]{footline}
|
|
jan@42381
|
51 |
\rule{\paperwidth}{0.3pt}
|
|
jan@42381
|
52 |
\colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}
|
|
jan@42381
|
53 |
\textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%
|
|
jan@42381
|
54 |
\insertshorttitle\rule{1em}{0pt}}
|
|
jan@42381
|
55 |
\rule{\paperwidth}{0.3pt}
|
|
jan@42381
|
56 |
\end{beamercolorbox}
|
|
jan@42381
|
57 |
\begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}
|
|
jan@42381
|
58 |
\end{beamercolorbox}
|
|
jan@42381
|
59 |
}%
|
|
jan@42381
|
60 |
|
|
jan@42381
|
61 |
%% Titelblatt-Einstellungen
|
|
jan@42381
|
62 |
\institute[IST, SPSC]{Institute for Software Technology\\Institute of Signal Processing and Speech Communication\\Graz University of Technology}
|
|
jan@42381
|
63 |
\title[ISAC for Signal Processing]{Interactive Course Material for\\ Signal Processing based on\\ Isabelle/\isac}
|
|
jan@42381
|
64 |
\subtitle{Baccalaureate Thesis}
|
|
jan@42381
|
65 |
\author{Jan Rocnik}
|
|
jan@42401
|
66 |
\date{\today}
|
|
jan@42381
|
67 |
|
|
jan@42381
|
68 |
% Subject and Keywords for PDF
|
|
jan@42381
|
69 |
\subject{Final presentation of Bakk. Thesis}
|
|
jan@42381
|
70 |
\keywords{isac, isabelle, ist, spsc, thesis, course material}
|
|
jan@42381
|
71 |
|
|
jan@42381
|
72 |
\titlegraphic{\includegraphics[width=20mm]{tuglogo}}
|
|
jan@42381
|
73 |
|
|
jan@42381
|
74 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
75 |
\begin{document}
|
|
jan@42381
|
76 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
77 |
|
|
jan@42381
|
78 |
\begin{frame}[plain]
|
|
jan@42381
|
79 |
\frametitle{}
|
|
jan@42381
|
80 |
\titlepage
|
|
jan@42381
|
81 |
\end{frame}
|
|
jan@42381
|
82 |
|
|
jan@42381
|
83 |
|
|
jan@42381
|
84 |
|
|
jan@42381
|
85 |
\begin{frame}
|
|
jan@42381
|
86 |
\frametitle{Contents}
|
|
jan@42401
|
87 |
\begin{spacing}{0.3}
|
|
jan@42381
|
88 |
\tableofcontents[hideallsubsections %
|
|
jan@42381
|
89 |
% ,pausesections
|
|
jan@42381
|
90 |
] % erzeugt Inhaltsverzeichnis
|
|
jan@42401
|
91 |
\end{spacing}
|
|
jan@42381
|
92 |
\end{frame}
|
|
jan@42381
|
93 |
|
|
jan@42381
|
94 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
95 |
\section{Introduction}
|
|
jan@42381
|
96 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
97 |
|
|
jan@42381
|
98 |
\subsection{isabelle}
|
|
jan@42381
|
99 |
\begin{frame}
|
|
jan@42381
|
100 |
\frametitle{What is isabelle?}
|
|
jan@42381
|
101 |
\begin{spacing}{1.5}
|
|
jan@42381
|
102 |
\begin{itemize}
|
|
jan@42401
|
103 |
\item Generic Proof Assistant
|
|
jan@42401
|
104 |
\item Formular Proofing in Logical Calculus
|
|
jan@42401
|
105 |
\item Developed in Cambridge, Muenchen and Paris
|
|
jan@42381
|
106 |
\end{itemize}
|
|
jan@42381
|
107 |
\end{spacing}
|
|
jan@42381
|
108 |
\end{frame}
|
|
jan@42381
|
109 |
|
|
jan@42381
|
110 |
\subsection{isac}
|
|
jan@42381
|
111 |
\begin{frame}
|
|
jan@42401
|
112 |
\frametitle{What is {\isac}?}
|
|
jan@42381
|
113 |
\begin{spacing}{1.5}
|
|
jan@42381
|
114 |
\begin{itemize}
|
|
jan@42401
|
115 |
\item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations
|
|
jan@42401
|
116 |
\item Learning Coach
|
|
jan@42401
|
117 |
\item Interactiv Course Material
|
|
jan@42401
|
118 |
\item Developed at TU Graz
|
|
jan@42381
|
119 |
\end{itemize}
|
|
jan@42381
|
120 |
\end{spacing}
|
|
jan@42381
|
121 |
\end{frame}
|
|
jan@42381
|
122 |
|
|
jan@42401
|
123 |
\subsection{motivation}
|
|
jan@42401
|
124 |
\begin{frame}
|
|
jan@42401
|
125 |
\frametitle{Motivation - {\isac{}}~Assessing Advances}
|
|
jan@42401
|
126 |
\begin{itemize}
|
|
jan@42401
|
127 |
\item Stepwise Solving Engineering Problems\\
|
|
jan@42401
|
128 |
{\small \textcolor{tug}{Consistent framework over the solving process}}
|
|
jan@42401
|
129 |
\item Explaining underlying knowledge\\
|
|
jan@42401
|
130 |
{\small \textcolor{tug}{Transparent Content, Access to Multimedia Content}}
|
|
jan@42401
|
131 |
\item Checking Steps Input by the Student\\
|
|
jan@42401
|
132 |
{\small \textcolor{tug}{Proof situation}}
|
|
jan@42401
|
133 |
\item Assessing stepwise Problem Solving\\
|
|
jan@42401
|
134 |
{\small \textcolor{tug}{One System for Tutoring and Assessment}}
|
|
jan@42401
|
135 |
\end{itemize}
|
|
jan@42401
|
136 |
\end{frame}
|
|
jan@42401
|
137 |
|
|
jan@42381
|
138 |
|
|
jan@42381
|
139 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
140 |
\section{Thesis Definition}
|
|
jan@42381
|
141 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
142 |
|
|
jan@42381
|
143 |
\begin{frame}
|
|
jan@42401
|
144 |
\frametitle{Thesis Definition}
|
|
jan@42401
|
145 |
%---> Follow up thesis abstract! <---%
|
|
jan@42401
|
146 |
\begin{itemize}
|
|
jan@42401
|
147 |
\item Creation of Interactive Course Material\\
|
|
jan@42401
|
148 |
{\small Based on Given Tasks}
|
|
jan@42401
|
149 |
\item Content Should be~\ldots~useable at Specific Lectures.
|
|
jan@42401
|
150 |
\item \ldots~useable for \emph{STEOP}.
|
|
jan@42401
|
151 |
\item Guideline for Upcoming TP-Programmers.
|
|
jan@42401
|
152 |
\item Feedback of Usability\\
|
|
jan@42401
|
153 |
{\small (TP-Programming Language)}
|
|
jan@42401
|
154 |
\end{itemize}
|
|
jan@42381
|
155 |
\end{frame}
|
|
jan@42381
|
156 |
|
|
jan@42381
|
157 |
\subsection{issues}
|
|
jan@42381
|
158 |
\begin{frame}
|
|
jan@42401
|
159 |
\frametitle{Issues to Accomplish I}
|
|
jan@42401
|
160 |
\begin{spacing}{1.4}
|
|
jan@42401
|
161 |
\begin{itemize}
|
|
jan@42401
|
162 |
\item What Knowledge is Mechanised in Isabelle?\\
|
|
jan@42401
|
163 |
{\small How about new?}
|
|
jan@42401
|
164 |
\item What Problems are Implemented in {\sisac{}}?\\
|
|
jan@42401
|
165 |
{\small How about new?}
|
|
jan@42401
|
166 |
\item What is the Effort?
|
|
jan@42401
|
167 |
\end{itemize}
|
|
jan@42401
|
168 |
\end{spacing}
|
|
jan@42381
|
169 |
|
|
jan@42401
|
170 |
\end{frame}
|
|
jan@42401
|
171 |
|
|
jan@42401
|
172 |
\begin{frame}
|
|
jan@42401
|
173 |
\frametitle{Issues to Accomplish II}
|
|
jan@42401
|
174 |
\begin{spacing}{1.4}
|
|
jan@42381
|
175 |
\begin{itemize}
|
|
jan@42401
|
176 |
\item How Look Calculations Like?\\
|
|
jan@42401
|
177 |
{\small Ansatzs, Subproblems?}
|
|
jan@42401
|
178 |
\item How are Problems Specified?\\
|
|
jan@42401
|
179 |
{\small Given, Pre-/Postcondition, Find?}
|
|
jan@42401
|
180 |
\item What is the Contents of the Interactiv Course Material?\\
|
|
jan@42401
|
181 |
{\small Figures, Explenations,\ldots}
|
|
jan@42381
|
182 |
\end{itemize}
|
|
jan@42401
|
183 |
\end{spacing}
|
|
jan@42381
|
184 |
\end{frame}
|
|
jan@42381
|
185 |
|
|
jan@42381
|
186 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
187 |
\section{Demo}
|
|
jan@42381
|
188 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
189 |
|
|
jan@42381
|
190 |
\begin{frame}
|
|
jan@42401
|
191 |
\frametitle{Demonstration of {\isac}}
|
|
jan@42381
|
192 |
\begin{spacing}{1.5}
|
|
jan@42381
|
193 |
\begin{itemize}
|
|
jan@42401
|
194 |
\item {\Large Development Enviroment} (Backend)
|
|
jan@42401
|
195 |
\vspace{15mm}
|
|
jan@42401
|
196 |
\item {\Large Math Assistant} (Frontend)
|
|
jan@42381
|
197 |
\end{itemize}
|
|
jan@42381
|
198 |
\end{spacing}
|
|
jan@42381
|
199 |
\end{frame}
|
|
jan@42381
|
200 |
|
|
jan@42381
|
201 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
202 |
\section{Summary}
|
|
jan@42381
|
203 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
204 |
|
|
jan@42401
|
205 |
\subsection{Accomplished Work}
|
|
jan@42381
|
206 |
\begin{frame}
|
|
jan@42401
|
207 |
\frametitle{Accomplished Work}
|
|
jan@42381
|
208 |
\begin{itemize}
|
|
jan@42401
|
209 |
\item Partial Fractions\\ {\small Theorems, Specification, Program}
|
|
jan@42401
|
210 |
\item Inverse Z-Transform with Partial Fractions\\ {\small Theorems, Specification, Program}
|
|
jan@42401
|
211 |
\item Isabelle Theory Indicating Issues\\ {\small Preperation for {\sisac{}}-developers}
|
|
jan@42381
|
212 |
\end{itemize}
|
|
jan@42381
|
213 |
\end{frame}
|
|
jan@42381
|
214 |
|
|
jan@42381
|
215 |
\subsection{Partially Accomplished}
|
|
jan@42381
|
216 |
\begin{frame}
|
|
jan@42381
|
217 |
\frametitle{Partially Accomplished}
|
|
jan@42401
|
218 |
\begin{spacing}{1.4}
|
|
jan@42381
|
219 |
\begin{itemize}
|
|
jan@42401
|
220 |
\item Guidelines for Upcoming TP-Programmers\\
|
|
jan@42401
|
221 |
{\small \textbf{Note:} Developement Enviroment and Languages Changes}
|
|
jan@42401
|
222 |
\item Examples
|
|
jan@42381
|
223 |
\end{itemize}
|
|
jan@42401
|
224 |
\end{spacing}
|
|
jan@42381
|
225 |
\end{frame}
|
|
jan@42381
|
226 |
|
|
jan@42381
|
227 |
\subsection{Not Accomplished}
|
|
jan@42381
|
228 |
\begin{frame}
|
|
jan@42381
|
229 |
\frametitle{Not Accomplished}
|
|
jan@42401
|
230 |
\begin{spacing}{1.2}
|
|
jan@42381
|
231 |
\begin{itemize}
|
|
jan@42401
|
232 |
\item Content of Interactiv Course Material\\
|
|
jan@42401
|
233 |
{\small Figures, Explenations,\ldots}
|
|
jan@42401
|
234 |
\item A Sufficient Count of Implementations
|
|
jan@42401
|
235 |
\item No Support of Labs and Lectures atm
|
|
jan@42401
|
236 |
\item No \emph{STEOP} Material atm
|
|
jan@42381
|
237 |
\end{itemize}
|
|
jan@42401
|
238 |
\end{spacing}
|
|
jan@42381
|
239 |
\end{frame}
|
|
jan@42381
|
240 |
|
|
jan@42381
|
241 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
242 |
\section{Conclusion}
|
|
jan@42381
|
243 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
244 |
|
|
jan@42381
|
245 |
\begin{frame}
|
|
jan@42381
|
246 |
\frametitle{Conculsion}
|
|
jan@42401
|
247 |
\begin{spacing}{1.2}
|
|
jan@42401
|
248 |
\begin{itemize}
|
|
jan@42401
|
249 |
\item TP-Programming Language not Ready
|
|
jan@42401
|
250 |
\item Not well documented
|
|
jan@42401
|
251 |
\vspace{5mm}
|
|
jan@42401
|
252 |
\item Hard to get Familar
|
|
jan@42401
|
253 |
\item Found Mistakes in own Work
|
|
jan@42401
|
254 |
\end{itemize}
|
|
jan@42401
|
255 |
\end{spacing}
|
|
jan@42381
|
256 |
\end{frame}
|
|
jan@42381
|
257 |
|
|
jan@42381
|
258 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
259 |
\end{document}
|
|
jan@42381
|
260 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
jan@42381
|
261 |
|
|
jan@42381
|
262 |
%% EOF |