jan@42246: \documentclass[a4paper, 12pt]{scrartcl} jan@42235: jan@42246: \usepackage[english,german]{babel} jan@42235: \usepackage[T1]{fontenc} jan@42235: \usepackage[latin1]{inputenc} jan@42235: neuper@42073: \usepackage{graphicx} jan@42246: \usepackage{endnotes} jan@42246: \usepackage{trfsigns} jan@42246: \usepackage{setspace} jan@42251: \usepackage{isabelle} jan@42251: \usepackage{isabellesym} jan@42235: neuper@42073: \bibliographystyle{alpha} neuper@42073: neuper@42073: \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} neuper@42073: \def\sisac{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$} neuper@42073: neuper@42073: \begin{document} neuper@42073: jan@42235: \title{ jan@42235: \Large{ jan@42235: \bf Interactive Course Material for Signal Processing based on Isabelle/\isac\\~\\ jan@42235: } jan@42276: \sisac-Team of the Institute for Software Technology,\\~\\ jan@42276: in Cooperation with the Institute of Signal Processing and Speech Communication\\~\\ jan@42276: Graz University of Technology\\ jan@42235: \vspace{0.7cm} jan@42235: \large{ jan@42276: Advisor: tba jan@42235: } jan@42235: } jan@42235: \author{Jan Simon Rocnik\\{\tt jan.rocnik@student.tugraz.at}} jan@42235: jan@42235: \date{\today} neuper@42073: \maketitle neuper@42073: \clearpage neuper@42073: \tableofcontents neuper@42073: \clearpage neuper@42073: neuper@42304: \abstract{ neuper@42304: abstract TODO\\ neuper@42304: } neuper@42304: neuper@42304: This thesis is structured as follows neuper@42073: neuper@42240: \section{Introduction} neuper@42073: jan@42235: todo neuper@42073: neuper@42240: motivation from \textbf{practice of mathematics learning} ... STEOP neuper@42240: neuper@42240: \textbf{mathematics applied} in signal processing (SP) neuper@42240: jan@42253: 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 neuper@42240: neuper@42240: This thesis tries to \textbf{connect these two worlds} ... this trial is one of the first; others see related work neuper@42240: neuper@42304: 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. neuper@42304: neuper@42240: \subsection{Mechanization of Mathematics} neuper@42073: jan@42235: todo neuper@42073: neuper@42240: hughe theories of mathematics neuper@42240: neuper@42240: still a hugh gap between these theories and ``real applications'' e.g. in SP neuper@42240: neuper@42240: ? 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. neuper@42240: neuper@42240: CTP Isabelle ... survey of knowledge, links to knowledge neuper@42240: neuper@42240: \paragraph{\sisac} neuper@42240: TODO neuper@42240: neuper@42240: adds an ``application'' axis (formal specifications of problems) and an ``algorithmic'' axis to the ``deductive'' axis of knowledge ... 3-dimensional universe of mathematics. neuper@42240: neuper@42240: \subsection{Goals of the Thesis} neuper@42240: neuper@42240: todo neuper@42240: neuper@42240: \subsection{Milestones for the Project} jan@42235: Die Planung des Projekts teilt sich in folgende Iterationen: neuper@42073: \begin{enumerate} neuper@42240: \item \textbf{Sammeln von Informationen über Themengebiete und deren Realisierbarkeit } (29.06. -- 27.07.) neuper@42240: identify problems relevant for certain SP lectures neuper@42240: neuper@42240: estimate chances to realized them within the scope of this thesis neuper@42240: neuper@42240: order for implementing the problems negotiated with lecturers neuper@42240: neuper@42240: jan@42235: \item \textbf{1. Präsentation - Auswählen der realisierbaren Themengebiete} (27.07.) jan@42235: \item \textbf{Ausarbeiten der Aufgaben in \isac} (01.09. -- 11.11.) jan@42235: \item \textbf{Dokumentation der Aufgaben} (14.11. -- 02.12.) jan@42235: \item \textbf{Ausarbeitung in Latex, Bakkarbeit} (05.12. -- todo) jan@42235: \item \textbf{2. Präsentation - Abschluss der Arbeit} (todo) neuper@42073: \end{enumerate} neuper@42073: neuper@42240: \subsection{Structure of the Thesis} neuper@42240: jan@42235: todo neuper@42240: neuper@42240: \section{Mechanization of Mathematics for SP Problems} neuper@42240: todo neuper@42240: neuper@42240: \subsection{Relevant Knowledge available in Isabelle} neuper@42240: todo neuper@42240: neuper@42240: \paragraph{example FFT}, describe in detail !!!! neuper@42240: neuper@42240: ? different meaning: FFT in Maple neuper@42240: neuper@42240: gap between what is available and what is required (@)! neuper@42240: neuper@42240: traditional notation ? neuper@42240: neuper@42240: \subsection{Relevant Knowledge available in \isac} neuper@42240: todo neuper@42240: neuper@42240: specifications (``application axis'') and methods (``algorithmic axis'') neuper@42240: neuper@42240: partial fractions, cancellation of multivariate rational terms, ... neuper@42240: neuper@42240: \subsection{Survey: Available Knowledge and Selected Problems} neuper@42240: todo neuper@42240: neuper@42240: estimate gap (@) for each problem (tables) neuper@42240: neuper@42240: conclusion: following order for implementing the problems ... neuper@42240: neuper@42240: \subsection{Formalization of missing knowledge in Isabelle} neuper@42240: todo neuper@42240: neuper@42240: axiomatization ... where ... and neuper@42240: neuper@42240: \subsection{Notes on Problems with Traditional Notation} neuper@42240: todo neuper@42240: neuper@42240: u[n] !! neuper@42240: neuper@42240: f x = why not f(x) ?!?! neuper@42240: neuper@42240: ... neuper@42240: jan@42276: terms are not full simplified in traditional notations, in isac we have to simplify them complete to check weather results are compatible or not. in e.g. the solutions of an second order linear equation is an rational in isac but in tradition we keep fractions as long as possible and as long as they are 'beautiful' (1/8, 5/16,...) jan@42276: neuper@42240: \section{Implementation of Certain SP Problems} neuper@42240: todo neuper@42240: neuper@42240: \subsection{Formal Specification of Problems} neuper@42240: todo neuper@42240: neuper@42240: \subsection{Methods Solving the Problems} neuper@42240: todo neuper@42240: neuper@42240: \subsection{Integration of Subproblems available in \isac} neuper@42240: todo neuper@42240: neuper@42240: \subsection{Examples and Multimedia Content} neuper@42240: todo neuper@42240: neuper@42240: neuper@42240: \section{Related Work and Open Questions} neuper@42240: todo neuper@42240: neuper@42240: See ``introduction'': This thesis tries to connect these two worlds ... this trial is one of the first; others see related work neuper@42240: neuper@42240: neuper@42240: neuper@42073: \section{Beschreibung der Meilensteine}\label{ms-desc} jan@42235: todo neuper@42073: \section{Bericht zum Projektverlauf} jan@42235: todo jan@42235: \section{Abschliesende Bemerkungen} jan@42235: todo neuper@42073: neuper@42073: \clearpage neuper@42073: jan@42253: %\bibliography{bib} neuper@42073: neuper@42073: \clearpage neuper@42073: neuper@42073: \appendix neuper@42073: %\section*{Anhang} jan@42251: \section{Demobeispiel} jan@42251: jan@42276: %\input{./Inverse_Z_Transform/document/Inverse_Z_Transform.tex} jan@42251: neuper@42073: \begin{verbatim} neuper@42073: jan@42235: bsp neuper@42073: neuper@42073: \end{verbatim} neuper@42073: neuper@42073: \section{Stundenliste} neuper@42073: neuper@42073: \subsection*{Voraussetzungen zum Arbeitsbeginn schaffen} neuper@42073: \begin{tabular}[t]{lll} neuper@42073: {\bf Datum} & {\bf Stunden} & {\bf Beschreibung} \\ neuper@42073: 10.02.2011 & 2:00 & Besprechung der Problemstellung \\ neuper@42073: \end{tabular} neuper@42073: jan@42246: \section{Calculations} jan@42251: \input{calulations} jan@42246: neuper@42073: neuper@42073: \end{document}