1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/isac/jrocnik/TUGlogo.pdf Tue Nov 08 17:20:57 2011 +0100
1.3 @@ -0,0 +1,219 @@
1.4 +%PDF-1.3
1.5 +%âãÏÓ
1.6 +2 0 obj
1.7 +<<
1.8 +/Length 2930
1.9 +>>
1.10 +stream
1.11 +0 0.957 0.569 0 k
1.12 +/GS1 gs
1.13 +0 31.119 20.745 -20.746 re
1.14 +f
1.15 +22.819 31.119 20.746 -20.746 re
1.16 +f
1.17 +q
1.18 +1 i
1.19 +0 41.492 112.876 -41.432 re
1.20 +W n
1.21 +45.641 31.119 20.744 -20.746 re
1.22 +f
1.23 +10.372 20.746 20.747 -20.686 re
1.24 +f
1.25 +Q
1.26 +35.268 41.492 20.744 -20.746 re
1.27 +f
1.28 +0.941 0.82 0.808 0.894 k
1.29 +1 i
1.30 +75.104 27.791 m
1.31 +68.462 27.791 l
1.32 +68.462 31.11 l
1.33 +85.581 31.11 l
1.34 +85.581 27.791 l
1.35 +78.94 27.791 l
1.36 +78.94 10.417 l
1.37 +75.104 10.417 l
1.38 +75.104 27.791 l
1.39 +f
1.40 +q
1.41 +0 41.492 112.876 -41.432 re
1.42 +W n
1.43 +104.828 18.021 m
1.44 +104.828 16.774 104.604 15.649 104.156 14.646 c
1.45 +103.708 13.643 103.097 12.79 102.321 12.09 c
1.46 +101.546 11.387 100.631 10.848 99.57 10.469 c
1.47 +98.511 10.088 97.359 9.898 96.115 9.898 c
1.48 +94.873 9.898 93.722 10.088 92.661 10.469 c
1.49 +91.601 10.848 90.678 11.387 89.895 12.09 c
1.50 +89.109 12.79 88.497 13.643 88.061 14.646 c
1.51 +87.621 15.649 87.403 16.774 87.403 18.021 c
1.52 +87.403 31.11 l
1.53 +91.241 31.11 l
1.54 +91.241 18.153 l
1.55 +91.241 17.648 91.321 17.117 91.485 16.562 c
1.56 +91.648 16.008 91.919 15.497 92.298 15.029 c
1.57 +92.676 14.563 93.177 14.178 93.801 13.877 c
1.58 +94.423 13.576 95.194 13.425 96.115 13.425 c
1.59 +97.035 13.425 97.808 13.576 98.431 13.877 c
1.60 +99.054 14.178 99.556 14.563 99.934 15.029 c
1.61 +100.312 15.497 100.582 16.008 100.746 16.562 c
1.62 +100.909 17.117 100.991 17.648 100.991 18.153 c
1.63 +100.991 31.11 l
1.64 +104.828 31.11 l
1.65 +104.828 18.021 l
1.66 +f
1.67 +83.257 7.566 m
1.68 +82.496 7.895 81.511 8.052 80.723 8.052 c
1.69 +78.43 8.052 77.162 6.609 77.162 4.734 c
1.70 +77.162 2.873 78.401 1.471 80.497 1.471 c
1.71 +81.032 1.471 81.456 1.523 81.793 1.602 c
1.72 +81.793 3.987 l
1.73 +79.71 3.987 l
1.74 +79.71 5.43 l
1.75 +83.679 5.43 l
1.76 +83.679 0.5 l
1.77 +82.638 0.238 81.553 0.028 80.497 0.028 c
1.78 +77.316 0.028 75.106 1.51 75.106 4.604 c
1.79 +75.106 7.737 77.162 9.494 80.497 9.494 c
1.80 +81.638 9.494 82.538 9.35 83.383 9.113 c
1.81 +83.257 7.566 l
1.82 +f
1.83 +85.62 6.938 m
1.84 +87.296 6.938 l
1.85 +87.296 5.403 l
1.86 +87.324 5.403 l
1.87 +87.408 6.033 88.182 7.095 89.308 7.095 c
1.88 +89.491 7.095 89.689 7.095 89.885 7.042 c
1.89 +89.885 5.272 l
1.90 +89.717 5.363 89.379 5.416 89.04 5.416 c
1.91 +87.507 5.416 87.507 3.633 87.507 2.664 c
1.92 +87.507 0.186 l
1.93 +85.62 0.186 l
1.94 +85.62 6.938 l
1.95 +f
1.96 +93.587 1.312 m
1.97 +94.164 1.312 94.614 1.549 94.909 1.916 c
1.98 +95.219 2.296 95.304 2.781 95.304 3.306 c
1.99 +94.487 3.306 l
1.100 +93.644 3.306 92.391 3.175 92.391 2.139 c
1.101 +92.391 1.563 92.911 1.312 93.587 1.312 c
1.102 +h
1.103 +91.376 6.583 m
1.104 +92.107 6.898 93.094 7.095 93.896 7.095 c
1.105 +96.105 7.095 97.021 6.242 97.021 4.249 c
1.106 +97.021 3.384 l
1.107 +97.021 2.703 97.035 2.191 97.049 1.693 c
1.108 +97.063 1.182 97.091 0.71 97.134 0.186 c
1.109 +95.473 0.186 l
1.110 +95.402 0.539 95.402 0.985 95.389 1.195 c
1.111 +95.359 1.195 l
1.112 +94.924 0.448 93.979 0.028 93.122 0.028 c
1.113 +91.842 0.028 90.588 0.749 90.588 2.034 c
1.114 +90.588 3.043 91.108 3.633 91.827 3.961 c
1.115 +92.546 4.289 93.474 4.355 94.263 4.355 c
1.116 +95.304 4.355 l
1.117 +95.304 5.442 94.783 5.81 93.671 5.81 c
1.118 +92.869 5.81 92.066 5.522 91.434 5.076 c
1.119 +91.376 6.583 l
1.120 +f
1.121 +98.569 6.938 m
1.122 +104.312 6.938 l
1.123 +104.312 5.495 l
1.124 +100.707 1.549 l
1.125 +104.438 1.549 l
1.126 +104.438 0.186 l
1.127 +98.414 0.186 l
1.128 +98.414 1.615 l
1.129 +102.087 5.574 l
1.130 +98.569 5.574 l
1.131 +98.569 6.938 l
1.132 +f
1.133 +0 0.957 0.569 0 k
1.134 +105.965 6.911 6.911 -6.851 re
1.135 +f
1.136 +Q
1.137 +endstream
1.138 +endobj
1.139 +3 0 obj
1.140 +<<
1.141 +/ProcSet [/PDF ]
1.142 +/ExtGState <<
1.143 +/GS1 4 0 R
1.144 +>>
1.145 +>>
1.146 +endobj
1.147 +4 0 obj
1.148 +<<
1.149 +/Type /ExtGState
1.150 +/SA false
1.151 +/SM 0.02
1.152 +/OP false
1.153 +/op false
1.154 +/OPM 1
1.155 +/BG2 /Default
1.156 +/UCR2 /Default
1.157 +/HT /Default
1.158 +/TR2 /Default
1.159 +>>
1.160 +endobj
1.161 +1 0 obj
1.162 +<<
1.163 +/Type /Page
1.164 +/Parent 5 0 R
1.165 +/Resources 3 0 R
1.166 +/Contents 2 0 R
1.167 +>>
1.168 +endobj
1.169 +6 0 obj
1.170 +<<
1.171 +/S /D
1.172 +>>
1.173 +endobj
1.174 +7 0 obj
1.175 +<<
1.176 +/Nums [0 6 0 R ]
1.177 +>>
1.178 +endobj
1.179 +5 0 obj
1.180 +<<
1.181 +/Type /Pages
1.182 +/Kids [1 0 R]
1.183 +/Count 1
1.184 +/MediaBox [0 0 113 42]
1.185 +>>
1.186 +endobj
1.187 +8 0 obj
1.188 +<<
1.189 +/CreationDate (D:20060111234722+13'00')
1.190 +/ModDate (D:20060111234722+13'00')
1.191 +/Producer (PSNormalizer.framework)
1.192 +>>
1.193 +endobj
1.194 +9 0 obj
1.195 +<<
1.196 +/Type /Catalog
1.197 +/Pages 5 0 R
1.198 +/PageLabels 7 0 R
1.199 +>>
1.200 +endobj
1.201 +xref
1.202 +0 10
1.203 +0000000000 65535 f
1.204 +0000003204 00000 n
1.205 +0000000016 00000 n
1.206 +0000002998 00000 n
1.207 +0000003064 00000 n
1.208 +0000003349 00000 n
1.209 +0000003284 00000 n
1.210 +0000003311 00000 n
1.211 +0000003429 00000 n
1.212 +0000003560 00000 n
1.213 +trailer
1.214 +<<
1.215 +/Size 10
1.216 +/Root 9 0 R
1.217 +/Info 8 0 R
1.218 +/ID [<99444215e2a4a31d5c4ca09b38102d5e><99444215e2a4a31d5c4ca09b38102d5e>]
1.219 +>>
1.220 +startxref
1.221 +3627
1.222 +%%EOF
2.1 --- a/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Thu Nov 03 11:50:02 2011 +0100
2.2 +++ b/doc-src/isac/jrocnik/bakkarbeit_jrocnik.tex Tue Nov 08 17:20:57 2011 +0100
2.3 @@ -4,14 +4,6 @@
2.4 %2345678901234567890123456789012345678901234567890123456789012345678901234567890
2.5 % 10 20 30 40 50 60 70 80
2.6
2.7 -%TODO:
2.8 -%%\cite{proakis2004contemporary}
2.9 -%%
2.10 -%%patch:
2.11 -%%structur: theory part ersetzt project undamentals
2.12 -%% "mechanization of math in isac" ersetzt introduction
2.13 -%% authoring math in isac ersetzt mechanization
2.14 -
2.15 %define document class
2.16 \documentclass[a4paper, 12pt]{article}
2.17
2.18 @@ -53,18 +45,19 @@
2.19
2.20 \begin{document}
2.21
2.22 -%----------// TITLE PAGE \\----------%
2.23 +%----------// TITLE PAGE \\----------%1
2.24
2.25 \input{./bakkarbeit_titlepage.tex}
2.26 -\cleardoublepage
2.27 +\newpage
2.28
2.29 -%----------// EMPTY PAGE \\----------%
2.30 -
2.31 -%todo
2.32 -
2.33 -%----------// THANKS \\----------%
2.34 +%----------// EMPTY PAGE \\----------%2
2.35
2.36 \setcounter{page}{2}
2.37 +\thispagestyle{empty}\mbox{}\newpage
2.38 +
2.39 +%----------// THANKS \\----------%3
2.40 +
2.41 +\setcounter{page}{3}
2.42 \begin{center}
2.43 Special Thanks to\\
2.44 \hfill \\
2.45 @@ -72,19 +65,19 @@
2.46 \emph{Dipl.-Ing. Bernhard Geiger}
2.47 \end{center}
2.48 \thispagestyle{empty}
2.49 -\cleardoublepage
2.50 +\newpage
2.51
2.52 -%----------// EMPTY PAGE \\----------%
2.53 +%----------// EMPTY PAGE \\----------%4
2.54
2.55 -%todo
2.56 +\thispagestyle{empty}\mbox{}\newpage
2.57
2.58 -%----------// ABSTRACT \\----------%
2.59 +%----------// ABSTRACT \\----------%5
2.60
2.61 \begin{abstract}
2.62 The Baccalaureate Thesis creates interactive course material for Signal Processing (SP) based on the experimental educational math assistant Isabelle/{\sisac} ({\em Isa}belle for Transparent {\em C}alculations in Applied Mathematics).
2.63 \par The content of the course material is defined together with the Signal Processing and Speech Communication Laboratory (SPSC Lab) of Graz University of Technology (TUG). The content is planned to be used in specific lectures and labs of the SPSC and thus is thoroughly concerned with underlying mathematical and physical theory.
2.64 One challenge of this thesis is, that much theory required for SPSC is not yet mechanized in Computer Theorem Provers (CTP); so this thesis will provide preliminary definitions and theorems (without proofs~!) implemented in Isabelle \emph{theories}.
2.65 -\par Another callenge is the implementation of interactive courses: this is done within the educational math assistant Isabelle/{\sisac}, which is under development at TU Graz. The present state of {\sisac{}} happens to provide the {\em first} occasion for authoring by a non-member of the {\sisac}-developer team. So this challenge involves alpha-testing of the underlying \emph{CTP-based programming language}, because error messages are still not user-friendly and need frequent contact with {\sisac}-developers.
2.66 +\par Another challenge is the implementation of interactive courses: this is done within the educational math assistant Isabelle/{\sisac}, which is under development at TU Graz. The present state of {\sisac{}} happens to provide the {\em first} occasion for authoring by a non-member of the {\sisac}-developer team. So this challenge involves alpha-testing of the underlying \emph{CTP-based programming language}, because error messages are still not user-friendly and need frequent contact with {\sisac}-developers.
2.67 So the practical outcome of this thesis is twofold:
2.68 \begin{enumerate}
2.69 \item Interactive course material hopefully useful in education within the SPSC Lab and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and
2.70 @@ -93,24 +86,27 @@
2.71 \end{abstract}
2.72 \clearpage
2.73
2.74 -%----------// T O C \\----------%
2.75 +%----------// EMPTY PAGE \\----------%6
2.76 +
2.77 +\thispagestyle{empty}\mbox{}\newpage
2.78 +
2.79 +%----------// T O C \\----------%7
2.80
2.81 \pagenumbering{Roman}
2.82 %This thesis is structured into a fundamental part introducing the motivation, the basic notions concerning the thesis aswell as the {\sisac{}} project and describing the mathematic base. Further a automatically generated practical part representing the work on {\sisac{}} which can be extended.
2.83 \tableofcontents
2.84 \clearpage
2.85 \pagenumbering{arabic}
2.86 -\setcounter{page}{6}
2.87 +\setcounter{page}{8}
2.88
2.89 %----------// PART-1 \\----------%
2.90
2.91 \part{Project Fundamentals}
2.92
2.93 -%The goals of the thesis are finally defined in section \ref{sec:goals} which seems to be very late. The reason for this fact is that there has a lot of research to be done prior and a lot of this research has to be described in this thesis before we are able to define the proper goals. All this is neccessary for understanding the effort on this work.
2.94 -
2.95 \section{Introduction}
2.96 +%TODO personal decision no workds like feeling
2.97 %The motivation to this thesis mainly takes it source from the feeling of understanding difficult signal processing tasks and the will to help others to get this feeling to.
2.98 -%\par Signal Processing (SP) requieres a huge range of mathematic knowledge as well as a feeling for simplification and number tricks but even though this fact, the operations themself are no higher ones. The main task is to understand. Aside this description we think of the classic math ideas and techniques, consisting of predefined formulas, notations and forumularsations we learn.
2.99 +%\par Signal Processing (SP) requieres a huge range of mathematic knowledge as well as a feeling for simplification and number tricks but even though this fact, the operations themself are no higher ones. The main task is to understand. Aside this description we think of the classic math ideas and techniques, consisting of...
2.100 %
2.101 Didactics of mathematics faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which ususally are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing.
2.102
2.103 @@ -124,19 +120,20 @@
2.104 \medskip
2.105 The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part.
2.106
2.107 -In part I, \S\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (\S\ref{emas}) and introduces the notions required for the implementation work (\S\ref{math-auth}). In particular, \S\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to \S\ref{sec:goals}.
2.108 +In part I, Section~\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (Section~\ref{emas}) and introduces the notions required for the implementation work (Section~\ref{math-auth}). In particular, Section~\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to Section~\ref{sec:goals}.
2.109
2.110 -\S\ref{sp} analyzes ten (TODO: exact no?) problems defined by the SPSC Lab for the knowledge already provided (\S\ref{know-isab}, \S\ref{know-isac}), discusses the selection of problems for implementation (\S\ref{know-missing}) TODO: further structure ?
2.111 +Section~\ref{sp} analyzes ten (TODO: exact no?) problems defined by the SPSC Lab for the knowledge already provided (Section~\ref{know-isab}, Section~\ref{know-isac}), discusses the selection of problems for implementation (Section~\ref{know-missing}) TODO: further structure ?
2.112 %(\S\ref{})
2.113
2.114 \section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac}
2.115 -%A problem behind is the mechanization of mathematic theories in CTP-bases languages. There is still a hugh gap between these theories and this what we call an applications - in Example Signal Processing.
2.116 +%no CTP!!!
2.117 +%A problem behind is the mechanization of mathematic theories in CTP-bases languages. There is still a huge gap between these algoritms and this what we want as a solution - in Example Signal Processing.
2.118 %\begin{example}
2.119 % \[
2.120 % X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY
2.121 % \]
2.122 % {\small\textit{
2.123 -% \noindent A very simple example on this what we call gap is the simplification above. It is needles to say that it is correct and also isabell forfills it correct - \emph{always}. But sometimes we don't want do simplificate these things, sometimes it is easyer for handling and understanding if we keep terms together. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between applications and theorem proofment.
2.124 +% \noindent A very simple example on this what we call gap is the simplification above. It is needles to say that it is correct and also isabell forfills it correct - \emph{always}. But sometimes we don't want expand such terms, sometimes we want another structure of them. Think of a problem were we now would need only the coefficients of $X$ and $Y$. This is what we call the gap between mechanical simplification and the solution.
2.125 % }}
2.126 % \caption{Correct but not usefull}\label{eg:gap}
2.127 %\end{example}
2.128 @@ -288,9 +285,9 @@
2.129 partial fractions, cancellation of multivariate rational terms, ...
2.130
2.131 \subsection{Survey: Requiered Knowledge and Selected Problem(s)}\label{know-missing}
2.132 -Following tables are showing the expected development effort for speciefic problems. The values are only very inaccurately approximations of the real work, but needed as a basis for descieding with which problem to start:
2.133 +Following tables (Table~\ref{tab:eff-four},~\ref{tab:eff-conv},~\ref{tab:eff-ztrans}) are showing the expected development effort for speciefic problems. The values are only very inaccurately approximations of the real work, but needed as a basis for descieding with which problem to start:
2.134
2.135 -\begin{table}[!H]
2.136 +\begin{table}[h]
2.137 \begin{centering}
2.138 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
2.139 requirements & comments &effort\\ \hline\hline
2.140 @@ -302,10 +299,10 @@
2.141 \multicolumn{2}{c|}{} & 70-80\\
2.142 \end{tabular}
2.143 \par\end{centering}
2.144 -\caption{Fourier-Transformation development effort}
2.145 +\caption{Fourier-Transformation development effort\label{tab:eff-four}}
2.146 \end{table}
2.147
2.148 -\begin{table}[H]
2.149 +\begin{table}[h]
2.150 \begin{centering}
2.151 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
2.152 requirements & comments &effort\\ \hline\hline
2.153 @@ -319,10 +316,10 @@
2.154 \multicolumn{2}{c|}{} & 70-90\\
2.155 \end{tabular}
2.156 \par\end{centering}
2.157 -\caption{Convolution Operations development effort}
2.158 +\caption{Convolution Operations development effort\label{tab:eff-conv}}
2.159 \end{table}
2.160
2.161 -\begin{table}[H]
2.162 +\begin{table}[h]
2.163 \begin{centering}
2.164 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}}
2.165 requirements & comments &effort\\ \hline\hline
2.166 @@ -339,7 +336,7 @@
2.167 % & & 1 MT
2.168 \end{tabular}
2.169 \par\end{centering}
2.170 -\caption{Z-Transformation development effort}
2.171 +\caption{Z-Transformation development effort\label{tab:eff-ztrans}}
2.172 \end{table}
2.173
2.174 As conclusion of the summerized efforts it is evident that only one topic can be tried to realized as a baccalaureate thesis. In accord with Dr. Neuper we decided after some practical tests to start with the implementation of the (Inverse) Z-Transformation. The Reason is that this topic can mostly be done with knowledge which was already tried to be mechanized in {\sisac}.