wneuper/isa: doc-isac/jrocnik/jrocnik

     1 \documentclass[%

     2 %handout, % prints handouts (=no animations, for printed version)

     3 %mathserif

     4 %xcolor=pst,

     5 14pt

     6 % fleqn

     7 ]{beamer}

     9 \usepackage{beamerthemedefault}

    11 \usepackage{color}

    12 \definecolor{lgray}{RGB}{238,238,238}

    13 \definecolor{gray}{rgb}{0.8,0.8,0.8}

    15 \useoutertheme[subsection=false]{smoothbars}

    16 %\useinnertheme{circles}

    18 \setbeamercolor{block title}{fg=black,bg=gray}

    19 \setbeamercolor{block title alerted}{use=alerted text,fg=black,bg=alerted text.fg!75!bg}

    20 \setbeamercolor{block title example}{use=example text,fg=black,bg=example text.fg!75!bg}

    21 \setbeamercolor{block body}{parent=normal text,use=block title,bg=block title.bg!25!bg}

    22 \setbeamercolor{block body alerted}{parent=normal text,use=block title alerted,bg=block title alerted.bg!25!bg}

    23 \setbeamercolor{block body example}{parent=normal text,use=block title example,bg=block title example.bg!25!bg}

    25 %activate hyperlinks at the end

    26 %\usepackage{hyperref}

    28 \usepackage[english]{babel}

    29 \usepackage[utf8]{inputenc}

    30 \usepackage{array}

    31 \usepackage{setspace}

    32 \usepackage{url}

    34 \definecolor{tug}{rgb}{0.96862,0.14509,0.27450}

    36 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}

    37 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}

    39 \setbeamertemplate{headline}[text line]{

    40 	\begin{beamercolorbox}[wd=\paperwidth,ht=8ex,dp=4ex]{}

    41 		\insertnavigation{0.85\paperwidth}

    42 		\raisebox{-10pt}{\includegraphics[width=15mm]{tuglogo}}\vskip2pt

    43 		\hskip-1pt\rule{\paperwidth}{0.3pt}

    44 	\end{beamercolorbox}

    45 }

    47 \setbeamertemplate{navigation symbols}{}

    48 \setbeamercolor{footline}{fg=black,bg=gray}

    50 % Fusszeile mit Autor, Titel und Foliennummer / Gesamtfolienzahl

    51 \setbeamertemplate{footline}[text line]{

    52 	\hskip-1pt

    53 	\begin{beamercolorbox}[wd=\paperwidth]{footline}

    54 			\rule{\paperwidth}{0.3pt}

    55 			\colorbox{tug}{\rule{3pt}{0pt}\rule{0pt}{3pt}}

    56 			\textbf{\rule{0pt}{5pt}\insertshortauthor\hfill\insertshortinstitute\hfill%

    57 					\insertshorttitle\rule{1em}{0pt}}

    58 			\rule{\paperwidth}{0.3pt}

    59 	\end{beamercolorbox}

    60 	\begin{beamercolorbox}[wd=\paperwidth,ht=2ex,dp=2ex]{white}

    61 	\end{beamercolorbox}

    62 }%

    64 %% Titelblatt-Einstellungen

    65 \institute[IST]{Institute for Software Technology\\Graz University of Technology}

    66 \title[ISAC for Signal Processing]{Interactive Course Material by TP-based Programming}

    67 \subtitle{A Case Study}

    68 \author{Jan Ro\v{c}nik}

    69 \date{24. June 2012}

    71 % Subject and Keywords for PDF

    72 \subject{CADGME Presentation}

    73 \keywords{interactive course material, signal processing, z transform, TP-based programming

    74 language, Lucas-Interpreter, Theorem Proving}

    76 \titlegraphic{\includegraphics[width=20mm]{tuglogo}}

    78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    79 \begin{document}

    80 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    82 \begin{frame}[plain]

    83   \frametitle{}

    84   \titlepage

    85 \end{frame}

    89 %\begin{frame}

    90 %  \frametitle{Contents}

    91 %  \begin{spacing}{0.3}

    92 %        \tableofcontents[hideallsubsections %

    93 %                        % ,pausesections

    94 %                        ] % erzeugt Inhaltsverzeichnis

    95 %  \end{spacing}

    96 %\end{frame}

    98 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    99 \section{Introduction}

   100 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   102 \subsection{isabelle}

   103 \begin{frame}

   104 	\frametitle{What is Isabelle?}

   105 	\begin{spacing}{2}

   106 		\begin{itemize}

   107 			\item Interactive Theorem Prover (Interactice TP)

   108 			\item Large body of mechanized math knowledge

   109 			\item Developed in Cambridge, Munich and Paris

   110 		\end{itemize}

   111 	\end{spacing}

   112 \end{frame}

   114 \subsection{isac}

   115 \begin{frame}

   116 	\frametitle{What is {\isac}?}

   117 	\begin{spacing}{1.7}

   118 		\begin{itemize}

   119 			\item \textcolor{tug}{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal A}$}belle for~{}\textcolor{tug}{${\cal C}$}alculations

   120 			\item Interactive Course Material

   121 			\item Learning Coach

   122 			\item Developed at Austrian Universities

   123 		\end{itemize}

   124 	\end{spacing}

   125 \end{frame}

   127 \subsection{motivation}

   128 \begin{frame}

   129 	\frametitle{{\isac{}} for Interactive Course Material}

   130 	\begin{itemize}

   131 		\item Stepwise solving of engineering problems\\

   132 					{\small $\rightarrow$ \textcolor{tug}{One Framework for all phases of problem solving}}

   133 		\item Explaining underlying knowledge\\

   134 					{\small $\rightarrow$  \textcolor{tug}{Transparent Content, Access to Multimedia Content}}

   135 		\item Checking steps input by the student\\

   136 					{\small $\rightarrow$ \textcolor{tug}{Proof Situation}}

   137 		\item Assessing stepwise problem solving\\

   138 					{\small $\rightarrow$ \textcolor{tug}{One system for tutoring and assessment}}

   139 	\end{itemize}

   140 \end{frame}

   143 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   144 \section{Material Creation}

   145 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   147 \subsection{steps}

   148 \begin{frame}

   149 	\frametitle{Course Material Creation {\normalsize Iterations}} %tasks? work flow?

   150 	\begin{spacing}{1.3}

   151 		\begin{enumerate}

   152 			\item Problem Analysis\\

   153 				{\small Variants of problem solving steps} %example partial fractions

   154 			\item \textbf{Analysis of mechanized knowledge}\\

   155 				{\small Existing and missing knowledge}

   156 			\item \textbf{Programming in a TP based language (TP-PL)}

   157 			\item Additional Content\\

   158 				{\small Multimedia explanations for underlying knowledge}

   159 		\end{enumerate}

   160 	\end{spacing}

   161 \end{frame}

   163 \subsection{issues}

   164 \begin{frame}

   165 	\frametitle{Issues to Accomplish {\normalsize Information Collection}}

   166 	\begin{spacing}{1.3}

   167 		\begin{itemize}

   168 			\item What knowledge is mechanized in Isabelle?\\

   169 						{\small Theorems, Definitions, Numbers,\ldots}

   170 			\item What knowledge is mechanized in {\isac{}}?\\

   171 						{\small Problem specifications, Programs,\ldots}

   172 			\item What additional explanations are required?\\

   173 				{\small Figures, Examples,\ldots}

   174 		\end{itemize}

   175 	\end{spacing}

   176 \end{frame}

   178 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   179 \section{Details}

   180 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   182 \subsection{Technical Survey}

   183 %\begin{frame}

   184 %	\frametitle{Technical Survey I {\normalsize Mechanizing Knowledge}}

   185 %	\begin{spacing}{1.5}

   186 %		\begin{itemize}

   187 %			\item Not enough knowledge is mechanized\\

   188 %						{\small Equation Solving, Integrals,\ldots}

   189 %			\item Computer Mathematicians required!\\

   190 %						{\small Mathematics: Equation solving, Engineer: Z-Transform}

   191 %			\item RISC Linz, Mathematics TU Graz

   192 %		\end{itemize}

   193 %	\end{spacing}

   194 %\end{frame}

   196 %\begin{frame}

   197 %	\frametitle{Technical Survey II {\normalsize Representation Problems} }

   198 %	\begin{spacing}{1.9}

   199 %		\begin{itemize}

   200 %			\item Different brackets have different meanings\\

   201 %						{\small $u[n]$ is a specific function application :) }

   202 %			\item We need Symbols, Indizes and Hochzahlen

   203 %			\item Different Representations for different purpos %winkel in polar oder kartesischen koordinaten usw.

   204 %		\end{itemize}

   205 %	\end{spacing}

   206 %\end{frame}

   208 \begin{frame}

   209 	\frametitle{Representation Problems}

   210 	\begin{spacing}{1.4}

   211 		\begin{center}

   213 			  \begin{itemize}

   214 			  		\item Can meaning of symbols be varied?\\

   215 							{\small $u[n]$ is a specific function in Signal Processing}

   216 						\item Simplification, tricks and beauty

   217 				\end{itemize}

   219 				{\small $X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY$}\\

   220 				\vspace{3mm}

   221 				{\small $\frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)=\frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=$}\\

   222 				{\small $=\frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}=\frac{1}{\omega}\,e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} $}

   225 		\end{center}

   226 	\end{spacing}

   227 \end{frame}

   229 \subsection{Demonstration}

   230 \begin{frame}

   231 	\frametitle{Demonstration}

   232 	\begin{spacing}{1.5}

   233 		\begin{itemize}

   234 			\item Backend

   235 			\begin{itemize}

   236 				\item Equation solving

   237 				\item Notation problems, Working with Rulesets

   238 				\item Framework expansion

   239 				\item My Work

   240 			\end{itemize}

   241 		\end{itemize}

   242 	\end{spacing}

   243 \end{frame}

   245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   246 \section{Summary}

   247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   249 \subsection{conclusion}

   250 \begin{frame}

   251 	\frametitle{Conclusion}

   252 	\begin{spacing}{1.2}

   253 	    \begin{itemize}

   254 	    	\item Proof of concept for TP-PL succesfull

   255 				\item Usability of TP-PL not sufficient

   256 				\item Requirements for improved usability clarified

   257 				\vspace{5mm}

   258 				\item Unacceptable to spend 200h on 1 program

   259 				\item \isac{} pointed at my own error

   260 			\end{itemize}

   261 		\end{spacing}

   262 \end{frame}

   264 \subsection{contact}

   265 \begin{frame}

   266 	\frametitle{Contact}

   267 	\begin{spacing}{1.7}

   268 	    \begin{tabular}{lr}

   269 				Isabelle & \small \texttt{\href{isabelle.in.tum.de}{isabelle.in.tum.de}}\\

   270 				The {\isac}-Project & \small \texttt{\href{www.ist.tugraz.at/isac}{www.ist.tugraz.at/isac}}\\

   271 				Project leader & \small \texttt{\href{mailto:wneuper@ist.tugraz.at}{wneuper@ist.tugraz.at}}\\

   272 				Jan Rocnik & \small \texttt{\href{mailto:jan.rocnik@student.tugraz.at}{jan.rocnik@student.tugraz.at}}

   273 			\end{tabular}

   274 		\end{spacing}

   275 \end{frame}

   277 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   278 \end{document}

   279 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   281 %% EOF

author	wneuper <Walther.Neuper@jku.at>
	Sun, 31 Dec 2023 09:42:27 +0100
changeset 60787	26037efefd61
parent 52107	f8845fc8f38d
permissions	-rwxr-xr-x