165 % Please use the following to indicate sections, subsections, |
165 % Please use the following to indicate sections, subsections, |
166 % etc. Please also use \subsubsection{...}, \paragraph{...} |
166 % etc. Please also use \subsubsection{...}, \paragraph{...} |
167 % and \subparagraph{...} as necessary. |
167 % and \subparagraph{...} as necessary. |
168 % |
168 % |
169 |
169 |
170 \section{Introduction} |
170 \section{Introduction}\label{intro} |
171 |
171 |
172 \paragraph{Didactics of mathematics} faces a specific issue, a gap between (1) introduction of math concepts and skills and (2) application of these concepts and skills, which usually are separated into different units in curricula (for good reasons). For instance, (1) teaching partial fraction decomposition is separated from (2) application for inverse Z-transform in signal processing. |
172 % \paragraph{Didactics of mathematics} |
173 \par |
173 %WN: wenn man in einem high-quality paper von 'didactics' spricht, |
174 This gap is an obstacle for applying math as an fundamental thinking technology in engineering: In (1) motivation is lacking because the question ``What is this stuff good for?'' cannot be treated sufficiently, and in (2) the ``stuff'' is not available to students in higher semesters as widespread experience shows. |
174 %WN muss man am state-of-the-art ankn"upfen -- siehe |
175 |
175 %WN W.Neuper, On the Emergence of TP-based Educational Math Assistants |
176 \paragraph{Motivation} taken by this didactic issue on the one hand, and ongoing research and development on a novel kind of educational mathematics assistant at Graz University of Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to scope with this issue on the other hand, several institutes are planning to join their expertise: the Institute for Information Systems and Computer Media (IICM), the Institute for Software Technology (IST), the Institutes for Mathematics, the Institute for Signal Processing and Speech Communication (SPSC), the Institute for Structural Analysis and the Institute of Electrical Measurement and Measurement Signal Processing. |
176 % faces a specific issue, a gap |
177 \par This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in \emph{STEOP}, the introductory orientation phase in Austria. \emph{STEOP} is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. |
177 % between (1) introduction of math concepts and skills and (2) |
178 |
178 % application of these concepts and skills, which usually are separated |
179 The paper will use the problem in Fig.\ref{fig-gclc} as a |
179 % into different units in curricula (for good reasons). For instance, |
|
180 % (1) teaching partial fraction decomposition is separated from (2) |
|
181 % application for inverse Z-transform in signal processing. |
|
182 % |
|
183 % \par This gap is an obstacle for applying math as an fundamental |
|
184 % thinking technology in engineering: In (1) motivation is lacking |
|
185 % because the question ``What is this stuff good for?'' cannot be |
|
186 % treated sufficiently, and in (2) the ``stuff'' is not available to |
|
187 % students in higher semesters as widespread experience shows. |
|
188 % |
|
189 % \paragraph{Motivation} taken by this didactic issue on the one hand, |
|
190 % and ongoing research and development on a novel kind of educational |
|
191 % mathematics assistant at Graz University of |
|
192 % Technology~\footnote{http://www.ist.tugraz.at/isac/} promising to |
|
193 % scope with this issue on the other hand, several institutes are |
|
194 % planning to join their expertise: the Institute for Information |
|
195 % Systems and Computer Media (IICM), the Institute for Software |
|
196 % Technology (IST), the Institutes for Mathematics, the Institute for |
|
197 % Signal Processing and Speech Communication (SPSC), the Institute for |
|
198 % Structural Analysis and the Institute of Electrical Measurement and |
|
199 % Measurement Signal Processing. |
|
200 %WN diese Information ist f"ur das Paper zu spezielle, zu aktuell |
|
201 %WN und damit zu verg"anglich. |
|
202 % \par This thesis is the first attempt to tackle the above mentioned |
|
203 % issue, it focuses on Telematics, because these specific studies focus |
|
204 % on mathematics in \emph{STEOP}, the introductory orientation phase in |
|
205 % Austria. \emph{STEOP} is considered an opportunity to investigate the |
|
206 % impact of {\sisac}'s prototype on the issue and others. |
|
207 % |
|
208 |
|
209 Traditional course material in engineering disciplines lacks an |
|
210 important component, interactive support for step-wise problem |
|
211 solving. Theorem-Proving (TP) technology can provide such support by |
|
212 specific services. An important part of such services is called |
|
213 ``next-step-guidance'', generated by a specific kind of ``TP-based |
|
214 programming language''. In the |
|
215 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such |
|
216 a language is prototyped in line with~\cite{plmms10} and built upon |
|
217 the theorem prover |
|
218 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/}. |
|
219 The TP services are coordinated by a specific interpreter for the |
|
220 programming language, called |
|
221 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the |
|
222 interpreter will be briefly re-introduced in order to make the paper |
|
223 self-contained. |
|
224 |
|
225 \medskip The main part of the paper is an account of first experiences |
|
226 with programming in this TP-based language. The experience was gained |
|
227 in a case study by the author. The author was considered an ideal |
|
228 candidate for this study for the following reasons: as a student in |
|
229 Telematics (computer science with focus on Signal Processing) he had |
|
230 general knowledge in programming as well as specific domain knowledge |
|
231 in Signal Processing; and he was not involved in the development of |
|
232 {\sisac}'s programming language and interpeter, thus a novice to the |
|
233 language. |
|
234 |
|
235 The goal of the case study was (1) some TP-based programs for |
|
236 interactive course material for a specific ``Adavanced Signal |
|
237 Processing Lab'' in a higher semester, (2) respective program |
|
238 development with as little advice from the {\sisac}-team and (3) records |
|
239 and comments for the main steps of development in an Isabelle theory; |
|
240 this theory should provide guidelines for future programmers. An |
|
241 excerpt from this theory is the main part of this paper. |
|
242 |
|
243 \medskip The paper will use the problem in Fig.\ref{fig-interactive} as a |
180 running example: |
244 running example: |
181 \begin{figure} [htb] |
245 \begin{figure} [htb] |
182 \begin{center} |
246 \begin{center} |
183 %\includegraphics[width=120mm]{fig/newgen/isac-Ztrans-math.png} |
247 \includegraphics[width=120mm]{fig/isac-Ztrans-math.png} |
184 \caption{Step-wise problem solving guided by the TP-based program} |
248 \caption{Step-wise problem solving guided by the TP-based program} |
185 \label{fig-interactive} |
249 \label{fig-interactive} |
186 \end{center} |
250 \end{center} |
187 \label{fig-gclc} |
|
188 \end{figure} |
251 \end{figure} |
|
252 The problem is from the domain of Signal Processing and requests to |
|
253 determine the inverse Z-transform for a given term. Fig.\ref{fig-interactive} |
|
254 also shows the beginning of the interactive construction of a solution |
|
255 for the problem. This construction is done in the right window named |
|
256 ``Worksheet''. |
|
257 |
|
258 User-interaction on the Worksheet is {\em checked} and {\em guided} by |
|
259 TP services: |
|
260 \begin{enumerate} |
|
261 \item Formulas input by the user are {\em checked} by TP: such a |
|
262 formula establishes a proof situation --- the prover has to derive the |
|
263 formula from the logical context. The context is built up from the |
|
264 formal specification of the problem (here hidden from the user) by the |
|
265 Lucas-Interpreter. |
|
266 \item If the user gets stuck, the program developed below in this |
|
267 paper ``knows the next step'' from behind the scenes. How the latter |
|
268 TP-service is exploited by dialogue authoring is out of scope of this |
|
269 paper and can be studied in~\cite{gdaroczy-EP-13}. |
|
270 \end{enumerate} It should be noted that the programmer using the |
|
271 TP-based language is not concerned with interaction at all; we will |
|
272 see that the program contains neither input-statements nor |
|
273 output-statements. Rather, interaction is handled by services |
|
274 generated automatically. |
|
275 |
|
276 \medskip So there is a clear separation of concerns: Dialogues are |
|
277 adapted by dialogue authors (in Java-based tools), using automatically |
|
278 generated TP services, while the TP-based program is written by |
|
279 mathematics experts (in Isabelle/ML). The latter is concern of this |
|
280 paper. |
|
281 |
|
282 \medskip The paper is structed as follows: The introduction |
|
283 \S\ref{intro} is followed by a brief re-introduction of the TP-based |
|
284 programming language in \S\ref{PL}, which extends the executable |
|
285 fragment of Isabelle's language (\S\ref{PL-isab}) by tactics which |
|
286 play a specific role in Lucas-Interpretation and in providing the TP |
|
287 services (\S\ref{PL-tacs}). The main part in \S\ref{trial} describes |
|
288 the main steps in developing the program for the running example: |
|
289 prepare domain knowledge, implement the formal specification of the |
|
290 problem, prepare the environment for the program, implement the |
|
291 program. The workflow of programming, debugging and testing is |
|
292 described in \S\ref{workflow}. The conclusion \S\ref{conclusion} will |
|
293 give directions identified for future development. |
|
294 |
189 |
295 |
190 \section{\isac's Prototype for a Programming Language}\label{PL} |
296 \section{\isac's Prototype for a Programming Language}\label{PL} |
191 The prototype's language extends the executable fragment in the |
297 The prototype's language extends the executable fragment in the |
192 language of the theorem prover |
298 language of the theorem prover |
193 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/} |
299 Isabelle~\cite{Nipkow-Paulson-Wenzel:2002}\footnote{http://isabelle.in.tum.de/} |
339 |
447 |
340 no input / output --- Lucas-Interpretation |
448 no input / output --- Lucas-Interpretation |
341 |
449 |
342 .\\.\\.\\TODO\\.\\.\\ |
450 .\\.\\.\\TODO\\.\\.\\ |
343 |
451 |
344 \section{Development of a Program on Trial}\label{trial} |
452 \section{Development of a Program on Trial}\label{trial} |
345 |
453 As mentioned above, {\sisac} is an experimental system for a proof of |
346 \subsection{Mechanization of Math in Isabelle/ISAC\label{isabisac}} |
454 concept for Lucas-Interpretation~\cite{wn:lucas-interp-12}. The |
347 |
455 latter interprets a specific kind of TP-based programming language, |
348 \paragraph{As mentioned in the introduction,} a prototype of an educational math assistant called {\sisac}\footnote{{\sisac}=\textbf{Isa}belle for \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges the gap between (1) introducation and (2) application of mathematics: {\sisac} is based on Computer Theorem Proving (TP), a technology which requires each fact and each action justified by formal logic, so {{\sisac{}}} makes justifications transparent to students in interactive step-wise problem solving. By that way {\sisac} already can serve both: |
456 which is as experimental as the whole prototype --- so programming in |
349 \begin{enumerate} |
457 this language can be only ``on trial'', presently. However, as a |
350 \item Introduction of math stuff (in e.g. partial fraction decomposition) by stepwise explaining and exercising respective symbolic calculations with ``next step guidance (NSG)'' and rigorously checking steps freely input by students --- this also in context with advanced applications (where the stuff to be taught in higher semesters can be skimmed through by NSG), and |
458 prototype, the language addresses essentials described below. |
351 \item Application of math stuff in advanced engineering courses (e.g. problems to be solved by inverse Z-transform in a Signal Processing Lab) and now without much ado about basic math techniques (like partial fraction decomposition): ``next step guidance'' supports students in independently (re-)adopting such techniques. |
459 |
352 \end{enumerate} |
460 \subsection{Mechanization of Math --- Domain Engineering}\label{isabisac} |
353 Before the question is answers, how {\sisac} accomplishes this task from a technical point of view, some remarks on the state-of-the-art is given, therefor follow up Section~\ref{emas}. |
461 |
354 |
462 %WN was Fachleute unter obigem Titel interessiert findet |
355 \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} |
463 %WN unterhalb des auskommentierten Textes. |
356 |
464 |
357 \paragraph{Educational software in mathematics} is, if at all, based on Computer Algebra Systems (CAS, for instance), Dynamic Geometry Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org} \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These base technologies are used to program math lessons and sometimes even exercises. The latter are cumbersome: the steps towards a solution of such an interactive exercise need to be provided with feedback, where at each step a wide variety of possible input has to be foreseen by the programmer - so such interactive exercises either require high development efforts or the exercises constrain possible inputs. |
465 %WN der Text unten spricht Benutzer-Aspekte anund ist nicht speziell |
358 |
466 %WN auf Computer-Mathematiker fokussiert. |
359 \subparagraph{A new generation} of educational math assistants (EMAs) is emerging presently, which is based on Theorem Proving (TP). TP, for instance Isabelle and Coq, is a technology which requires each fact and each action justified by formal logic. Pushed by demands for \textit{proven} correctness of safety-critical software TP advances into software engineering; from these advancements computer mathematics benefits in general, and math education in particular. Two features of TP are immediately beneficial for learning: |
467 % \paragraph{As mentioned in the introduction,} a prototype of an |
360 |
468 % educational math assistant called |
361 \paragraph{TP have knowledge in human readable format,} that is in standard predicate calculus. TP following the LCF-tradition have that knowledge down to the basic definitions of set, equality, etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; following the typical deductive development of math, natural numbers are defined and their properties proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, etc. Present knowledge mechanized in TP exceeds high-school mathematics by far, however by knowledge required in software technology, and not in other engineering sciences. |
469 % {{\sisac}}\footnote{{{\sisac}}=\textbf{Isa}belle for |
362 |
470 % \textbf{C}alculations, see http://www.ist.tugraz.at/isac/.} bridges |
363 \paragraph{TP can model the whole problem solving process} in mathematical problem solving {\em within} a coherent logical framework. This is already being done by three projects, by Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor. |
471 % the gap between (1) introducation and (2) application of mathematics: |
364 \par |
472 % {{\sisac}} is based on Computer Theorem Proving (TP), a technology which |
365 Having the whole problem solving process within a logical coherent system, such a design guarantees correctness of intermediate steps and of the result (which seems essential for math software); and the second advantage is that TP provides a wealth of theories which can be exploited for mechanizing other features essential for educational software. |
473 % requires each fact and each action justified by formal logic, so |
366 |
474 % {{{\sisac}{}}} makes justifications transparent to students in |
367 \subsubsection{Generation of User Guidance in EMAs}\label{user-guid} |
475 % interactive step-wise problem solving. By that way {{\sisac}} already |
368 |
476 % can serve both: |
369 One essential feature for educational software is feedback to user input and assistance in coming to a solution. |
477 % \begin{enumerate} |
370 |
478 % \item Introduction of math stuff (in e.g. partial fraction |
371 \paragraph{Checking user input} by ATP during stepwise problem solving is being accomplished by the three projects mentioned above exclusively. They model the whole problem solving process as mentioned above, so all what happens between formalized assumptions (or formal specification) and goal (or fulfilled postcondition) can be mechanized. Such mechanization promises to greatly extend the scope of educational software in stepwise problem solving. |
479 % decomposition) by stepwise explaining and exercising respective |
372 |
480 % symbolic calculations with ``next step guidance (NSG)'' and rigorously |
373 \paragraph{NSG (Next step guidance)} comprises the system's ability to propose a next step; this is a challenge for TP: either a radical restriction of the search space by restriction to very specific problem classes is required, or much care and effort is required in designing possible variants in the process of problem solving \cite{proof-strategies-11}. |
481 % checking steps freely input by students --- this also in context with |
374 \par |
482 % advanced applications (where the stuff to be taught in higher |
375 Another approach is restricted to problem solving in engineering domains, where a problem is specified by input, precondition, output and postcondition, and where the postcondition is proven by ATP behind the scenes: Here the possible variants in the process of problem solving are provided with feedback {\em automatically}, if the problem is described in a TP-based programing language: |
483 % semesters can be skimmed through by NSG), and |
376 \cite{plmms10} the programmer only describes the math algorithm without caring about interaction (the respective program is functional and even has no input or output statements!); interaction is generated as a side-effect by the interpreter --- an efficient separation of concern between math programmers and dialog designers promising application all over engineering disciplines. |
484 % \item Application of math stuff in advanced engineering courses |
377 |
485 % (e.g. problems to be solved by inverse Z-transform in a Signal |
378 |
486 % Processing Lab) and now without much ado about basic math techniques |
379 \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}} |
487 % (like partial fraction decomposition): ``next step guidance'' supports |
380 Authoring new mathematics knowledge in {\sisac} can be compared with ``application programing'' of engineering problems; most of such programing uses CAS-based programing languages (CAS = Computer Algebra Systems; e.g. Mathematica's or Maple's programing language). |
488 % students in independently (re-)adopting such techniques. |
381 |
489 % \end{enumerate} |
382 \paragraph{A novel type of TP-based language} is used by {\sisac{}} \cite{plmms10} for describing how to construct a solution to an engineering problem and for calling equation solvers, integration, etc~\footnote{Implementation of CAS-like functionality in TP is not primarily concerned with efficiency, but with a didactic question: What to decide for: for high-brow algorithms at the state-of-the-art or for elementary algorithms comprehensible for students?} within TP; TP can ensure ``systems that never make a mistake'' \cite{casproto} - are impossible for CAS which have no logics underlying. |
490 % Before the question is answers, how {{\sisac}} |
383 |
491 % accomplishes this task from a technical point of view, some remarks on |
384 \subparagraph{Authoring is perfect} by writing such TP based programs; the application programmer is not concerned with interaction or with user guidance: this is concern of a novel kind of program interpreter called Lucas-Interpreter. This interpreter hands over control to a dialog component at each step of calculation (like a debugger at breakpoints) and calls automated TP to check user input following personalized strategies according to a feedback module. |
492 % the state-of-the-art is given, therefor follow up Section~\ref{emas}. |
385 \par |
493 % |
386 However ``application programing with TP'' is not done with writing a program: according to the principles of TP, each step must be justified. Such justifications are given by theorems. So all steps must be related to some theorem, if there is no such theorem it must be added to the existing knowledge, which is organized in so-called \textbf{theories} in Isabelle. A theorem must be proven; fortunately Isabelle comprises a mechanism (called ``axiomatization''), which allows to omit proofs. Such a theorem is shown in Example~\ref{eg:neuper1}. |
494 % \subsection{Educational Mathematics Assistants (EMAs)}\label{emas} |
387 |
495 % |
388 \vbox{ |
496 % \paragraph{Educational software in mathematics} is, if at all, based |
389 \begin{example} |
497 % on Computer Algebra Systems (CAS, for instance), Dynamic Geometry |
|
498 % Systems (DGS, for instance \footnote{GeoGebra http://www.geogebra.org} |
|
499 % \footnote{Cinderella http://www.cinderella.de/}\footnote{GCLC |
|
500 % http://poincare.matf.bg.ac.rs/~janicic/gclc/}) or spread-sheets. These |
|
501 % base technologies are used to program math lessons and sometimes even |
|
502 % exercises. The latter are cumbersome: the steps towards a solution of |
|
503 % such an interactive exercise need to be provided with feedback, where |
|
504 % at each step a wide variety of possible input has to be foreseen by |
|
505 % the programmer - so such interactive exercises either require high |
|
506 % development efforts or the exercises constrain possible inputs. |
|
507 % |
|
508 % \subparagraph{A new generation} of educational math assistants (EMAs) |
|
509 % is emerging presently, which is based on Theorem Proving (TP). TP, for |
|
510 % instance Isabelle and Coq, is a technology which requires each fact |
|
511 % and each action justified by formal logic. Pushed by demands for |
|
512 % \textit{proven} correctness of safety-critical software TP advances |
|
513 % into software engineering; from these advancements computer |
|
514 % mathematics benefits in general, and math education in particular. Two |
|
515 % features of TP are immediately beneficial for learning: |
|
516 % |
|
517 % \paragraph{TP have knowledge in human readable format,} that is in |
|
518 % standard predicate calculus. TP following the LCF-tradition have that |
|
519 % knowledge down to the basic definitions of set, equality, |
|
520 % etc~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL.html}; |
|
521 % following the typical deductive development of math, natural numbers |
|
522 % are defined and their properties |
|
523 % proven~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Number\_Theory/Primes.html}, |
|
524 % etc. Present knowledge mechanized in TP exceeds high-school |
|
525 % mathematics by far, however by knowledge required in software |
|
526 % technology, and not in other engineering sciences. |
|
527 % |
|
528 % \paragraph{TP can model the whole problem solving process} in |
|
529 % mathematical problem solving {\em within} a coherent logical |
|
530 % framework. This is already being done by three projects, by |
|
531 % Ralph-Johan Back, by ActiveMath and by Carnegie Mellon Tutor. |
|
532 % \par |
|
533 % Having the whole problem solving process within a logical coherent |
|
534 % system, such a design guarantees correctness of intermediate steps and |
|
535 % of the result (which seems essential for math software); and the |
|
536 % second advantage is that TP provides a wealth of theories which can be |
|
537 % exploited for mechanizing other features essential for educational |
|
538 % software. |
|
539 % |
|
540 % \subsubsection{Generation of User Guidance in EMAs}\label{user-guid} |
|
541 % |
|
542 % One essential feature for educational software is feedback to user |
|
543 % input and assistance in coming to a solution. |
|
544 % |
|
545 % \paragraph{Checking user input} by ATP during stepwise problem solving |
|
546 % is being accomplished by the three projects mentioned above |
|
547 % exclusively. They model the whole problem solving process as mentioned |
|
548 % above, so all what happens between formalized assumptions (or formal |
|
549 % specification) and goal (or fulfilled postcondition) can be |
|
550 % mechanized. Such mechanization promises to greatly extend the scope of |
|
551 % educational software in stepwise problem solving. |
|
552 % |
|
553 % \paragraph{NSG (Next step guidance)} comprises the system's ability to |
|
554 % propose a next step; this is a challenge for TP: either a radical |
|
555 % restriction of the search space by restriction to very specific |
|
556 % problem classes is required, or much care and effort is required in |
|
557 % designing possible variants in the process of problem solving |
|
558 % \cite{proof-strategies-11}. |
|
559 % \par |
|
560 % Another approach is restricted to problem solving in engineering |
|
561 % domains, where a problem is specified by input, precondition, output |
|
562 % and postcondition, and where the postcondition is proven by ATP behind |
|
563 % the scenes: Here the possible variants in the process of problem |
|
564 % solving are provided with feedback {\em automatically}, if the problem |
|
565 % is described in a TP-based programing language: \cite{plmms10} the |
|
566 % programmer only describes the math algorithm without caring about |
|
567 % interaction (the respective program is functional and even has no |
|
568 % input or output statements!); interaction is generated as a |
|
569 % side-effect by the interpreter --- an efficient separation of concern |
|
570 % between math programmers and dialog designers promising application |
|
571 % all over engineering disciplines. |
|
572 % |
|
573 % |
|
574 % \subsubsection{Math Authoring in Isabelle/ISAC\label{math-auth}} |
|
575 % Authoring new mathematics knowledge in {{\sisac}} can be compared with |
|
576 % ``application programing'' of engineering problems; most of such |
|
577 % programing uses CAS-based programing languages (CAS = Computer Algebra |
|
578 % Systems; e.g. Mathematica's or Maple's programing language). |
|
579 % |
|
580 % \paragraph{A novel type of TP-based language} is used by {{\sisac}{}} |
|
581 % \cite{plmms10} for describing how to construct a solution to an |
|
582 % engineering problem and for calling equation solvers, integration, |
|
583 % etc~\footnote{Implementation of CAS-like functionality in TP is not |
|
584 % primarily concerned with efficiency, but with a didactic question: |
|
585 % What to decide for: for high-brow algorithms at the state-of-the-art |
|
586 % or for elementary algorithms comprehensible for students?} within TP; |
|
587 % TP can ensure ``systems that never make a mistake'' \cite{casproto} - |
|
588 % are impossible for CAS which have no logics underlying. |
|
589 % |
|
590 % \subparagraph{Authoring is perfect} by writing such TP based programs; |
|
591 % the application programmer is not concerned with interaction or with |
|
592 % user guidance: this is concern of a novel kind of program interpreter |
|
593 % called Lucas-Interpreter. This interpreter hands over control to a |
|
594 % dialog component at each step of calculation (like a debugger at |
|
595 % breakpoints) and calls automated TP to check user input following |
|
596 % personalized strategies according to a feedback module. |
|
597 % \par |
|
598 % However ``application programing with TP'' is not done with writing a |
|
599 % program: according to the principles of TP, each step must be |
|
600 % justified. Such justifications are given by theorems. So all steps |
|
601 % must be related to some theorem, if there is no such theorem it must |
|
602 % be added to the existing knowledge, which is organized in so-called |
|
603 % \textbf{theories} in Isabelle. A theorem must be proven; fortunately |
|
604 % Isabelle comprises a mechanism (called ``axiomatization''), which |
|
605 % allows to omit proofs. Such a theorem is shown in |
|
606 % Example~\ref{eg:neuper1}. |
|
607 |
|
608 The running example, introduced by Fig.\ref{fig-interactive} on |
|
609 p.\pageref{fig-interactive}, requires to determine the inverse $\cal |
|
610 Z$-transform for a class of functions. The domain of Signal Processing |
|
611 is accustomed to specific notation for the resulting functions, which |
|
612 are absolutely summable and are called TODO: $u[n]$, where $u$ is the |
|
613 function, $n$ is the argument and the brackets indicate that the |
|
614 arguments are TODO. Surprisingly, Isabelle accepts the rules for |
|
615 ${\cal Z}^{-1}$ in this traditional notation~\footnote{Isabelle |
|
616 experts might be particularly surprised, that the brackets do not |
|
617 cause errors in typing (as lists).}: |
|
618 %\vbox{ |
|
619 % \begin{example} |
390 \label{eg:neuper1} |
620 \label{eg:neuper1} |
391 {\small\begin{tabbing} |
621 {\small\begin{tabbing} |
392 123\=123\=123\=123\=\kill |
622 123\=123\=123\=123\=\kill |
393 \hfill \\ |
623 \hfill \\ |
394 \>axiomatization where \\ |
624 \>axiomatization where \\ |
395 \>\> rule1: ``1 = $\delta$ [n]'' and\\ |
625 \>\> rule1: ``${\cal Z}^{-1}\;1 = \delta [n]$'' and\\ |
396 \>\> rule2: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z / (z - 1) = u [n]'' and\\ |
626 \>\> rule2: ``$\vert\vert z \vert\vert > 1 \Rightarrow {\cal Z}^{-1}\;z / (z - 1) = u [n]$'' and\\ |
397 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\ |
627 \>\> rule3: ``$\vert\vert$ z $\vert\vert$ < 1 ==> z / (z - 1) = -u [-n - 1]'' and \\ |
|
628 %TODO |
398 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\ |
629 \>\> rule4: ``$\vert\vert$ z $\vert\vert$ > $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = $\alpha^n$ $\cdot$ u [n]'' and\\ |
|
630 %TODO |
399 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\ |
631 \>\> rule5: ``$\vert\vert$ z $\vert\vert$ < $\vert\vert$ $\alpha$ $\vert\vert$ ==> z / (z - $\alpha$) = -($\alpha^n$) $\cdot$ u [-n - 1]'' and\\ |
400 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]'' |
632 %TODO |
|
633 \>\> rule6: ``$\vert\vert$ z $\vert\vert$ > 1 ==> z/(z - 1)$^2$ = n $\cdot$ u [n]''\\ |
|
634 %TODO |
401 \end{tabbing} |
635 \end{tabbing} |
402 } |
636 } |
403 \end{example} |
637 % \end{example} |
404 } |
638 %} |
405 |
639 These 6 rules can be used as conditional rewrite rules, depending on |
406 In order to provide TP with logical facts for checking user input, the Lucas-Interpreter requires a \textbf{specification}. Such a specification is shown in Example~\ref{eg:neuper2}. |
640 the respective convergence radius. Satisfaction from notation |
|
641 contrasts with the word {\em axiomatization}: As TP-based, the |
|
642 programming language expects these rules as {\em proved} theorems, and |
|
643 not as axioms implemented in the above brute force manner; otherwise |
|
644 all the verification efforts envisaged (like proof of the |
|
645 post-condition, see below) would be meaningless. |
|
646 |
|
647 Isabelle provides a large body of knowledge, rigorously proven from |
|
648 the basic axioms of mathematics~\footnote{This way of rigorously |
|
649 deriving all knowledge from first principles is called the |
|
650 LCF-paradigm in TP.}. In the case of the Z-Transform the most advanced |
|
651 knowledge can be found in the theoris on Multivariate |
|
652 Analysis~\footnote{http://isabelle.in.tum.de/dist/library/HOL/HOL-Multivariate\_Analysis}. However, |
|
653 building up knowledge such that a proof for the above rules would be |
|
654 reasonably short and easily comprehensible, still requires lots of |
|
655 work (and is definitely out of scope of our case study). |
|
656 |
|
657 \medskip At the state-of-the-art in mechanization of knowledge in |
|
658 engineering, the process does not stop with the mechanization of |
|
659 mathematics. Rather, ``Formal Methods''~\cite{TODO-formal-methods} |
|
660 proceed to formal description of physical items. Signal Processing, |
|
661 for instance is concerned with physical devices for signal acquisition |
|
662 and reconstruction, which involve measuring a physical signal, storing |
|
663 it, and possibly later rebuilding the original signal or an |
|
664 approximation thereof. For digital systems, this typically includes |
|
665 sampling and quantization; devices for signal compression, including |
|
666 audio compression, image compression, and video compression, etc. |
|
667 ``Domain engineering''\cite{db-domain-engineering} is concerned with |
|
668 {\em specification} of these devices' components and features; this |
|
669 part in the process of mechanization is only at the beginning. |
|
670 |
|
671 \medskip TP-based programming, concern of this paper, adds a third |
|
672 part of mechanisation, providing a third axis of ``algorithmic |
|
673 knowledge'' in Fig.\ref{fig:mathuni} on p.\pageref{fig:mathuni}. |
|
674 |
|
675 \begin{figure} |
|
676 \hfill \\ |
|
677 \begin{center} |
|
678 \includegraphics{fig/universe} |
|
679 \caption{Didactic ``Math-Universe''\label{fig:mathuni}} |
|
680 \end{center} |
|
681 \end{figure} |
|
682 %WN Deine aktuelle Benennung oben wird Dir kein Fachmann abnehmen; |
|
683 %WN bitte folgende Bezeichnungen nehmen: |
|
684 %WN |
|
685 %WN axis 1: Algorithmic Knowledge (Programs) |
|
686 %WN axis 2: Application-oriented Knowledge (Specifications) |
|
687 %WN axis 3: Deductive Knowledge (Axioms, Definitions, Theorems) |
|
688 |
|
689 \subsection{Specification of the Problem}\label{spec} |
|
690 %WN <--> \chapter 7 der Thesis |
|
691 %WN die Argumentation unten sollte sich NUR auf Verifikation beziehen.. |
|
692 In order to provide TP with logical facts for checking user input, the |
|
693 Lucas-Interpreter requires a \textbf{specification}. Such a |
|
694 specification is shown in Example~\ref{eg:neuper2}. |
|
695 |
|
696 ------------------------------------------------------------------- |
|
697 |
|
698 Hier brauchen wir die Spezifikation des 'running example' ... |
407 |
699 |
408 \vbox{ |
700 \vbox{ |
409 \begin{example} |
701 \begin{example} |
410 \label{eg:neuper2} |
702 \label{eg:neuper2} |
411 {\small\begin{tabbing} |
703 {\small\begin{tabbing} |
437 ``\>\>[Test,solve\_linear])'' \\ |
734 ``\>\>[Test,solve\_linear])'' \\ |
438 ``\>[BOOL equ, REAL z])'' \\ |
735 ``\>[BOOL equ, REAL z])'' \\ |
439 \end{tabbing} |
736 \end{tabbing} |
440 } |
737 } |
441 {\small\textit{ |
738 {\small\textit{ |
442 \noindent If a program requires a result which has to be calculated first we can use a subproblem to do so. In our specific case we wanted to calculate the zeros of a fraction and used a subproblem to calculate the zeros of the denominator polynom. |
739 \noindent If a program requires a result which has to be |
|
740 calculated first we can use a subproblem to do so. In our specific |
|
741 case we wanted to calculate the zeros of a fraction and used a |
|
742 subproblem to calculate the zeros of the denominator polynom. |
443 }} |
743 }} |
444 \end{example} |
744 \end{example} |
445 } |
745 } |
446 |
746 |
|
747 \subsection{Implementation of the Method}\label{meth} |
|
748 %WN <--> \chapter 7 der Thesis |
|
749 TODO |
|
750 \subsection{Preparation of ML-Functions for the Program}\label{funs} |
|
751 %WN <--> Thesis 6.1 -- 6.3: jene ausw"ahlen, die Du f"ur \label{progr} |
|
752 %WN brauchst |
|
753 TODO |
|
754 \subsection{Implementation of the TP-based Program}\label{progr} |
|
755 %WN <--> \chapter 8 der Thesis |
|
756 TODO |
|
757 |
447 \section{Workflow of Programming in the Prototype}\label{workflow} |
758 \section{Workflow of Programming in the Prototype}\label{workflow} |
|
759 ------------------------------------------------------------------- |
|
760 |
|
761 ``workflow'' heisst: das mache ich zuerst, dann das ... |
|
762 |
|
763 \subsection{Preparations and Trials}\label{flow-prep} |
|
764 TODO ... Build\_Inverse\_Z\_Transform.thy !!! |
|
765 |
|
766 \subsection{Implementation in Isabelle/{\isac}}\label{flow-impl} |
|
767 TODO Build\_Inverse\_Z\_Transform.thy ... ``imports Isac'' |
|
768 |
|
769 \subsection{Transfer into the Isabelle/{\isac} Knowledge}\label{flow-trans} |
|
770 TODO http://www.ist.tugraz.at/isac/index.php/Extend\_ISAC\_Knowledge\#Add\_an\_example ? |
|
771 |
|
772 ------------------------------------------------------------------- |
|
773 |
|
774 Das unterhalb hab' ich noch nicht durchgearbeitet; einiges w\"are |
|
775 vermutlich auf andere sections aufzuteilen. |
|
776 |
|
777 ------------------------------------------------------------------- |
448 |
778 |
449 \subsection{Formalization of missing knowledge in Isabelle} |
779 \subsection{Formalization of missing knowledge in Isabelle} |
450 |
780 |
451 \paragraph{A problem} behind is the mechanization of mathematic theories in TP-bases languages. There is still a huge gap between these algorithms and this what we want as a solution - in Example Signal Processing. |
781 \paragraph{A problem} behind is the mechanization of mathematic |
|
782 theories in TP-bases languages. There is still a huge gap between |
|
783 these algorithms and this what we want as a solution - in Example |
|
784 Signal Processing. |
452 |
785 |
453 \vbox{ |
786 \vbox{ |
454 \begin{example} |
787 \begin{example} |
455 \label{eg:gap} |
788 \label{eg:gap} |
456 \[ |
789 \[ |
457 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY |
790 X\cdot(a+b)+Y\cdot(c+d)=aX+bX+cY+dY |
458 \] |
791 \] |
459 {\small\textit{ |
792 {\small\textit{ |
460 \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 Isabelle for fills it correct - \emph{always}. But sometimes we don't want expand such terms, sometimes we want another structure of 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 simplification and the solution. |
793 \noindent A very simple example on this what we call gap is the |
|
794 simplification above. It is needles to say that it is correct and also |
|
795 Isabelle for fills it correct - \emph{always}. But sometimes we don't |
|
796 want expand such terms, sometimes we want another structure of |
|
797 them. Think of a problem were we now would need only the coefficients |
|
798 of $X$ and $Y$. This is what we call the gap between mechanical |
|
799 simplification and the solution. |
461 }} |
800 }} |
462 \end{example} |
801 \end{example} |
463 } |
802 } |
464 |
803 |
465 \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: Mechanized math starts from mathematical models and \emph{hopefully} proceeds to match physics. Academic engineering starts from physics (experimentation, measurement) and then proceeds to mathematical modeling and formalization. The process from a physical observance to a mathematical theory is unavoidable bound of setting up a big collection of standards, rules, definition but also exceptions. These are the things making mechanization that difficult. |
804 \paragraph{We are not able to fill this gap,} until we have to live |
|
805 with it but first have a look on the meaning of this statement: |
|
806 Mechanized math starts from mathematical models and \emph{hopefully} |
|
807 proceeds to match physics. Academic engineering starts from physics |
|
808 (experimentation, measurement) and then proceeds to mathematical |
|
809 modeling and formalization. The process from a physical observance to |
|
810 a mathematical theory is unavoidable bound of setting up a big |
|
811 collection of standards, rules, definition but also exceptions. These |
|
812 are the things making mechanization that difficult. |
466 |
813 |
467 \vbox{ |
814 \vbox{ |
468 \begin{example} |
815 \begin{example} |
469 \label{eg:units} |
816 \label{eg:units} |
470 \[ |
817 \[ |
471 m,\ kg,\ s,\ldots |
818 m,\ kg,\ s,\ldots |
472 \] |
819 \] |
473 {\small\textit{ |
820 {\small\textit{ |
474 \noindent Think about some units like that one's above. Behind each unit there is a discerning and very accurate definition: One 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 platinum-iridium cylinder in paris; and so on. But are these definitions usable in a computer mechanized world?! |
821 \noindent Think about some units like that one's above. Behind |
|
822 each unit there is a discerning and very accurate definition: One |
|
823 Meter is the distance the light travels, in a vacuum, through the time |
|
824 of 1 / 299.792.458 second; one kilogram is the weight of a |
|
825 platinum-iridium cylinder in paris; and so on. But are these |
|
826 definitions usable in a computer mechanized world?! |
475 }} |
827 }} |
476 \end{example} |
828 \end{example} |
477 } |
829 } |
478 |
830 |
479 \paragraph{A computer} or a TP-System builds on programs with predefined logical rules and does not know any mathematical trick (follow up example \ref{eg:trick}) or recipe to walk around difficult expressions. |
831 \paragraph{A computer} or a TP-System builds on programs with |
|
832 predefined logical rules and does not know any mathematical trick |
|
833 (follow up example \ref{eg:trick}) or recipe to walk around difficult |
|
834 expressions. |
480 |
835 |
481 \vbox{ |
836 \vbox{ |
482 \begin{example} |
837 \begin{example} |
483 \label{eg:trick} |
838 \label{eg:trick} |
484 \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] |
839 \[ \frac{1}{j\omega}\cdot\left(e^{-j\omega}-e^{j3\omega}\right)= \] |
485 \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= |
840 \[ \frac{1}{j\omega}\cdot e^{-j2\omega}\cdot\left(e^{j\omega}-e^{-j\omega}\right)= |
486 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] |
841 \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$\frac{1}{j}\,\left(e^{j\omega}-e^{-j\omega}\right)$}= \] |
487 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] |
842 \[ \frac{1}{\omega}\, e^{-j2\omega}\cdot\colorbox{lgray}{$2\, sin(\omega)$} \] |
488 {\small\textit{ |
843 {\small\textit{ |
489 \noindent Sometimes it is also useful to be able to apply some \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 hard to find out what operations have to be done to transform a result into a meaningful one. |
844 \noindent Sometimes it is also useful to be able to apply some |
|
845 \emph{tricks} to get a beautiful and particularly meaningful result, |
|
846 which we are able to interpret. But as seen in this example it can be |
|
847 hard to find out what operations have to be done to transform a result |
|
848 into a meaningful one. |
490 }} |
849 }} |
491 \end{example} |
850 \end{example} |
492 } |
851 } |
493 |
852 |
494 \paragraph{The only possibility,} for such a system, is to work through its known definitions and stops if none of these fits. Specified on Signal Processing or any other application it is often possible to walk through by doing simple creases. This creases are in general based on simple math operational but the challenge is to teach the machine \emph{all}\footnote{Its pride to call it \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 survey of knowledge which links to other knowledge and {\sisac{}} a trainer and helper but no human compensating calculator. |
853 \paragraph{The only possibility,} for such a system, is to work |
|
854 through its known definitions and stops if none of these |
|
855 fits. Specified on Signal Processing or any other application it is |
|
856 often possible to walk through by doing simple creases. This creases |
|
857 are in general based on simple math operational but the challenge is |
|
858 to teach the machine \emph{all}\footnote{Its pride to call it |
|
859 \emph{all}.} of them. Unfortunately the goal of TP Isabelle is to |
|
860 reach a high level of \emph{all} but it in real it will still be a |
|
861 survey of knowledge which links to other knowledge and {{\sisac}{}} a |
|
862 trainer and helper but no human compensating calculator. |
495 \par |
863 \par |
496 {{\sisac{}}} itself aims to adds an \emph{application} axis (formal specifications of problems out of topics from Signal Processing, etc.) and an \emph{algorithmic} axis to the \emph{deductive} axis of physical knowledge. The result is a three-dimensional universe of mathematics seen in Figure~\ref{fig:mathuni}. |
864 {{{\sisac}{}}} itself aims to adds an \emph{application} axis (formal |
|
865 specifications of problems out of topics from Signal Processing, etc.) |
|
866 and an \emph{algorithmic} axis to the \emph{deductive} axis of |
|
867 physical knowledge. The result is a three-dimensional universe of |
|
868 mathematics seen in Figure~\ref{fig:mathuni}. |
497 |
869 |
498 \begin{figure} |
870 \begin{figure} |
499 \hfill \\ |
871 \hfill \\ |
500 \begin{center} |
872 \begin{center} |
501 \includegraphics{fig/universe} |
873 \includegraphics{fig/universe} |
515 |
892 |
516 |
893 |
517 \[ f(p)=\ldots\; p \in \quad R \] |
894 \[ f(p)=\ldots\; p \in \quad R \] |
518 |
895 |
519 {\small\textit{ |
896 {\small\textit{ |
520 \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 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 computer science now we have the problem to tell the machine (TP) the difference between this two notations. This Problem is called \emph{Lambda Calculus}. |
897 \noindent Above we see two equations. The first equation aims to |
|
898 be a mapping of an function from the reel range to the reel one, but |
|
899 when we change only one letter we get the second equation which |
|
900 usually aims to insert a reel point $p$ into the reel function. In |
|
901 computer science now we have the problem to tell the machine (TP) the |
|
902 difference between this two notations. This Problem is called |
|
903 \emph{Lambda Calculus}. |
521 }} |
904 }} |
522 \end{example} |
905 \end{example} |
523 } |
906 } |
524 |
907 |
525 \paragraph{An other problem} is that terms are not full simplified in traditional notations, in {\sisac} 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 {\sisac} but in tradition we keep fractions as long as possible and as long as they aim to be \textit{beautiful} (1/8, 5/16,...). |
908 \paragraph{An other problem} is that terms are not full simplified in |
526 \subparagraph{The math} which should be mechanized in Computer Theorem Provers (\emph{TP}) has (almost) a problem with traditional notations (predicate calculus) for axioms, definitions, lemmas, theorems as a computer program 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 these symbols we still have a problem to interpret them at all. (Follow up \hbox{Example \ref{eg:symbint1}}) |
909 traditional notations, in {{\sisac}} we have to simplify them complete |
|
910 to check weather results are compatible or not. in e.g. the solutions |
|
911 of an second order linear equation is an rational in {{\sisac}} but in |
|
912 tradition we keep fractions as long as possible and as long as they |
|
913 aim to be \textit{beautiful} (1/8, 5/16,...). |
|
914 \subparagraph{The math} which should be mechanized in Computer Theorem |
|
915 Provers (\emph{TP}) has (almost) a problem with traditional notations |
|
916 (predicate calculus) for axioms, definitions, lemmas, theorems as a |
|
917 computer program or script is not able to interpret every Greek or |
|
918 Latin letter and every Greek, Latin or whatever calculations |
|
919 symbol. Also if we would be able to handle these symbols we still have |
|
920 a problem to interpret them at all. (Follow up \hbox{Example |
|
921 \ref{eg:symbint1}}) |
527 |
922 |
528 \vbox{ |
923 \vbox{ |
529 \begin{example} |
924 \begin{example} |
530 \label{eg:symbint1} |
925 \label{eg:symbint1} |
531 \[ |
926 \[ |
532 u\left[n\right] \ \ldots \ unitstep |
927 u\left[n\right] \ \ldots \ unitstep |
533 \] |
928 \] |
534 {\small\textit{ |
929 {\small\textit{ |
535 \noindent The unitstep is something we need to solve Signal Processing problem classes. But in {{\sisac{}}} the rectangular brackets have a different meaning. So we abuse them for our requirements. We get something which is not defined, but usable. The Result is syntax only without semantic. |
930 \noindent The unitstep is something we need to solve Signal |
|
931 Processing problem classes. But in {{{\sisac}{}}} the rectangular |
|
932 brackets have a different meaning. So we abuse them for our |
|
933 requirements. We get something which is not defined, but usable. The |
|
934 Result is syntax only without semantic. |
536 }} |
935 }} |
537 \end{example} |
936 \end{example} |
538 } |
937 } |
539 |
938 |
540 In different problems, symbols and letters have different meanings and ask for different ways to get through. (Follow up \hbox{Example \ref{eg:symbint2}}) |
939 In different problems, symbols and letters have different meanings and |
|
940 ask for different ways to get through. (Follow up \hbox{Example |
|
941 \ref{eg:symbint2}}) |
541 |
942 |
542 \vbox{ |
943 \vbox{ |
543 \begin{example} |
944 \begin{example} |
544 \label{eg:symbint2} |
945 \label{eg:symbint2} |
545 \[ |
946 \[ |
546 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent |
947 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent |
547 \] |
948 \] |
548 {\small\textit{ |
949 {\small\textit{ |
549 \noindent For using exponents the three \texttt{widehat} symbols are required. The reason for that is due the development of {{\sisac{}}} the single \texttt{widehat} and also the double were already in use for different operations. |
950 \noindent For using exponents the three \texttt{widehat} symbols |
|
951 are required. The reason for that is due the development of |
|
952 {{{\sisac}{}}} the single \texttt{widehat} and also the double were |
|
953 already in use for different operations. |
550 }} |
954 }} |
551 \end{example} |
955 \end{example} |
552 } |
956 } |
553 |
957 |
554 \paragraph{Also the output} can be a problem. We are familiar with a specified notations and style taught in university but a computer program has no knowledge of the form proved by a professor and the machines themselves also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a human 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 live with. |
958 \paragraph{Also the output} can be a problem. We are familiar with a |
|
959 specified notations and style taught in university but a computer |
|
960 program has no knowledge of the form proved by a professor and the |
|
961 machines themselves also have not yet the possibilities to print every |
|
962 symbol (correct) Recent developments provide proofs in a human |
|
963 readable format but according to the fact that there is no money for |
|
964 good working formal editors yet, the style is one thing we have to |
|
965 live with. |
555 |
966 |
556 \section{Problems rising out of the Development Environment} |
967 \section{Problems rising out of the Development Environment} |
557 |
968 |
558 fehlermeldungen! TODO |
969 fehlermeldungen! TODO |
559 |
970 |
560 \section{Conclusion} |
971 \section{Conclusion}\label{conclusion} |
561 |
972 |
562 TODO |
973 TODO |
563 |
974 |
564 \bibliographystyle{alpha} |
975 \bibliographystyle{alpha} |
565 \bibliography{references} |
976 \bibliography{references} |