122 This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in STEOP, the introductory orientation phase. STEOP is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. |
122 This thesis is the first attempt to tackle the above mentioned issue, it focuses on Telematics, because these specific studies focus on mathematics in STEOP, the introductory orientation phase. STEOP is considered an opportunity to investigate the impact of {\sisac}'s prototype on the issue and others. |
123 |
123 |
124 \medskip |
124 \medskip |
125 The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part. |
125 The thesis is structured as follows: Part I concerns theory, part II the implementation work, where the latter is the main part. |
126 |
126 |
127 In part I, \S\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (\S\ref{emas}) and introduces the notions required for the implementation work (\S\ref{math-auth}). In particular, \S\ref{user-guid} explains, why math authoring in \sisac{} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to \S\ref{sec:goals}. |
127 In part I, \S\ref{isabisac} gives a brief description of the state-of-the-art for educational math assistants (\S\ref{emas}) and introduces the notions required for the implementation work (\S\ref{math-auth}). In particular, \S\ref{user-guid} explains, why math authoring in {\sisac{}} is {\em not} concerned with interaction (and thus not with user guidance etc at all~!). So a concise description of the thesis' goals needs to be postponed to \S\ref{sec:goals}. |
128 |
128 |
129 \S\ref{sp} analyzes ten (TODO: exact no?) problems defined by the SPSC Lab for the knowledge already provided (\S\ref{know-isab}, \S\ref{know-isac}), discusses the selection of problems for implementation (\S\ref{know-missing}) TODO: further structure ? |
129 \S\ref{sp} analyzes ten (TODO: exact no?) problems defined by the SPSC Lab for the knowledge already provided (\S\ref{know-isab}, \S\ref{know-isac}), discusses the selection of problems for implementation (\S\ref{know-missing}) TODO: further structure ? |
130 %(\S\ref{}) |
130 %(\S\ref{}) |
131 |
131 |
132 \section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac} |
132 \section{Mechanization of Math in Isabelle/{\isac}}\label{isabisac} |
160 % {\small\textit{ |
160 % {\small\textit{ |
161 % \noindent Sometimes it is also usefull to be able to apply some \emph{tricks} to get a beautiful and particulary 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. |
161 % \noindent Sometimes it is also usefull to be able to apply some \emph{tricks} to get a beautiful and particulary 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. |
162 % }} |
162 % }} |
163 % \caption{Mathematic tricks}\label{eg:trick} |
163 % \caption{Mathematic tricks}\label{eg:trick} |
164 %\end{example} |
164 %\end{example} |
165 %For such a system the only possibility 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 generell based on simple math operatiopms but the challange is to teach the machine \emph{all}\footnote{Its pride to call it \emph{all}.} of them. Unfortunataly the goal of CTP 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 calulator. |
165 %For such a system the only possibility 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 generell based on simple math operatiopms but the challange is to teach the machine \emph{all}\footnote{Its pride to call it \emph{all}.} of them. Unfortunataly the goal of CTP 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 calulator. |
166 %\par {\sisac{}} itselfs aims to adds an \emph{application} axis (formal specifications of problems outof 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. |
166 %\par {{\sisac{}}} itselfs aims to adds an \emph{application} axis (formal specifications of problems outof 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. |
167 % |
167 % |
168 %\subsubsection*{Notes on Mechanization of Mathematics} |
168 %\subsubsection*{Notes on Mechanization of Mathematics} |
169 %This thesis tries to \emph{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. As we are still in a eary part of development, this is the first thesis dealing within this topic and there is \emph{no} related work to guid through. A more detailed description about this fact can be found in Section \ref{sec:related}. |
169 %This thesis tries to \emph{connect} these two worlds and is one of the first guidelines to implement problem classes in {\sisac}. As we are still in a eary part of development, this is the first thesis dealing within this topic and there is \emph{no} related work to guid through. A more detailed description about this fact can be found in Section \ref{sec:related}. |
170 %The major challenge of the practical part, of this thesis, is, that "connecting the two worlds" involves programming in a CTP-based programming language which is in a very early state of prototyping. There is no concrete experience data ready to grep. |
170 %The major challenge of the practical part, of this thesis, is, that "connecting the two worlds" involves programming in a CTP-based programming language which is in a very early state of prototyping. There is no concrete experience data ready to grep. |
171 % |
171 % |
172 As mentioned in the introduction, a prototype of an educational math assistant called \sisac\footnote{\sisac=\textbf{Isa}belle \cite{Nipkow-Paulson-Wenzel:2002} 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 (CTP), 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: |
172 As mentioned in the introduction, a prototype of an educational math assistant called {\sisac}\footnote{{\sisac}=\textbf{Isa}belle \cite{Nipkow-Paulson-Wenzel:2002} 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 (CTP), 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: |
173 \begin{enumerate} |
173 \begin{enumerate} |
174 \item Introduction of math stuff (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 |
174 \item Introduction of math stuff (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 |
175 \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 partical fraction decomposition): ``next step guidance'' supports students in independenly (re-)adopting such techniques. |
175 \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 partical fraction decomposition): ``next step guidance'' supports students in independenly (re-)adopting such techniques. |
176 \end{enumerate} |
176 \end{enumerate} |
177 Before the question is answers, how {\sisac} accoplishes this task from a technical point of view, some remarks on the state-of-the-art is given: |
177 Before the question is answers, how {\sisac} accoplishes this task from a technical point of view, some remarks on the state-of-the-art is given: |
235 Such a specification is checked before the execution of a program is started, the same applies for sub-programs. In the following example program the sub-programs are designated by {\tt SubProblem}: TODO one example. |
235 Such a specification is checked before the execution of a program is started, the same applies for sub-programs. In the following example program the sub-programs are designated by {\tt SubProblem}: TODO one example. |
236 |
236 |
237 |
237 |
238 \subsection{Goals of the Thesis}\label{sec:goals} |
238 \subsection{Goals of the Thesis}\label{sec:goals} |
239 %Imagine a piece of software would be able to support you by understanding every problem class, upcoming in the first years attending university - wouldn't it be great? |
239 %Imagine a piece of software would be able to support you by understanding every problem class, upcoming in the first years attending university - wouldn't it be great? |
240 %\par {\sisac{}} tries to do that, but the current state of the art is miles away from this goal and a single implementation of a problem is not enough to cahnge this circumstamce. Through this fact it is all the more essential to try, test, research and document the implementation of problem classes from "`real world"' applications. Responding to the abstract at the begin of this document the thesis has two folds; on the one hand certainly to provide interactiv course material for Signal Processing (which means to implement a single problem provided by the Institute of Signal Processing and Speech Communication (SPSC); follow up Calulcations), and to extract experience data respectively help the {\sisac{}}-team by setting up a detailed description of technicalities hacking {\sisac{}} on the other hand. |
240 %\par {{\sisac{}}} tries to do that, but the current state of the art is miles away from this goal and a single implementation of a problem is not enough to cahnge this circumstamce. Through this fact it is all the more essential to try, test, research and document the implementation of problem classes from "`real world"' applications. Responding to the abstract at the begin of this document the thesis has two folds; on the one hand certainly to provide interactiv course material for Signal Processing (which means to implement a single problem provided by the Institute of Signal Processing and Speech Communication (SPSC); follow up Calulcations), and to extract experience data respectively help the {{\sisac{}}}-team by setting up a detailed description of technicalities hacking {{\sisac{}}} on the other hand. |
241 %\par Another goal is to demonstrate the power and attractivity of {\sisac}. |
241 %\par Another goal is to demonstrate the power and attractivity of {\sisac}. |
242 Now all the notions are in place to describe the task ``Interactive Course Material for Signal Processing based on Isabelle/\sisac'' appropriately by the following points: |
242 Now all the notions are in place to describe the task ``Interactive Course Material for Signal Processing based on Isabelle/{\sisac}'' appropriately by the following points: |
243 \begin{enumerate} |
243 \begin{enumerate} |
244 \item Analyze the problems given by the SPSC Lab for mathematics \textbf{knowledge required}, search the knowledge already available in Isabelle/\sisac, estimate efforts required to fill the gap between knowledge required and knowledge available, and finally select problems for implementation accordingly. |
244 \item Analyze the problems given by the SPSC Lab for mathematics \textbf{knowledge required}, search the knowledge already available in Isabelle/{\sisac}, estimate efforts required to fill the gap between knowledge required and knowledge available, and finally select problems for implementation accordingly. |
245 \item Implement the selected problems in Isabelle/\sisac, which means, in appropriate Isabelle theories \textbf{for each problem} implement: |
245 \item Implement the selected problems in Isabelle/{\sisac}, which means, in appropriate Isabelle theories \textbf{for each problem} implement: |
246 \begin{enumerate} |
246 \begin{enumerate} |
247 \item \textbf{Definitions and theorems} required within the specification (including ``descriptions'' for input variables and output variables) and the program (proofs omitted via ``axiomaization'') |
247 \item \textbf{Definitions and theorems} required within the specification (including ``descriptions'' for input variables and output variables) and the program (proofs omitted via ``axiomaization'') |
248 \item \textbf{A specification} which describes the input variables, the preconditions on the input (a challenge for rigorously exact mathematics~!), the output variables and the postcondition, which relates input to output such that the problem is characterized formally (another challenge for rigorously exact mathematics~!) |
248 \item \textbf{A specification} which describes the input variables, the preconditions on the input (a challenge for rigorously exact mathematics~!), the output variables and the postcondition, which relates input to output such that the problem is characterized formally (another challenge for rigorously exact mathematics~!) |
249 \item \textbf{A program} describing the algorithm which solves the problem, i.e. which constructs output meeting the postcondition. Programming involves identifying the steps (tactics~!) which create the calculation and calling CAS-functions (simplification, equation solvers, etc) appropriately. Modularization of programs into {\tt SubProblems} has to prepare for re-use of code. |
249 \item \textbf{A program} describing the algorithm which solves the problem, i.e. which constructs output meeting the postcondition. Programming involves identifying the steps (tactics~!) which create the calculation and calling CAS-functions (simplification, equation solvers, etc) appropriately. Modularization of programs into {\tt SubProblems} has to prepare for re-use of code. |
250 \end{enumerate} |
250 \end{enumerate} |
252 \item \textbf{Document the implementation} such that |
252 \item \textbf{Document the implementation} such that |
253 \begin{enumerate} |
253 \begin{enumerate} |
254 % \item Interactive course material hopefully useful in education within the SPSC Lab and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and |
254 % \item Interactive course material hopefully useful in education within the SPSC Lab and within STEOP, the introductory orientation phase at TUG, as a preview for students in Telematics on later application of math knowledge introduced in the first semester and |
255 % \item A detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and {\sisac}-developers with feedback in usability of the CTP-based program language. |
255 % \item A detailed description of technicalities in programming implemented as an interactive Isabelle/Isar theory, providing future programmers with guidelines and {\sisac}-developers with feedback in usability of the CTP-based program language. |
256 \item subsequent application programmers have guidelines for further implementation of interactive course material in SPSC and other engineering sciences |
256 \item subsequent application programmers have guidelines for further implementation of interactive course material in SPSC and other engineering sciences |
257 \item \sisac{} developers get feedback for ongoing improvement of the CTP-based programming language, the respective development environment and the respective program interpreter (called Lucas-Interpreter) |
257 \item {\sisac{}} developers get feedback for ongoing improvement of the CTP-based programming language, the respective development environment and the respective program interpreter (called Lucas-Interpreter) |
258 \item development of knowledge for engineering sciences is being motivated in the Isabelle community. |
258 \item development of knowledge for engineering sciences is being motivated in the Isabelle community. |
259 \end{enumerate} |
259 \end{enumerate} |
260 \end{enumerate} |
260 \end{enumerate} |
261 |
261 |
262 |
262 |
307 |
307 |
308 \begin{table}[H] |
308 \begin{table}[H] |
309 \begin{centering} |
309 \begin{centering} |
310 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
310 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
311 requirements & comments &effort\\ \hline\hline |
311 requirements & comments &effort\\ \hline\hline |
312 simplify rationals & \sisac & 0\\ \hline |
312 simplify rationals & {\sisac} & 0\\ \hline |
313 define $\sum\limits_{i=0}^{n}i$ & partly \sisac & 10\\ \hline |
313 define $\sum\limits_{i=0}^{n}i$ & partly {\sisac} & 10\\ \hline |
314 simplify sum & termorder & 10\\ |
314 simplify sum & termorder & 10\\ |
315 & simplify rules & 20\\ |
315 & simplify rules & 20\\ |
316 & use simplify rationals& 0\\ \hline |
316 & use simplify rationals& 0\\ \hline |
317 index adjustments & with unit step & 10\\ \hline |
317 index adjustments & with unit step & 10\\ \hline |
318 example collection & with explanations & 20\\ \hline\hline |
318 example collection & with explanations & 20\\ \hline\hline |
324 |
324 |
325 \begin{table}[H] |
325 \begin{table}[H] |
326 \begin{centering} |
326 \begin{centering} |
327 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
327 \begin{tabular}{p{4cm}|p{5cm}|rp{2.5cm}} |
328 requirements & comments &effort\\ \hline\hline |
328 requirements & comments &effort\\ \hline\hline |
329 solve for part.fract. & \sisac: degree 2 & 0\\ |
329 solve for part.fract. & {\sisac}: degree 2 & 0\\ |
330 & complex nomminators & 30\\ |
330 & complex nomminators & 30\\ |
331 & degree > 2 & MT\\ \hline |
331 & degree > 2 & MT\\ \hline |
332 simplify polynomial & \sisac & 0\\ |
332 simplify polynomial & {\sisac} & 0\\ |
333 simplify rational & \sisac & 0\\ \hline |
333 simplify rational & {\sisac} & 0\\ \hline |
334 partial fraction & degree 2, & 20\\ |
334 partial fraction & degree 2, & 20\\ |
335 decomposition & specification, method& 30\\ \hline |
335 decomposition & specification, method& 30\\ \hline |
336 ${\cal Z}^{-1}$ table & explanations, figures& 20\\ \hline |
336 ${\cal Z}^{-1}$ table & explanations, figures& 20\\ \hline |
337 example collection & with explanations & 20\\ \hline\hline |
337 example collection & with explanations & 20\\ \hline\hline |
338 \multicolumn{2}{c|}{} & 90-120\\ |
338 \multicolumn{2}{c|}{} & 90-120\\ |
367 \begin{example} |
367 \begin{example} |
368 \[ |
368 \[ |
369 u\left[n\right] \ \ldots \ unitstep |
369 u\left[n\right] \ \ldots \ unitstep |
370 \] |
370 \] |
371 {\small\textit{ |
371 {\small\textit{ |
372 \noindent The unitstep is something we need to solve Signal Processing problem classes. But in {\sisac{}} the rectangular breakets have a different meaning. So we abuse them for our requirements. We get something which is not defined, but useable. The Result is syntax only without semantic. |
372 \noindent The unitstep is something we need to solve Signal Processing problem classes. But in {{\sisac{}}} the rectangular breakets have a different meaning. So we abuse them for our requirements. We get something which is not defined, but useable. The Result is syntax only without semantic. |
373 }} |
373 }} |
374 \caption{Expression Interpretation}\label{eg:symbint1} |
374 \caption{Expression Interpretation}\label{eg:symbint1} |
375 \end{example} |
375 \end{example} |
376 |
376 |
377 \noindent In different problems, symbols and letters have different meanings and ask for different ways to get through. (Follow up \hbox{Example \ref{eg:symbint2}}) |
377 \noindent In different problems, symbols and letters have different meanings and ask for different ways to get through. (Follow up \hbox{Example \ref{eg:symbint2}}) |
378 \begin{example} |
378 \begin{example} |
379 \[ |
379 \[ |
380 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent |
380 \widehat{\ }\ \widehat{\ }\ \widehat{\ } \ \ldots \ exponent |
381 \] |
381 \] |
382 {\small\textit{ |
382 {\small\textit{ |
383 \noindent For using exponents the three widehat symbols are required. The reason for that is due the development of {\sisac{}} the single widehat and also the double were already in use for different operations. |
383 \noindent For using exponents the three widehat symbols are required. The reason for that is due the development of {{\sisac{}}} the single widehat and also the double were already in use for different operations. |
384 }} |
384 }} |
385 \caption{Symbol Interpretation}\label{eg:symbint2} |
385 \caption{Symbol Interpretation}\label{eg:symbint2} |
386 \end{example} |
386 \end{example} |
387 Exclusive from the input, also the output can be a problem. We are familar with a specified notations and style taught in university but a computer programm has no knowledge of the form probved by a professor and the maschines themselve also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a humand readable format but according to the fact that there is no mony for good working formel editors yet, the style is one thing we have to live with. |
387 Exclusive from the input, also the output can be a problem. We are familar with a specified notations and style taught in university but a computer programm has no knowledge of the form probved by a professor and the maschines themselve also have not yet the possibilities to print every symbol (correct) Recent developments provide proofs in a humand readable format but according to the fact that there is no mony for good working formel editors yet, the style is one thing we have to live with. |
388 |
388 |
389 \section{Milestones for the Thesis} |
389 \section{Milestones for the Thesis} |
390 The thesis was splitted into six iterations |
390 The thesis was splitted into six iterations |
391 \begin{description} |
391 \begin{description} |
392 \item[(29.06. -- 27.07.)] Collection of detailed informations about different STEOP topics \ref{ssec:infcol} |
392 \item[(29.06. -- 27.07.)] Collection of detailed informations about different STEOP topics \ref{ssec:infcol} |
393 \item[(27.07.)] First Prsentation - Decition on which Problems will be implemented \ref{ssec:pres1} |
393 \item[(27.07.)] First Prsentation - Decition on which Problems will be implemented \ref{ssec:pres1} |
394 \item[(01.09. -- 11.11.)] Implementing the Problem Class in {\sisac{}} \ref{ssec:impl} |
394 \item[(01.09. -- 11.11.)] Implementing the Problem Class in {{\sisac{}}} \ref{ssec:impl} |
395 \item[(14.11. -- 02.12.)] Documentation of the Implementation \ref{ssec:doc} |
395 \item[(14.11. -- 02.12.)] Documentation of the Implementation \ref{ssec:doc} |
396 \item[(05.12. -- todo)] Writting on the thesis \ref{ssec:thes} |
396 \item[(05.12. -- todo)] Writting on the thesis \ref{ssec:thes} |
397 \item[todo] Second Prsentation - Work review \ref{ssec:pres2} |
397 \item[todo] Second Prsentation - Work review \ref{ssec:pres2} |
398 \end{description} |
398 \end{description} |
399 |
399 |
408 \subsection{Writting on the thesis}\label{ssec:thes} |
408 \subsection{Writting on the thesis}\label{ssec:thes} |
409 \subsection{Second Prsentation - Work review}\label{ssec:pres2} |
409 \subsection{Second Prsentation - Work review}\label{ssec:pres2} |
410 |
410 |
411 \section{Related Work}\label{sec:related} |
411 \section{Related Work}\label{sec:related} |
412 Unusual for a Baccalaureate Thesis, there is {\em no} related work; this requires explanation. |
412 Unusual for a Baccalaureate Thesis, there is {\em no} related work; this requires explanation. |
413 Of course, this thesis relies on front-of-the wave computer mathematics, on CTP. But {\sisac{}} uses CTP in a very specific way, which is too weakly related to other work: programming in the CTP-based language and rigorous formal specification of problems in Signal Processing where the main tasks in the practical part of this thesis. The major challenge for the practical work was given by the fact, that the work concerned alpha-testing of the CTP-based programming environment. |
413 Of course, this thesis relies on front-of-the wave computer mathematics, on CTP. But {{\sisac{}}} uses CTP in a very specific way, which is too weakly related to other work: programming in the CTP-based language and rigorous formal specification of problems in Signal Processing where the main tasks in the practical part of this thesis. The major challenge for the practical work was given by the fact, that the work concerned alpha-testing of the CTP-based programming environment. |
414 \par Another area of work could be considered as related work: authoring of e-learning content. However, {\sisac{}} provides division of concern such that the practical part of this thesis could focus on computer mathematics; this work was not concerned with interaction (the CTP-based programming language has neither input statements nor output statements), nor with dialog guidance nor with any kind of learning theory. |
414 \par Another area of work could be considered as related work: authoring of e-learning content. However, {{\sisac{}}} provides division of concern such that the practical part of this thesis could focus on computer mathematics; this work was not concerned with interaction (the CTP-based programming language has neither input statements nor output statements), nor with dialog guidance nor with any kind of learning theory. |
415 \par These two reasons are given for the unusual statement, that there is no related work to be discussed in this thesis. |
415 \par These two reasons are given for the unusual statement, that there is no related work to be discussed in this thesis. |
416 |
416 |
417 \section{Review} |
417 \section{Review} |
418 todo |
418 todo |
419 \section{Open Questions} |
419 \section{Open Questions} |
420 todo |
420 todo |
421 \section{Conclusions} |
421 \section{Conclusions} |
422 todo |
422 todo |
423 |
423 |
424 \bibliographystyle{alpha} |
424 %\bibliographystyle{alpha} |
425 \bibliography{references} |
425 %\bibliography{references} |
426 %\bibliography{bib/math-eng,bib/didact,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math} |
426 %\bibliography{bib/math-eng,bib/didact,bib/bk,bib/RISC_2,bib/isac,bib/pl,bib/math} |
427 |
427 |
428 |
428 |
429 \clearpage |
429 \clearpage |
430 |
430 |