|
1 % Title: bakkarbeit_jrocnik.tex |
|
2 % Author: Jan Rocnik |
|
3 % (c) copyright due to lincense terms. |
|
4 %2345678901234567890123456789012345678901234567890123456789012345678901234567890 |
|
5 % 10 20 30 40 50 60 70 80 |
|
6 |
|
7 %TODO: |
|
8 %%\cite{proakis2004contemporary} |
|
9 %%--01-- pointer or label to related works |
|
10 |
|
11 %define document class |
1 \documentclass[a4paper, 12pt]{article} |
12 \documentclass[a4paper, 12pt]{article} |
2 |
13 |
|
14 %packages for language and input |
3 \usepackage[english]{babel} |
15 \usepackage[english]{babel} |
4 \usepackage[T1]{fontenc} |
16 \usepackage[T1]{fontenc} |
5 \usepackage[latin1]{inputenc} |
17 \usepackage[latin1]{inputenc} |
6 |
18 |
|
19 %generel packages |
7 \usepackage{url} |
20 \usepackage{url} |
8 \usepackage{graphicx} |
21 \usepackage{graphicx} |
9 \usepackage{endnotes} |
22 \usepackage{endnotes} |
10 \usepackage{trfsigns} |
23 \usepackage{trfsigns} |
11 \usepackage{setspace} |
24 \usepackage{setspace} |
12 \usepackage[pdfpagelabels]{hyperref} |
25 \usepackage[pdfpagelabels]{hyperref} |
13 \usepackage{longtable} |
26 \usepackage{longtable} |
14 %isabelle relevant |
27 |
|
28 %isabelle relevant packages |
15 \usepackage{isabelle,isabellesym} |
29 \usepackage{isabelle,isabellesym} |
16 \usepackage{pdfsetup} |
30 |
17 |
31 %define isac logos |
18 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
32 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
19 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
33 \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} |
|
34 |
|
35 %----------// BEGIN DOCUMENT \\----------% |
20 |
36 |
21 \begin{document} |
37 \begin{document} |
22 |
38 |
23 %----------// INFO SETUP \\----------% |
39 %----------// INFO SETUP \\----------% |
24 |
40 |
89 |
105 |
90 %----------// PART-1 \\----------% |
106 %----------// PART-1 \\----------% |
91 |
107 |
92 \part{Project Fundamentals} |
108 \part{Project Fundamentals} |
93 |
109 |
94 \section{Introduction --TODO--} |
110 \section{Introduction} |
95 |
111 |
96 The motivation to this thesis mainly takes it source from thr practice of mathematics learning and further ... STEOP |
112 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. |
97 \cite{proakis2004contemporary} |
113 \par Signal Processing 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. |
98 |
114 \par Mathematics mechanized in Computer Theorem Provers \emph{(CTP)} has (almost) a problem with traditional mathematical notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer programm or script is not able to interpret every greek or latin letter and every greek, latin or whatever calculations symbol. Also if we would be able to handle thehse symbols we would have a problem to interpret them correctly. In different problems, symbols and letters have different meanings and ask for different ways to get through. Exclusive from the input, also the output can be a problem. We are familar with a specified notations and style taught in university but a computer programm has no knowledge of the form probved by a professor and the maschines themselve also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a humand readable format but according to the fact that there is no mony for good working formel editors yet, the style is one thing we have to live with. |
99 \textbf{mathematics applied} in signal processing (SP) |
115 \par This thesis tries to \empg{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. For others see related works. %--01-- |
100 |
116 The major challenge of the practical part, of this thesis, is, that "`connecting the two worlds"' involves programming in a CTP-based programming language which is in a very early state of prototyping. There is no concrete experience data ready to hand. |
101 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 |
|
102 |
|
103 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work |
|
104 |
|
105 the major challenge of the practical part is, that ``connecting the two worlds'' involves programming in a CTP-based programming language which is in a very early state of prototyping. |
|
106 |
117 |
107 \subsection{Mechanization of Mathematics} |
118 \subsection{Mechanization of Mathematics} |
108 |
119 |
109 todo |
120 todo |
110 |
121 |