mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{TODO-formal-methods}

 mathematics traditionally used in these sciences. Rather, ``Formal Methods''~\cite{

 fm-03}

 ``Domain engineering''\cite{db-domain-engineering} is concerned with

 ``Domain engineering''\cite{db:dom-eng} is concerned with

 \subsection{Implementation of the TP-based Program}\label{progr}

 \subsection{Implementation of the TP-based Program}\label{progr} 

 So finally all the prerequisites are described and the program can be

 \paragraph{After introducing} neccesarry informations about the {\sisac{}}

 presented which computes a solution for the problem of the running

 System, the main part of a implementation in the TP-bases language can be shown.

 example from p.\pageref{fig-interactive}. The reader remembering the

 \par

 introduction of the programming language in \S\ref{PL-isab} might

 Solution~\ref{s:impl} shows us the implementation of the

 immediately comprehend the program:

 Inverse-Z-Transformation, a description on the code is given afterwards.

 {\small\it

 \begin{tabbing}\label{s:impl}

 \begin{solution}

 123l\=123\=123\=123\=123\=123\=123\=((x\=123\=(x \=123\=123\=\kill

 \label{s:impl}

 \begin{tabbing}

 \small\it

 123l\=123\=123\=123\=123\=123\=123\=123\=123\=(x \=123\=123\=\kill

 \>{\rm 08}\>\>\>\>\>\>\>\>  ( \> Isac, \\

 \>{\rm 08}\>\>\>\>\>\>\>\>  ( Isac, [partial\_fraction, rational, simplification], [] )\\

 \>{\rm 08}\>\>\>\>\>\>\>\>\>  [partial\_fraction, rational, simplification]\\

 %\>{\rm 10}\>\>\>\>\>\>\>\>\>  [simplification, of\_rationals, to\_partial\_fraction] ) \\

 \>{\rm 09}\>\>\>\>\>\>\>\>\>  [simplification,of\_rationals,to\_partial\_fraction] ) \\

 \>{\rm 09}\>\>\>\>\>\>\>\>  [ (rhs X\_eq)::real, z::real ]; \\

 \>{\rm 10}\>\>\>\>\>\>\>\>  [ (rhs X\_eq)::real, z::real ]; \\

 \>{\rm 10}\>\>\>  (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\

 \>{\rm 12}\>\>\>  (X'\_eq::bool) = {\tt Take} ((X'::real =$>$ bool) z = ZZ\_1 part\_frac) ; \\

 \>{\rm 11}\>\>\>  X'\_eq = (({\tt Rewrite\_Set} ruleYZ) @@   \\

 \>{\rm 12}\>\>\>  X'\_eq = {\tt Rewrite\_Set} ruleYZ X'\_eq ;   \\

 \>{\rm 12}\>\>\>\>\>  $\;\;$ ({\tt Rewrite\_Set} inverse\_z)) X'\_eq \\

 \>{\rm 15}\>\>\>  X'\_eq = {\tt Rewrite\_Set} inverse\_z X'\_eq \\

 \>{\rm 13}\>\>  {\tt IN } \\

 \>{\rm 16}\>\>  {\tt IN } \\

 \>{\rm 14}\>\>\>  X'\_eq\\

 \>{\rm 15}\>\>\>  X'\_eq

 \end{tabbing}}

 \end{tabbing}

 \end{solution}

 \newpage

 % \newpage

 -------------------------------------------------------------------

 % -------------------------------------------------------------------

 % 

 Material, falls noch Platz bleibt ...

 % Material, falls noch Platz bleibt ...

 % 

 -------------------------------------------------------------------

 % -------------------------------------------------------------------

 % 

 % 

 \subsubsection{Trials on Notation and Termination}

 % \subsubsection{Trials on Notation and Termination}

 % 

 \paragraph{Technical notations} are a big problem for our piece of software,

 % \paragraph{Technical notations} are a big problem for our piece of software,

 but the reason for that isn't a fault of the software itself, one of the

 % but the reason for that isn't a fault of the software itself, one of the

 troubles comes out of the fact that different technical subtopics use different

 % troubles comes out of the fact that different technical subtopics use different

 symbols and notations for a different purpose. The most famous example for such

 % symbols and notations for a different purpose. The most famous example for such

 a symbol is the complex number $i$ (in cassique math) or $j$ (in technical

 % a symbol is the complex number $i$ (in cassique math) or $j$ (in technical

 math). In the specific part of signal processing one of this notation issues is

 % math). In the specific part of signal processing one of this notation issues is

 the use of brackets --- we use round brackets for analoge signals and squared

 % the use of brackets --- we use round brackets for analoge signals and squared

 brackets for digital samples. Also if there is no problem for us to handle this

 % brackets for digital samples. Also if there is no problem for us to handle this

 fact, we have to tell the machine what notation leads to wich meaning and that

 % fact, we have to tell the machine what notation leads to wich meaning and that

 this purpose seperation is only valid for this special topic - signal

 % this purpose seperation is only valid for this special topic - signal

 processing.

 % processing.

 \subparagraph{In the programming language} itself it is not possible to declare

 % \subparagraph{In the programming language} itself it is not possible to declare

 fractions, exponents, absolutes and other operators or remarks in a way to make

 % fractions, exponents, absolutes and other operators or remarks in a way to make

 them pretty to read; our only posssiblilty were ASCII characters and a handfull

 % them pretty to read; our only posssiblilty were ASCII characters and a handfull

 greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.

 % greek symbols like: $\alpha, \beta, \gamma, \phi,\ldots$.

 \par

 % \par

 With the upper collected knowledge it is possible to check if we were able to

 % With the upper collected knowledge it is possible to check if we were able to

 donate all required terms and expressions.

 % donate all required terms and expressions.

 % 

 \subsubsection{Definition and Usage of Rules}

 % \subsubsection{Definition and Usage of Rules}

 % 

 \paragraph{The core} of our implemented problem is the Z-Transformation, due

 % \paragraph{The core} of our implemented problem is the Z-Transformation, due

 the fact that the transformation itself would require higher math which isn't

 % the fact that the transformation itself would require higher math which isn't

 yet avaible in our system we decided to choose the way like it is applied in

 % yet avaible in our system we decided to choose the way like it is applied in

 labratory and problem classes at our university - by applying transformation

 % labratory and problem classes at our university - by applying transformation

 rules (collected in transformation tables).

 % rules (collected in transformation tables).

 \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the

 % \paragraph{Rules,} in {\sisac{}}'s programming language can be designed by the

 use of axiomatizations like shown in Example~\ref{eg:ruledef}

 % use of axiomatizations like shown in Example~\ref{eg:ruledef}

 % 

 \begin{example}

 % \begin{example}

   \label{eg:ruledef}

 %   \label{eg:ruledef}

   \hfill\\

 %   \hfill\\

   \begin{verbatim}

 %   \begin{verbatim}

   axiomatization where

 %   axiomatization where

     rule1: ``1 = $\delta$[n]'' and

 %     rule1: ``1 = $\delta$[n]'' and

     rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and

 %     rule2: ``|| z || > 1 ==> z / (z - 1) = u [n]'' and

     rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''

 %     rule3: ``|| z || < 1 ==> z / (z - 1) = -u [-n - 1]''

   \end{verbatim}

 %   \end{verbatim}

 \end{example}

 % \end{example}

 % 

 This rules can be collected in a ruleset and applied to a given expression as

 % This rules can be collected in a ruleset and applied to a given expression as

 follows in Example~\ref{eg:ruleapp}.

 % follows in Example~\ref{eg:ruleapp}.

 % 

 \begin{example}

 % \begin{example}

   \hfill\\

 %   \hfill\\

   \label{eg:ruleapp}

 %   \label{eg:ruleapp}

   \begin{enumerate}

 %   \begin{enumerate}

   \item Store rules in ruleset:

 %   \item Store rules in ruleset:

   \begin{verbatim}

 %   \begin{verbatim}

   val inverse_Z = append_rls "inverse_Z" e_rls

 %   val inverse_Z = append_rls "inverse_Z" e_rls

     [ Thm ("rule1",num_str @{thm rule1}),

 %     [ Thm ("rule1",num_str @{thm rule1}),

       Thm ("rule2",num_str @{thm rule2}),

 %       Thm ("rule2",num_str @{thm rule2}),

       Thm ("rule3",num_str @{thm rule3})

 %       Thm ("rule3",num_str @{thm rule3})

     ];\end{verbatim}

 %     ];\end{verbatim}

   \item Define exression:

 %   \item Define exression:

   \begin{verbatim}

 %   \begin{verbatim}

   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}

 %   val sample_term = str2term "z/(z-1)+z/(z-</delta>)+1";\end{verbatim}

   \item Apply ruleset:

 %   \item Apply ruleset:

   \begin{verbatim}

 %   \begin{verbatim}

   val SOME (sample_term', asm) = 

 %   val SOME (sample_term', asm) = 

     rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}

 %     rewrite_set_ thy true inverse_Z sample_term;\end{verbatim}

   \end{enumerate}

 %   \end{enumerate}

 \end{example}

 % \end{example}

 % 

 The use of rulesets makes it much easier to develop our designated applications,

 % The use of rulesets makes it much easier to develop our designated applications,

 but the programmer has to be careful and patient. When applying rulesets

 % but the programmer has to be careful and patient. When applying rulesets

 two important issues have to be mentionend:

 % two important issues have to be mentionend:

 \subparagraph{How often} the rules have to be applied? In case of

 % \subparagraph{How often} the rules have to be applied? In case of

 transformations it is quite clear that we use them once but other fields

 % transformations it is quite clear that we use them once but other fields

 reuqire to apply rules until a special condition is reached (e.g.

 % reuqire to apply rules until a special condition is reached (e.g.

 a simplification is finished when there is nothing to be done left).

 % a simplification is finished when there is nothing to be done left).

 \subparagraph{The order} in which rules are applied often takes a big effect

 % \subparagraph{The order} in which rules are applied often takes a big effect

 and has to be evaluated for each purpose once again.

 % and has to be evaluated for each purpose once again.

 \par

 % \par

 In our special case of Signal Processing and the rules defined in

 % In our special case of Signal Processing and the rules defined in

 Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all

 % Example~\ref{eg:ruledef} we have to apply rule~1 first of all to transform all

 constants. After this step has been done it no mather which rule fit's next.

 % constants. After this step has been done it no mather which rule fit's next.

 % 

 \subsubsection{Helping Functions}

 % \subsubsection{Helping Functions}

 % 

 \paragraph{New Programms require,} often new ways to get through. This new ways

 % \paragraph{New Programms require,} often new ways to get through. This new ways

 means that we handle functions that have not been in use yet, they can be 

 % means that we handle functions that have not been in use yet, they can be 

 something special and unique for a programm or something famous but unneeded in

 % something special and unique for a programm or something famous but unneeded in

 the system yet. In our dedicated example it was for example neccessary to split

 % the system yet. In our dedicated example it was for example neccessary to split

 a fraction into numerator and denominator; the creation of such function and

 % a fraction into numerator and denominator; the creation of such function and

 even others is described in upper Sections~\ref{simp} and \ref{funs}.

 % even others is described in upper Sections~\ref{simp} and \ref{funs}.

 % 

 \subsubsection{Trials on equation solving}

 % \subsubsection{Trials on equation solving}

 %simple eq and problem with double fractions/negative exponents

 % %simple eq and problem with double fractions/negative exponents

 \paragraph{The Inverse Z-Transformation} makes it neccessary to solve

 % \paragraph{The Inverse Z-Transformation} makes it neccessary to solve

 equations degree one and two. Solving equations in the first degree is no 

 % equations degree one and two. Solving equations in the first degree is no 

 problem, wether for a student nor for our machine; but even second degree

 % problem, wether for a student nor for our machine; but even second degree

 equations can lead to big troubles. The origin of this troubles leads from

 % equations can lead to big troubles. The origin of this troubles leads from

 the build up process of our equation solving functions; they have been

 % the build up process of our equation solving functions; they have been

 implemented some time ago and of course they are not as good as we want them to

 % implemented some time ago and of course they are not as good as we want them to

 be. Wether or not following we only want to show how cruel it is to build up new

 % be. Wether or not following we only want to show how cruel it is to build up new

 work on not well fundamentials.

 % work on not well fundamentials.

 \subparagraph{A simple equation solving,} can be set up as shown in the next

 % \subparagraph{A simple equation solving,} can be set up as shown in the next

 example:

 % example:

 % 

 \begin{example}

 % \begin{example}

 \begin{verbatim}

 % \begin{verbatim}

 %   

   val fmz =

 %   val fmz =

     ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",

 %     ["equality (-1 + -2 * z + 8 * z ^^^ 2 = (0::real))",

      "solveFor z",

 %      "solveFor z",

      "solutions L"];                                    

 %      "solutions L"];                                    

 % 

   val (dI',pI',mI') =

 %   val (dI',pI',mI') =

     ("Isac", 

 %     ("Isac", 

       ["abcFormula","degree_2","polynomial","univariate","equation"],

 %       ["abcFormula","degree_2","polynomial","univariate","equation"],

       ["no_met"]);\end{verbatim}

 %       ["no_met"]);\end{verbatim}

 \end{example}

 % \end{example}

 % 

 Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give

 % Here we want to solve the equation: $-1+-2\cdot z+8\cdot z^{2}=0$. (To give

 a short overview on the commands; at first we set up the equation and tell the

 % a short overview on the commands; at first we set up the equation and tell the

 machine what's the bound variable and where to store the solution. Second step 

 % machine what's the bound variable and where to store the solution. Second step 

 is to define the equation type and determine if we want to use a special method

 % is to define the equation type and determine if we want to use a special method

 to solve this type.) Simple checks tell us that the we will get two results for

 % to solve this type.) Simple checks tell us that the we will get two results for

 this equation and this results will be real.

 % this equation and this results will be real.

 So far it is easy for us and for our machine to solve, but

 % So far it is easy for us and for our machine to solve, but

 mentioned that a unvariate equation second order can have three different types

 % mentioned that a unvariate equation second order can have three different types

 of solutions it is getting worth.

 % of solutions it is getting worth.

 \subparagraph{The solving of} all this types of solutions is not yet supported.

 % \subparagraph{The solving of} all this types of solutions is not yet supported.

 Luckily it was needed for us; but something which has been needed in this 

 % Luckily it was needed for us; but something which has been needed in this 

 context, would have been the solving of an euation looking like:

 % context, would have been the solving of an euation looking like:

 $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned

 % $-z^{-2}+-2\cdot z^{-1}+8=0$ which is basically the same equation as mentioned

 before (remember that befor it was no problem to handle for the machine) but

 % before (remember that befor it was no problem to handle for the machine) but

 now, after a simple equivalent transformation, we are not able to solve

 % now, after a simple equivalent transformation, we are not able to solve

 it anymore.

 % it anymore.

 \subparagraph{Error messages} we get when we try to solve something like upside

 % \subparagraph{Error messages} we get when we try to solve something like upside

 were very confusing and also leads us to no special hint about a problem.

 % were very confusing and also leads us to no special hint about a problem.

 \par The fault behind is, that we have no well error handling on one side and

 % \par The fault behind is, that we have no well error handling on one side and

 no sufficient formed equation solving on the other side. This two facts are

 % no sufficient formed equation solving on the other side. This two facts are

 making the implemention of new material very difficult.

 % making the implemention of new material very difficult.

 % 

 \subsection{Formalization of missing knowledge in Isabelle}

 % \subsection{Formalization of missing knowledge in Isabelle}

 % 

 \paragraph{A problem} behind is the mechanization of mathematic

 % \paragraph{A problem} behind is the mechanization of mathematic

 theories in TP-bases languages. There is still a huge gap between

 % theories in TP-bases languages. There is still a huge gap between

 these algorithms and this what we want as a solution - in Example

 % these algorithms and this what we want as a solution - in Example

 Signal Processing. 

 % Signal Processing. 

 % 

 \vbox{

 % \vbox{

   \begin{example}

 %   \begin{example}

     \label{eg:gap}

 %     \label{eg:gap}

     \[

 %     \[

       X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY

 %       X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY

     \]

 %     \]

     {\small\textit{

 %     {\small\textit{

       \noindent A very simple example on this what we call gap is the

 %       \noindent A very simple example on this what we call gap is the

 simplification above. It is needles to say that it is correct and also

 % simplification above. It is needles to say that it is correct and also

 Isabelle for fills it correct - \emph{always}. But sometimes we don't

 % Isabelle for fills it correct - \emph{always}. But sometimes we don't

 want expand such terms, sometimes we want another structure of

 % want expand such terms, sometimes we want another structure of

 them. Think of a problem were we now would need only the coefficients

 % them. Think of a problem were we now would need only the coefficients

 of $X$ and $Y$. This is what we call the gap between mechanical

 % of $X$ and $Y$. This is what we call the gap between mechanical

 simplification and the solution.

 % simplification and the solution.

     }}

 %     }}

   \end{example}

 %   \end{example}

 }

 % }

 % 

 \paragraph{We are not able to fill this gap,} until we have to live

 % \paragraph{We are not able to fill this gap,} until we have to live

 with it but first have a look on the meaning of this statement:

 % with it but first have a look on the meaning of this statement:

 Mechanized math starts from mathematical models and \emph{hopefully}

 % Mechanized math starts from mathematical models and \emph{hopefully}

 proceeds to match physics. Academic engineering starts from physics

 % proceeds to match physics. Academic engineering starts from physics

 (experimentation, measurement) and then proceeds to mathematical

 % (experimentation, measurement) and then proceeds to mathematical

 modeling and formalization. The process from a physical observance to

 % modeling and formalization. The process from a physical observance to

 a mathematical theory is unavoidable bound of setting up a big

 % a mathematical theory is unavoidable bound of setting up a big

 collection of standards, rules, definition but also exceptions. These

 % collection of standards, rules, definition but also exceptions. These

 are the things making mechanization that difficult.

 % are the things making mechanization that difficult.

 % 

 \vbox{

 % \vbox{

   \begin{example}

 %   \begin{example}

     \label{eg:units}

 %     \label{eg:units}

     \[

 %     \[

       m,\ kg,\ s,\ldots

 %       m,\ kg,\ s,\ldots

     \]

 %     \]

     {\small\textit{

 %     {\small\textit{

       \noindent Think about some units like that one's above. Behind

 %       \noindent Think about some units like that one's above. Behind

 each unit there is a discerning and very accurate definition: One

 % each unit there is a discerning and very accurate definition: One

 Meter is the distance the light travels, in a vacuum, through the time

 % Meter is the distance the light travels, in a vacuum, through the time

 of 1 / 299.792.458 second; one kilogram is the weight of a

 % of 1 / 299.792.458 second; one kilogram is the weight of a

 platinum-iridium cylinder in paris; and so on. But are these

 % platinum-iridium cylinder in paris; and so on. But are these

 definitions usable in a computer mechanized world?!

 % definitions usable in a computer mechanized world?!

     }}

 %     }}

   \end{example}

 %   \end{example}

 }

 % }

 % 

 \paragraph{A computer} or a TP-System builds on programs with

 % \paragraph{A computer} or a TP-System builds on programs with

 predefined logical rules and does not know any mathematical trick

 % predefined logical rules and does not know any mathematical trick

 (follow up example \ref{eg:trick}) or recipe to walk around difficult

 % (follow up example \ref{eg:trick}) or recipe to walk around difficult

 expressions. 

 % expressions. 

 % 

 \vbox{

 % \vbox{

   \begin{example}

 %   \begin{example}

     \label{eg:trick}

 %     \label{eg:trick}

   \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]

 %   \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \]

   \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=

 %   \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)=

      \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]

 %      \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \]

   \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]

 %   \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \]

     {\small\textit{

 %     {\small\textit{

       \noindent Sometimes it is also useful to be able to apply some

 %       \noindent Sometimes it is also useful to be able to apply some

 \emph{tricks} to get a beautiful and particularly meaningful result,

 % \emph{tricks} to get a beautiful and particularly meaningful result,

 which we are able to interpret. But as seen in this example it can be

 % which we are able to interpret. But as seen in this example it can be

 hard to find out what operations have to be done to transform a result

 % hard to find out what operations have to be done to transform a result

 into a meaningful one.

 % into a meaningful one.

     }}

 %     }}

   \end{example}

 %   \end{example}

 }

 % }

 % 

 \paragraph{The only possibility,} for such a system, is to work

 % \paragraph{The only possibility,} for such a system, is to work

 through its known definitions and stops if none of these

 % through its known definitions and stops if none of these

 fits. Specified on Signal Processing or any other application it is

 % fits. Specified on Signal Processing or any other application it is

 often possible to walk through by doing simple creases. This creases

 % often possible to walk through by doing simple creases. This creases

 are in general based on simple math operational but the challenge is

 % are in general based on simple math operational but the challenge is

 to teach the machine \emph{all}\footnote{Its pride to call it

 % to teach the machine \emph{all}\footnote{Its pride to call it

 \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to

 % \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to

 reach a high level of \emph{all} but it in real it will still be a

 % reach a high level of \emph{all} but it in real it will still be a

 survey of knowledge which links to other knowledge and {{\sisac}{}} a

 % survey of knowledge which links to other knowledge and {{\sisac}{}} a

 trainer and helper but no human compensating calculator. 

 % trainer and helper but no human compensating calculator. 

 \par

 % \par

 {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal

 % {{{\sisac}{}}} itself aims to adds \emph{Algorithmic Knowledge} (formal

 specifications of problems out of topics from Signal Processing, etc.)

 % specifications of problems out of topics from Signal Processing, etc.)

 and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of

 % and \emph{Application-oriented Knowledge} to the \emph{deductive} axis of

 physical knowledge. The result is a three-dimensional universe of

 % physical knowledge. The result is a three-dimensional universe of

 mathematics seen in Figure~\ref{fig:mathuni}.

 % mathematics seen in Figure~\ref{fig:mathuni}.

 % 

 \begin{figure}

 % \begin{figure}

   \begin{center}

 %   \begin{center}

     \includegraphics{fig/universe}

 %     \includegraphics{fig/universe}

     \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is

 %     \caption{Didactic ``Math-Universe'': Algorithmic Knowledge (Programs) is

              combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result

 %              combined with Application-oriented Knowledge (Specifications) and Deductive Knowledge (Axioms, Definitions, Theorems). The Result

              leads to a three dimensional math universe.\label{fig:mathuni}}

 %              leads to a three dimensional math universe.\label{fig:mathuni}}

   \end{center}

 %   \end{center}

 \end{figure}

 % \end{figure}

 % 

 %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;

 % %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen;

 %WN bitte folgende Bezeichnungen nehmen:

 % %WN bitte folgende Bezeichnungen nehmen:

 %WN 

 % %WN 

 %WN axis 1: Algorithmic Knowledge (Programs)

 % %WN axis 1: Algorithmic Knowledge (Programs)

 %WN axis 2: Application-oriented Knowledge (Specifications)

 % %WN axis 2: Application-oriented Knowledge (Specifications)

 %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)

 % %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems)

 %WN 

 % %WN 

 %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf

 % %WN und bitte die R"ander von der Grafik wegschneiden (was ich f"ur *.pdf

 %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz

 % %WN nicht hinkriege --- weshalb ich auch die eJMT-Forderung nicht ganz

 %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)

 % %WN verstehe, separierte PDFs zu schicken; ich w"urde *.png schicken)

 % 

 %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's

 % %JR Ränder und beschriftung geändert. Keine Ahnung warum eJMT sich pdf's

 %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's

 % %JR wünschen, würde ebenfalls png oder ähnliches verwenden, aber wenn pdf's

 %JR gefordert werden WN2...

 % %JR gefordert werden WN2...

 %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann

 % %WN2 meiner Meinung nach hat sich eJMT unklar ausgedr"uckt (z.B. kann

 %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse

 % %WN2 man meines Wissens pdf-figures nicht auf eine bestimmte Gr"osse

 %WN2 zusammenschneiden um die R"ander weg zu bekommen)

 % %WN2 zusammenschneiden um die R"ander weg zu bekommen)

 %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und

 % %WN2 Mein Vorschlag ist, in umserem tex-file bei *.png zu bleiben und

 %WN2 png + pdf figures mitzuschicken.

 % %WN2 png + pdf figures mitzuschicken.

 % 

 \subsection{Notes on Problems with Traditional Notation}

 % \subsection{Notes on Problems with Traditional Notation}

 % 

 \paragraph{During research} on these topic severely problems on

 % \paragraph{During research} on these topic severely problems on

 traditional notations have been discovered. Some of them have been

 % traditional notations have been discovered. Some of them have been

 known in computer science for many years now and are still unsolved,

 % known in computer science for many years now and are still unsolved,

 one of them aggregates with the so called \emph{Lambda Calculus},

 % one of them aggregates with the so called \emph{Lambda Calculus},

 Example~\ref{eg:lamda} provides a look on the problem that embarrassed

 % Example~\ref{eg:lamda} provides a look on the problem that embarrassed

 us.

 % us.

 % 

 \vbox{

 % \vbox{

   \begin{example}

 %   \begin{example}

     \label{eg:lamda}

 %     \label{eg:lamda}

 % 

   \[ f(x)=\ldots\;  \quad R \rightarrow \quad R \]

 %   \[ f(x)=\ldots\;  \quad R \rightarrow \quad R \]

 % 

 % 

   \[ f(p)=\ldots\;  p \in \quad R \]

 %   \[ f(p)=\ldots\;  p \in \quad R \]

 % 

     {\small\textit{

 %     {\small\textit{

       \noindent Above we see two equations. The first equation aims to

 %       \noindent Above we see two equations. The first equation aims to

 be a mapping of an function from the reel range to the reel one, but

 % be a mapping of an function from the reel range to the reel one, but

 when we change only one letter we get the second equation which

 % when we change only one letter we get the second equation which

 usually aims to insert a reel point $p$ into the reel function. In

 % usually aims to insert a reel point $p$ into the reel function. In

 computer science now we have the problem to tell the machine (TP) the

 % computer science now we have the problem to tell the machine (TP) the

 difference between this two notations. This Problem is called

 % difference between this two notations. This Problem is called

 \emph{Lambda Calculus}.

 % \emph{Lambda Calculus}.

     }}

 %     }}

   \end{example}

 %   \end{example}

 }

 % }

 % 

 \paragraph{An other problem} is that terms are not full simplified in

 % \paragraph{An other problem} is that terms are not full simplified in

 traditional notations, in {{\sisac}} we have to simplify them complete

 % traditional notations, in {{\sisac}} we have to simplify them complete

 to check weather results are compatible or not. in e.g. the solutions

 % to check weather results are compatible or not. in e.g. the solutions

 of an second order linear equation is an rational in {{\sisac}} but in

 % of an second order linear equation is an rational in {{\sisac}} but in

 tradition we keep fractions as long as possible and as long as they

 % tradition we keep fractions as long as possible and as long as they

 aim to be \textit{beautiful} (1/8, 5/16,...).

 % aim to be \textit{beautiful} (1/8, 5/16,...).

 \subparagraph{The math} which should be mechanized in Computer Theorem

 % \subparagraph{The math} which should be mechanized in Computer Theorem

 Provers (\emph{TP}) has (almost) a problem with traditional notations

 % Provers (\emph{TP}) has (almost) a problem with traditional notations

 (predicate calculus) for axioms, definitions, lemmas, theorems as a

 % (predicate calculus) for axioms, definitions, lemmas, theorems as a

 computer program or script is not able to interpret every Greek or

 % computer program or script is not able to interpret every Greek or

 Latin letter and every Greek, Latin or whatever calculations

 % Latin letter and every Greek, Latin or whatever calculations

 symbol. Also if we would be able to handle these symbols we still have

 % symbol. Also if we would be able to handle these symbols we still have

 a problem to interpret them at all. (Follow up \hbox{Example

 % a problem to interpret them at all. (Follow up \hbox{Example

 \ref{eg:symbint1}})

 % \ref{eg:symbint1}})

 % 

 \vbox{

 % \vbox{

   \begin{example}

 %   \begin{example}

     \label{eg:symbint1}

 %     \label{eg:symbint1}

     \[

 %     \[

       u\left[n\right] \ \ldots \ unitstep

 %       u\left[n\right] \ \ldots \ unitstep

     \]

 %     \]

     {\small\textit{

 %     {\small\textit{

       \noindent The unitstep is something we need to solve Signal

 %       \noindent The unitstep is something we need to solve Signal

 Processing problem classes. But in {{{\sisac}{}}} the rectangular

 % Processing problem classes. But in {{{\sisac}{}}} the rectangular

 brackets have a different meaning. So we abuse them for our

 % brackets have a different meaning. So we abuse them for our

 requirements. We get something which is not defined, but usable. The

 % requirements. We get something which is not defined, but usable. The

 Result is syntax only without semantic.

 % Result is syntax only without semantic.

     }}

 %     }}

   \end{example}

 %   \end{example}

 }

 % }

 % 

 In different problems, symbols and letters have different meanings and

 % In different problems, symbols and letters have different meanings and

 ask for different ways to get through. (Follow up \hbox{Example

 % ask for different ways to get through. (Follow up \hbox{Example

 \ref{eg:symbint2}}) 

 % \ref{eg:symbint2}}) 

 % 

 \vbox{

 % \vbox{

   \begin{example}

 %   \begin{example}

     \label{eg:symbint2}

 %     \label{eg:symbint2}

     \[

 %     \[

       \widehat{\ }\ \widehat{\ }\ \widehat{\ } \  \ldots \  exponent

 %       \widehat{\ }\ \widehat{\ }\ \widehat{\ } \  \ldots \  exponent

     \]

 %     \]

     {\small\textit{

 %     {\small\textit{

     \noindent For using exponents the three \texttt{widehat} symbols

 %     \noindent For using exponents the three \texttt{widehat} symbols

 are required. The reason for that is due the development of

 % are required. The reason for that is due the development of

 {{{\sisac}{}}} the single \texttt{widehat} and also the double were

 % {{{\sisac}{}}} the single \texttt{widehat} and also the double were

 already in use for different operations.

 % already in use for different operations.

     }}

 %     }}

   \end{example}

 %   \end{example}

 }

 % }

 % 

 \paragraph{Also the output} can be a problem. We are familiar with a

 % \paragraph{Also the output} can be a problem. We are familiar with a

 specified notations and style taught in university but a computer

 % specified notations and style taught in university but a computer

 program has no knowledge of the form proved by a professor and the

 % program has no knowledge of the form proved by a professor and the

 machines themselves also have not yet the possibilities to print every

 % machines themselves also have not yet the possibilities to print every

 symbol (correct) Recent developments provide proofs in a human

 % symbol (correct) Recent developments provide proofs in a human

 readable format but according to the fact that there is no money for

 % readable format but according to the fact that there is no money for

 good working formal editors yet, the style is one thing we have to

 % good working formal editors yet, the style is one thing we have to

 live with.

 % live with.

 % 

 \section{Problems rising out of the Development Environment}

 % \section{Problems rising out of the Development Environment}

 % 

 fehlermeldungen! TODO

 % fehlermeldungen! TODO