equal
deleted
inserted
replaced
36 \maketitle |
36 \maketitle |
37 \clearpage |
37 \clearpage |
38 \tableofcontents |
38 \tableofcontents |
39 \clearpage |
39 \clearpage |
40 |
40 |
|
41 \abstract{ |
|
42 abstract TODO\\ |
|
43 } |
|
44 |
|
45 This thesis is structured as follows |
41 |
46 |
42 \section{Introduction} |
47 \section{Introduction} |
43 |
48 |
44 todo |
49 todo |
45 |
50 |
48 \textbf{mathematics applied} in signal processing (SP) |
53 \textbf{mathematics applied} in signal processing (SP) |
49 |
54 |
50 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 |
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 |
51 |
56 |
52 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work |
57 This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work |
|
58 |
|
59 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. |
53 |
60 |
54 \subsection{Mechanization of Mathematics} |
61 \subsection{Mechanization of Mathematics} |
55 |
62 |
56 todo |
63 todo |
57 |
64 |