1 \documentclass[a4paper, 12pt]{scrartcl} |
1 \documentclass[a4paper, 12pt]{article} |
2 |
2 |
3 \usepackage[english,german]{babel} |
3 \usepackage[english]{babel} |
4 \usepackage[T1]{fontenc} |
4 \usepackage[T1]{fontenc} |
5 \usepackage[latin1]{inputenc} |
5 \usepackage[latin1]{inputenc} |
6 |
6 |
|
7 \usepackage{url} |
7 \usepackage{graphicx} |
8 \usepackage{graphicx} |
8 \usepackage{endnotes} |
9 \usepackage{endnotes} |
9 \usepackage{trfsigns} |
10 \usepackage{trfsigns} |
10 \usepackage{setspace} |
11 \usepackage{setspace} |
11 \usepackage{isabelle} |
12 \usepackage{isabelle} |
12 \usepackage{isabellesym} |
13 \usepackage{isabellesym} |
|
14 \usepackage[pdfpagelabels]{hyperref} |
13 |
15 |
14 \bibliographystyle{alpha} |
16 \bibliographystyle{alpha} |
15 |
17 |
16 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
18 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
17 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
19 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
20 |
22 |
21 \title{ |
23 \title{ |
22 \Large{ |
24 \Large{ |
23 \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\ |
25 \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\ |
24 } |
26 } |
25 \sisac-Team of the Institute for Software Technology,\\~\\ |
27 \sisac-Team in Cooperation with \\~\\ |
26 in Cooperation with the Institute of Signal Processing and Speech Communication\\~\\ |
28 Institute for Software Technology\\ |
|
29 Institute of Signal Processing and Speech Communication\\~\\ |
27 Graz University of Technology\\ |
30 Graz University of Technology\\ |
28 \vspace{0.7cm} |
31 \vspace{0.7cm} |
29 \large{ |
32 \normalsize{ |
30 Advisor: tba |
33 Supervisor: Univ.-Prof. Dipl.-Ing. Dr.techn. Wotawa Franz |
31 } |
34 } |
32 } |
35 } |
33 \author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}} |
36 |
|
37 \author{Jan Simon Rocnik\\\href{mailto:student.tugraz.at}{\tt jan.rocnik@student.tugraz.at}} |
34 |
38 |
35 \date{\today} |
39 \date{\today} |
|
40 |
|
41 \begin{titlepage} |
36 \maketitle |
42 \maketitle |
37 \clearpage |
43 \thispagestyle{empty}\end{titlepage} |
|
44 \clearpage |
|
45 |
|
46 \setcounter{page}{2} |
|
47 \begin{center} |
|
48 Special Thanks to\\ |
|
49 \hfill \\ |
|
50 \emph{Dr.techn. Walther Neuper}\\ |
|
51 \emph{Dipl.-Ing. Bernhard Geiger} |
|
52 \end{center} |
|
53 \thispagestyle{empty} |
|
54 \clearpage |
|
55 |
|
56 |
|
57 \begin{abstract} |
|
58 The Baccalaureate Thesis creates interactive course material for Signal Processing based on the experimental math assistant Isabelle/\sisac. |
|
59 |
|
60 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. |
|
61 |
|
62 One challenge of this thesis is, that theory is not yet mechanized in Computer Theorem Provers (CTP); so this thesis will provide preliminary definitions in so-called \emph{theories} of the CTP Isabelle and theorems without proofs. |
|
63 |
|
64 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 ``CTP-based programming language'', because error messages are still not user-friendly and need frequent contact with \sisac-developers. |
|
65 |
|
66 So the practical outcome of this thesis is twofold: |
|
67 |
|
68 (1) 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 |
|
69 |
|
70 (2) a detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and \sisac-developers with feedback in usability of the CTP-based program language. |
|
71 \end{abstract}\clearpage |
|
72 |
|
73 |
|
74 \pagenumbering{Roman} |
38 \tableofcontents |
75 \tableofcontents |
39 \clearpage |
76 \clearpage |
40 |
77 \pagenumbering{arabic} |
41 \abstract{ |
78 |
42 abstract TODO\\ |
79 \setcounter{page}{5} |
43 } |
80 This thesis is structured as follows: |
44 |
81 |
45 This thesis is structured as follows |
82 \section{Introduction --TODO--} |
46 |
83 |
47 \section{Introduction} |
84 The motivation to this thesis mainly takes it source from thr practice of mathematics learning and further ... STEOP |
48 |
|
49 todo |
|
50 |
|
51 motivation from \textbf{practice of mathematics learning} ... STEOP |
|
52 |
85 |
53 \textbf{mathematics applied} in signal processing (SP) |
86 \textbf{mathematics applied} in signal processing (SP) |
54 |
87 |
55 mathematics mechanized in Computer Theorem Provers \textbf{(CTP)} ... (almost) traditional mathematical notation (predicate calculus) for axioms, definitions, lemmas, theorems. Recent developments provide also proofs in a humand readable format TODO |
88 mathematics mechanized in Computer Theorem Provers \textbf{(CTP)} ... (almost) traditional mathematical notation (predicate calculus) for axioms, definitions, lemmas, theorems. Recent developments provide also proofs in a humand readable format TODO |
56 |
89 |
80 todo |
113 todo |
81 |
114 |
82 \subsection{Milestones for the Project} |
115 \subsection{Milestones for the Project} |
83 Die Planung des Projekts teilt sich in folgende Iterationen: |
116 Die Planung des Projekts teilt sich in folgende Iterationen: |
84 \begin{enumerate} |
117 \begin{enumerate} |
85 \item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.) |
118 \item \textbf{Sammeln von Informationen "uber Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.) |
86 identify problems relevant for certain SP lectures |
119 identify problems relevant for certain SP lectures |
87 |
120 |
88 estimate chances to realized them within the scope of this thesis |
121 estimate chances to realized them within the scope of this thesis |
89 |
122 |
90 order for implementing the problems negotiated with lecturers |
123 order for implementing the problems negotiated with lecturers |
91 |
124 |
92 |
125 |
93 \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.) |
126 \item \textbf{1. Prsentation - Auswhlen der realisierbaren Themengebiete} (27.07.) |
94 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.) |
127 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.) |
95 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) |
128 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) |
96 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) |
129 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) |
97 \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo) |
130 \item \textbf{2. Prsentation - Abschluss der Arbeit} (todo) |
98 \end{enumerate} |
131 \end{enumerate} |
99 |
132 |
100 \subsection{Structure of the Thesis} |
133 \subsection{Structure of the Thesis} |
101 |
134 |
102 todo |
135 todo |
113 |
146 |
114 gap between what is available and what is required (@)! |
147 gap between what is available and what is required (@)! |
115 |
148 |
116 traditional notation ? |
149 traditional notation ? |
117 |
150 |
118 \subsection{Relevant Knowledge available in \isac} |
151 \subsection{Relevant Knowledge available in isac} |
119 todo |
152 todo |
120 |
153 |
121 specifications (``application axis'') and methods (``algorithmic axis'') |
154 specifications (``application axis'') and methods (``algorithmic axis'') |
122 |
155 |
123 partial fractions, cancellation of multivariate rational terms, ... |
156 partial fractions, cancellation of multivariate rational terms, ... |