30 \clearpage |
30 \clearpage |
31 \tableofcontents |
31 \tableofcontents |
32 \clearpage |
32 \clearpage |
33 |
33 |
34 |
34 |
35 \section{Zur Aufgabenstellung} |
35 \section{Introduction} |
36 |
36 |
37 todo |
37 todo |
38 |
38 |
39 \section{Planung des Projektes} |
39 motivation from \textbf{practice of mathematics learning} ... STEOP |
|
40 |
|
41 \textbf{mathematics applied} in signal processing (SP) |
|
42 |
|
43 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 \cite{TODO} |
|
44 |
|
45 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work |
|
46 |
|
47 \subsection{Mechanization of Mathematics} |
40 |
48 |
41 todo |
49 todo |
42 |
50 |
43 \subsection{Zeitplanung des Projekt} |
51 hughe theories of mathematics |
|
52 |
|
53 still a hugh gap between these theories and ``real applications'' e.g. in SP |
|
54 |
|
55 ? academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modelling --- mechanized math starts from mathematical models and (hopefully !) proceeds to match physics. |
|
56 |
|
57 CTP Isabelle ... survey of knowledge, links to knowledge |
|
58 |
|
59 \paragraph{\sisac} |
|
60 TODO |
|
61 |
|
62 adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics. |
|
63 |
|
64 \subsection{Goals of the Thesis} |
|
65 |
|
66 todo |
|
67 |
|
68 \subsection{Milestones for the Project} |
44 Die Planung des Projekts teilt sich in folgende Iterationen: |
69 Die Planung des Projekts teilt sich in folgende Iterationen: |
45 \begin{enumerate} |
70 \begin{enumerate} |
46 \item \textbf{Sammeln von Informationen über Themengebite und deren Realisierbarkeit } (29.06. -- 27.07.) |
71 \item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.) |
|
72 identify problems relevant for certain SP lectures |
|
73 |
|
74 estimate chances to realized them within the scope of this thesis |
|
75 |
|
76 order for implementing the problems negotiated with lecturers |
|
77 |
|
78 |
47 \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.) |
79 \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.) |
48 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.) |
80 \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.) |
49 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) |
81 \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) |
50 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) |
82 \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) |
51 \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo) |
83 \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo) |
52 \end{enumerate} |
84 \end{enumerate} |
53 |
85 |
54 \section{Konzepte und Lösungen} |
86 \subsection{Structure of the Thesis} |
|
87 |
55 todo |
88 todo |
|
89 |
|
90 \section{Mechanization of Mathematics for SP Problems} |
|
91 todo |
|
92 |
|
93 \subsection{Relevant Knowledge available in Isabelle} |
|
94 todo |
|
95 |
|
96 \paragraph{example FFT}, describe in detail !!!! |
|
97 |
|
98 ? different meaning: FFT in Maple |
|
99 |
|
100 gap between what is available and what is required (@)! |
|
101 |
|
102 traditional notation ? |
|
103 |
|
104 \subsection{Relevant Knowledge available in \isac} |
|
105 todo |
|
106 |
|
107 specifications (``application axis'') and methods (``algorithmic axis'') |
|
108 |
|
109 partial fractions, cancellation of multivariate rational terms, ... |
|
110 |
|
111 \subsection{Survey: Available Knowledge and Selected Problems} |
|
112 todo |
|
113 |
|
114 estimate gap (@) for each problem (tables) |
|
115 |
|
116 conclusion: following order for implementing the problems ... |
|
117 |
|
118 \subsection{Formalization of missing knowledge in Isabelle} |
|
119 todo |
|
120 |
|
121 axiomatization ... where ... and |
|
122 |
|
123 \subsection{Notes on Problems with Traditional Notation} |
|
124 todo |
|
125 |
|
126 u[n] !! |
|
127 |
|
128 f x = why not f(x) ?!?! |
|
129 |
|
130 ... |
|
131 |
|
132 \section{Implementation of Certain SP Problems} |
|
133 todo |
|
134 |
|
135 \subsection{Formal Specification of Problems} |
|
136 todo |
|
137 |
|
138 \subsection{Methods Solving the Problems} |
|
139 todo |
|
140 |
|
141 \subsection{Integration of Subproblems available in \isac} |
|
142 todo |
|
143 |
|
144 \subsection{Examples and Multimedia Content} |
|
145 todo |
|
146 |
|
147 |
|
148 \section{Related Work and Open Questions} |
|
149 todo |
|
150 |
|
151 See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work |
|
152 |
|
153 |
|
154 |
56 \section{Beschreibung der Meilensteine}\label{ms-desc} |
155 \section{Beschreibung der Meilensteine}\label{ms-desc} |
57 todo |
156 todo |
58 \section{Bericht zum Projektverlauf} |
157 \section{Bericht zum Projektverlauf} |
59 todo |
158 todo |
60 \section{Abschliesende Bemerkungen} |
159 \section{Abschliesende Bemerkungen} |