170 \abstract{ |
171 \abstract{ |
171 This is a proposal for a Masters Thesis at RISC, the Research Institute for Symbolic Computation at Linz University.\\ |
172 This is a proposal for a Masters Thesis at RISC, the Research Institute for Symbolic Computation at Linz University.\\ |
172 |
173 |
173 Calculation with fractions is an important part of Computer Algebra Systems (CAS). This proposal aims at a specific part of such calculations, the greatest common divisor (GCD) used for cancellation, but in the very general context of multivariate polynomials. Cancellation of multivariate polynomials is a settled topic in Computer Algebra, respective algorithms well documented and implementations available in all CASs. |
174 Calculation with fractions is an important part of Computer Algebra Systems (CAS). This proposal aims at a specific part of such calculations, the greatest common divisor (GCD) used for cancellation, but in the very general context of multivariate polynomials. Cancellation of multivariate polynomials is a settled topic in Computer Algebra, respective algorithms well documented and implementations available in all CASs. |
174 |
175 |
175 This proposal claims for novelty with respect to the context of implementation in Computer Theorem Proving (CTP). On CTP's present development towards industrial use in software and systems verification, specific domain models involve demand on more and more mathematics, and within mathematics involve demand for more and more features. The proposed implementation of GCD and cancellation follows an actual demand. |
176 This proposal claims for novelty with respect to the context of implementation, an implementation as a CAS-feature in Computer Theorem Proving (CTP). On CTP's present development towards industrial use in software and systems verification, specific domain models involve demand on more and more mathematics, and within mathematics involve demand for more and more features. Thus the proposed implementation of GCD and cancellation follows an actual demand. |
176 |
177 |
177 If the implementation is successful, it might be included into the distribution of Isabelle, one of the two dominating CTPs in Europe. |
178 If the implementation is successful, it is planned to be included into the distribution of Isabelle, one of the two dominating CTPs in Europe. As part of the Isabelle distribution it will also serve the {\sisac} project aiming at an educational math assistant under development at RISC Linz and Graz University of Technology. |
178 } |
179 } |
179 |
180 |
180 \newpage |
181 \newpage |
181 %WN vorerst zu Zwecken der "Ubersicht lassen ... |
182 %WN vorerst zu Zwecken der "Ubersicht lassen ... |
182 \tableofcontents |
183 \tableofcontents |
183 |
184 |
184 \section{Background} |
185 \section{Background} |
185 The \sisac-project is a research and development project at the Institute for Software Technology of the Graz University of Technology. It is an educational mathematics assistant, a single-stepping system for applied mathematics based on the computer theorem prover Isabelle. The special is an easy readable knowledge base including Isabelles HOL-theories and a transparently working knowledge interpreter (a generalization of 'single stepping' algebra systems). |
186 The \sisac-project is a research and development project launched at the Institute for Software Technology of the Graz University of Technology (TUG) and now continued at the Research Institute for Symbolic Computation (RISC) of University of Linz and at the Institute for Information Systems and Computer Media (IICM) of TUG. The resulting \sisac{} prototype is a ``transparent single-stepping system for applied mathematics'' based on the computer theorem prover Isabelle. The prototype has been proven useful in field tests at Austrain schools \cite{imst-htl06-SH,imst-htl07-SH,imst-hpts08-SH} and is now extended for wider use. |
186 The background to both, development and research, is given by actual needs in math education as well as by foundamental questions about 'the mechanization of thinking' as an essential aspect in mathematics and in technology. |
187 |
187 The \sisac-system under construction comprises a tutoring-system and an authoring-system. The latter provides for adaption to various needs of individual users and educational institutions and for extensions to arbitrary fields of applied mathematics. |
188 Authoring knowledge in \sisac{} provides a strict separation of concerns between authoring math knowledge and authoring dialogues. The latter is pursued at IICM, the former is concern of this thesis. Math authoring is done by use of a CTP-based programming language \cite{plmms10} or by use of SML \cite{pl:milner97} as the meta language and implementation language of Isabelle. Since the code resulting from this thesis shall serve Isabelle, it will be written in SML. Via Isabelle distribution this thesis shall also serve \sisac; a re-implementation in \sisac's CTP-based language is planned as a subsequent project -- this will make cancellation transparent for singe-stepping. |
188 |
189 |
189 TODO:\\ |
190 %The special is an easy readable knowledge base including Isabelles HOL-theories and a transparently working knowledge interpreter (a generalization of 'single stepping' algebra systems). |
|
191 %The background to both, development and research, is given by actual needs in math education as well as by foundamental questions about 'the mechanization of thinking' as an essential aspect in mathematics and in technology. |
|
192 %The \sisac-system under construction comprises a tutoring-system and an authoring-system. The latter provides for adaption to various needs of individual users and educational institutions and for extensions to arbitrary fields of applied mathematics. |
|
193 |
|
194 TODO.WN111107 bitte googeln und je einen Absatz kopieren + zitieren woher (PLAGIATsgefahr):\\ |
190 European provers: Isabelle \cite{Nipkow-Paulson-Wenzel:2002}, Coq \cite{Huet_all:94}\\ |
195 European provers: Isabelle \cite{Nipkow-Paulson-Wenzel:2002}, Coq \cite{Huet_all:94}\\ |
191 American provers: PVS~\cite{pvs}, ACL2~\footnote{http://userweb.cs.utexas.edu/~moore/acl2/}\\ |
196 American provers: PVS~\cite{pvs}, ACL2~\footnote{http://userweb.cs.utexas.edu/~moore/acl2/}\\ |
192 |
197 |
193 \section{Goal of the thesis} |
198 \section{Goal of the thesis} |
194 \subsection{Current situation} |
199 \subsection{Current situation} |
195 At the time there is no good implimentation for the problem of canceling fractions in \sisac and or in Isabelle. But because canceling is important for calculating with fractions a new implimentation is necessary. |
200 At the presetn time there is no implimentation for the problem of canceling fractions in Isabelle, and a deficient one in \sisac. But because canceling is important for calculating with fractions a new implimentation is necessary. |
196 |
201 |
197 \subsection{Problem} |
202 \subsection{Problem} |
198 The wish is to handle fractions in \sisac not only in one variable also in more. So the goal of this thesis ist to find, assess and evaluate the existing algorithms and methods for finding the GCD. This will be an functional programm with the posibility to include it into Isabelle. |
203 The wish is to handle fractions in \sisac{} not only in one variable also in more. So the goal of this thesis ist to find, assess and evaluate the existing algorithms and methods for finding the GCD. This will be an functional programm with the posibility to include it into Isabelle, where it will be used by \sisac{} as well. |
199 |
204 |
200 %WN eine pr"azisere Beschreibung des Problems kann ich mir nicht vorstellen (englische Version der Mail haben wir auch, aber sie passt nicht zur deutschen Antwort von Prof.Nipkow) ... |
205 %WN eine pr"azisere Beschreibung des Problems kann ich mir nicht vorstellen (englische Version der Mail haben wir auch, aber sie passt nicht zur deutschen Antwort von Prof.Nipkow) ... |
201 \bigskip |
206 \bigskip |
202 TODO Mail to Prof. Nipkow, leader of the development of Isabelle \cite{Nipkow-Paulson-Wenzel:2002} at TU M\"unchen, Mon, 23 May 2011 08:58:14 +0200: |
207 A mail to Prof. Nipkow, leader of the development of Isabelle \cite{Nipkow-Paulson-Wenzel:2002} at TU M\"unchen, Mon, 23 May 2011 08:58:14 +0200 describes the problem as follows: |
203 \begin{verbatim} |
208 \begin{verbatim} |
204 Eine erste Idee, wie die Integration der Diplomarbeit f"ur |
209 Eine erste Idee, wie die Integration der Diplomarbeit f"ur |
205 einen Benutzer von Isabelle aussehen k"onnte, w"are zum |
210 einen Benutzer von Isabelle aussehen k"onnte, w"are zum |
206 Beispiel im |
211 Beispiel im |
207 |
212 |
235 Tobias Nipkow |
240 Tobias Nipkow |
236 \end{verbatim} |
241 \end{verbatim} |
237 |
242 |
238 |
243 |
239 \subsection{Expected results} |
244 \subsection{Expected results} |
240 Find good algorithms for the different problems, and find out which one will be the best for the special problem.\\ |
245 Implementation of algorithms for the different problems, and find out which one will be the best for the specific requirements in Isabelle.\\ |
241 The program should handling: |
246 The program should accomplish: |
242 \begin{itemize} |
247 \begin{itemize} |
243 \item[]real and rational coefficients. Maybe also imaginary coefficients. |
248 \item Real and rational coefficients. Maybe also imaginary coefficients. |
244 \item[]Multi variable polynomials canceling and adding, when they are in normal form. |
249 \item Canceling and adding multivariate polynomials, when they are in normal form. |
245 \end{itemize} |
250 \end{itemize} |
246 For the program should be used a functional programming language with good commentaries. And it should be based on Isabelle and works correctly in \sisac. |
251 The program will be written in the functional programming language SML with appropriate comments. The resulting code shall meet the coding standards of Isabelle \cite{isar-impl} p.3-10. The integration of the code into the Isabelle distribution will be done by the Isabelle developer team. |
247 |
252 |
248 \section{State of the art} |
253 \section{State of the art} |
249 In a broad view the context of this thesis can be seen as ``computation and deduction'': simplification and in particular cancellation of rational terms is concern of \textbf{computation} implemented in Computer Algebra Systems (CAS) --- whereas the novelty within the thesis is given by an implementation of cancellation in a computer theorem prover (CTP), i.e. in the domain of \textbf{deduction} with respective logical rigor not addressed in the realm of CAS. |
254 In a broad view the context of this thesis can be seen as ``computation and deduction'': simplification and in particular cancellation of rational terms is concern of \textbf{computation} implemented in Computer Algebra Systems (CAS) --- whereas the novelty within the thesis is given by an implementation of cancellation in a computer theorem prover (CTP), i.e. in the domain of \textbf{deduction} with respective logical rigor not addressed in the realm of CAS. |
250 |
255 |
251 Below, after a general survey on computation, represented by CAS, and on deduction, represented by CTP, a more narrow view on ``CAS-functionality in CTP'' is pursued. |
256 Below, after a general survey on computation, represented by CAS, and on deduction, represented by CTP, a more narrow view on ``CAS-functionality in CTP'' is pursued. |
295 \subsection{Motivation for CAS-functionality in CTP} |
300 \subsection{Motivation for CAS-functionality in CTP} |
296 In the realm of CTP formuas are dominated by quantifiers $\forall$, $\exists$ and $\epsilon$ (such) and by operations like $\Rightarrow$, $\land$ and $\lor$. Numbers were strangers initially; numerals have been introduced to Isabelle not much before the year 2000~\footnote{In directory src/Provers/Arith/ see the files cancel\_numerals.ML and cancel\_numeral\_factor.ML in the Isabelle distribution 2011. They still use the notation $\#1,\#2,\#3,\dots$ from before 2000~!}. However, then numerals have been implemented with {\em polymorphic type} such that $2\cdot r\cdot\pi$ ($2$ is type \textit{real}) and $\pi_{\it approx}=3.14\,\land\, 2\cdot r\cdot\pi_{\it approx}$ can be written as well as $\sum_i^n i=\frac{n\cdot(n+1)}{2}$ ($2$ is type \textit{nat}). The different types are inferred by Hindle-Milner type inference \cite{damas-milner-82,Milner-78,Hindley-69}. |
301 In the realm of CTP formuas are dominated by quantifiers $\forall$, $\exists$ and $\epsilon$ (such) and by operations like $\Rightarrow$, $\land$ and $\lor$. Numbers were strangers initially; numerals have been introduced to Isabelle not much before the year 2000~\footnote{In directory src/Provers/Arith/ see the files cancel\_numerals.ML and cancel\_numeral\_factor.ML in the Isabelle distribution 2011. They still use the notation $\#1,\#2,\#3,\dots$ from before 2000~!}. However, then numerals have been implemented with {\em polymorphic type} such that $2\cdot r\cdot\pi$ ($2$ is type \textit{real}) and $\pi_{\it approx}=3.14\,\land\, 2\cdot r\cdot\pi_{\it approx}$ can be written as well as $\sum_i^n i=\frac{n\cdot(n+1)}{2}$ ($2$ is type \textit{nat}). The different types are inferred by Hindle-Milner type inference \cite{damas-milner-82,Milner-78,Hindley-69}. |
297 |
302 |
298 1994 was an important year for CTP: the Pentium Bug caused excitement in the IT community all around the world and motivated INTEL to invest greatly into formal verification of circuits (which carried over to verification of software). Not much later John Harrison mechanized real numbers as Dedekind Cuts in HOL Light \footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} and derived calculus, derivative and integral from that definition \cite{harr:thesis}, an implementation which has been transferred to Isabelle very soon after that~\footnote{In the directory src/HOL/Multivariate\_Analysis/ see the files Gauge\_Measure.thy, Integration.thy, Derivative.thy, Real\_Integration.thy, Brouwer\_Fixpoint.thy, Fashoda.thy}. |
303 1994 was an important year for CTP: the Pentium Bug caused excitement in the IT community all around the world and motivated INTEL to invest greatly into formal verification of circuits (which carried over to verification of software). Not much later John Harrison mechanized real numbers as Dedekind Cuts in HOL Light \footnote{http://www.cl.cam.ac.uk/~jrh13/hol-light/} and derived calculus, derivative and integral from that definition \cite{harr:thesis}, an implementation which has been transferred to Isabelle very soon after that~\footnote{In the directory src/HOL/Multivariate\_Analysis/ see the files Gauge\_Measure.thy, Integration.thy, Derivative.thy, Real\_Integration.thy, Brouwer\_Fixpoint.thy, Fashoda.thy}. |
299 |
304 |
300 Harrison also says that ``CAS are ill-defined'' and gives, among others, an example relevant for this thesis on cancellation: TODO ... meromorphic functions ... |
305 Harrison also says that ``CAS are ill-defined'' and gives, among others, an example relevant for this thesis on cancellation: TODO.WN111104 search for ... meromorphic functions in http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-428.ps.gz |
301 |
306 |
302 \medskip |
307 \medskip |
303 The main motivation for further introduction of CAS-functionality to CTP is also technology-driven: In this decade domain engineering is becoming an academic discipline with industrial relevance \cite{db:dom-eng}: vigorous efforts extend the scope of formal specifications even beyond software technology, and thus respective domains of mathematical knowledge are being mechanized in CTP. The Archive of Formal Proofs~\footnote{http://afp.sourceforge.net/} is Isabelle's repository for such work. |
308 The main motivation for further introduction of CAS-functionality to CTP is also technology-driven: In this decade domain engineering is becoming an academic discipline with industrial relevance \cite{db:dom-eng}: vigorous efforts extend the scope of formal specifications even beyond software technology, and thus respective domains of mathematical knowledge are being mechanized in CTP. The Archive of Formal Proofs~\footnote{http://afp.sourceforge.net/} is Isabelle's repository for such work. |
304 |
309 |
305 \subsection{Simplification within CTP} |
310 \subsection{Simplification within CTP} |
350 \end{verbatim} |
355 \end{verbatim} |
351 %WN: bist du schon angemeldet in den Mailing-Listen isabelle-users@ und isabelle-dev@ ? WENN NICHT, DANN WIRD ES H"OCHSTE ZEIT !!! |
356 %WN: bist du schon angemeldet in den Mailing-Listen isabelle-users@ und isabelle-dev@ ? WENN NICHT, DANN WIRD ES H"OCHSTE ZEIT !!! |
352 |
357 |
353 \subsection{Open Issues with CAS-functionality in CTP}\label{cas-funct} |
358 \subsection{Open Issues with CAS-functionality in CTP}\label{cas-funct} |
354 There is at least one effort explicitly dedicated to implement CAS-functionality in CTP \cite{cezary-phd}. %WN bitte unbedingt lesen (kann von mir in Papierform ausgeborgt werden) !!! |
359 There is at least one effort explicitly dedicated to implement CAS-functionality in CTP \cite{cezary-phd}. %WN bitte unbedingt lesen (kann von mir in Papierform ausgeborgt werden) !!! |
355 In this work three issues has been identified: partiality conditions, multi-valued functions and real numbers. These issues are addressed in the subsequent paragraphs, followed by a forth issue raised by \sisac. |
360 In this work three issues has been identified: partiality conditions, multi-valued functions and real numbers. These issues are addressed in the subsequent paragraphs, followed by a forth issue raised by \sisac{}. |
356 |
361 |
357 \paragraph{Partiality conditions}\label{part-cond} are introduced by partial functions or by conditional rewriting. An example of how the CAS-functionality \cite{cezary-phd} looks like is given on p.\pageref{fig:casproto}. |
362 \paragraph{Partiality conditions}\label{part-cond} are introduced by partial functions or by conditional rewriting. An example of how the CAS-functionality \cite{cezary-phd} looks like is given on p.\pageref{fig:casproto}. |
358 \cite{cezary-phd} gives an introductory example (floated to p.\pageref{fig:casproto}) which will be referred to in the sequel. |
363 \cite{cezary-phd} gives an introductory example (floated to p.\pageref{fig:casproto}) which will be referred to in the sequel. |
359 \input{thol.tex} |
364 \input{thol.tex} |
360 %WN das nachfolgende Format-Problem l"osen wir sp"ater ... |
365 %WN das nachfolgende Format-Problem l"osen wir sp"ater ... |
381 CAS-like input-response loop. For the user input given in the |
386 CAS-like input-response loop. For the user input given in the |
382 \texttt{In} lines, the system produces the output in \texttt{Out} |
387 \texttt{In} lines, the system produces the output in \texttt{Out} |
383 lines together with HOL Light theorems that state the equality |
388 lines together with HOL Light theorems that state the equality |
384 between the input and the output.} |
389 between the input and the output.} |
385 \end{figure} |
390 \end{figure} |
386 In lines {\tt In6, Out6} this examples shows how to reliably simplify $\sqrt{x}$. \cite{caspartial} %TODO |
391 In lines {\tt In6, Out6} this examples shows how to reliably simplify $\sqrt{x}$. \cite{caspartial} gives more details on handling side conditions in formalized partial functions. |
387 gives more details on handling side conditions in formalized partial functions. |
|
388 |
392 |
389 Analoguous to this example, cancellations (this thesis is concerned with) like |
393 Analoguous to this example, cancellations (this thesis is concerned with) like |
390 $$\frac{x^2-y^2}{x^2-x\cdot y}=\frac{x+y}{x}\;\;\;\;{\it assuming}\;x-y\not=0\land x\not=0$$ |
394 $$\frac{x^2-y^2}{x^2-x\cdot y}=\frac{x+y}{x}\;\;\;\;{\it assuming}\;x-y\not=0\land x\not=0$$ |
391 produce assumptions, $x-y\not=0, x\not=0$ here. Since the code produced in the framework of this thesis will be implemented in Isabelle's simplifier (outside this thesis), the presentation to the user will be determined by Isabelle and \sisac{} using the respective component of Isabelle. Also reliable handling of assumptions like $x-y\not=0, x\not=0$ is up to these systems. |
395 produce assumptions, $x-y\not=0, x\not=0$ here. Since the code produced in the framework of this thesis will be implemented in Isabelle's simplifier (outside this thesis), the presentation to the user will be determined by Isabelle and \sisac{}{} using the respective component of Isabelle. Also reliable handling of assumptions like $x-y\not=0, x\not=0$ is up to these systems. |
392 |
396 |
393 \paragraph{Multi-valued functions:}\label{multi-valued} |
397 \paragraph{Multi-valued functions:}\label{multi-valued} |
394 \cite{seeingroots,davenp-multival-10} discuss cases where CAS are error prone when dropping a branch of a multi-valued function~\footnote{``Multivalued \textit{function}'' is a misnomer, since the value of a function applied to a certain argument is unique by definition of function.}. Familiar examples are ... |
398 \cite{seeingroots,davenp-multival-10} discuss cases where CAS are error prone when dropping a branch of a multi-valued function~\footnote{``Multivalued \textit{function}'' is a misnomer, since the value of a function applied to a certain argument is unique by definition of function.}. Familiar examples are ... |
395 %WN ... zur Erkl"arung ein paar Beispiele von http://en.wikipedia.org/wiki/Multivalued_function |
399 %TODO.WN111104 ... zur Erkl"arung ein paar Beispiele von http://en.wikipedia.org/wiki/Multivalued_function |
396 |
400 |
397 \paragraph{Real numbers} cannot be represented by numerals. In engineering applications, however, approximation by floating-point numbers are frequently useful. In CTP floating-point numbers must be handled rigorously as approximations. Already \cite{harr:thesis} introduced operations on real numerals accompanied by rigorous calculation of precision. \cite{russellphd} describes efficient implementation of infinite precision real numbers in Coq. |
401 \paragraph{Real numbers} cannot be represented by numerals. In engineering applications, however, approximation by floating-point numbers are frequently useful. In CTP floating-point numbers must be handled rigorously as approximations. Already \cite{harr:thesis} introduced operations on real numerals accompanied by rigorous calculation of precision. \cite{russellphd} describes efficient implementation of infinite precision real numbers in Coq. |
398 |
402 |
399 \paragraph{All solutions for equations} must be guaranted, if equation solving is embedded within CTP. So, given an equation $f(x)=0$ and the set of solutions $S$ of this equation, we want to have both, |
403 \paragraph{All solutions for equations} must be guaranted, if equation solving is embedded within CTP. So, given an equation $f(x)=0$ and the set of solutions $S$ of this equation, we want to have both, |
400 \begin{eqnarray} |
404 \begin{eqnarray} |
401 \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut} |
405 \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut} |
402 x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0 \label{all-solut} |
406 x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0 \label{all-solut} |
403 \end{eqnarray} |
407 \end{eqnarray} |
404 where (\ref{all-solut}) ensures that $S$ contains {\em all} solutions of the equation. The \sisac-project has implemented a prototype of an equation solver~\footnote{See \textit{equations} in the hierarchy of specifications at http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}. |
408 where (\ref{all-solut}) ensures that $S$ contains {\em all} solutions of the equation. The \sisac{}-project has implemented a prototype of an equation solver~\footnote{See \textit{equations} in the hierarchy of specifications at http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index\_pbl.html}. |
405 |
409 |
406 There is demand for fullfledged equation solving in CTP, including equational systems and differential equations, because \sisac{} has a prototype of a CTP-based programming language calling CAS functions; and Lucas-Interpretation \cite{wn:lucas-interp-12} makes these functions accessible by single-stepping and ``next step guidance'', which would automatically generate a learning system for equation solving. |
410 There is demand for fullfledged equation solving in CTP, including equational systems and differential equations, because \sisac{}{} has a prototype of a CTP-based programming language calling CAS functions; and Lucas-Interpretation \cite{wn:lucas-interp-12} makes these functions accessible by single-stepping and ``next step guidance'', which would automatically generate a learning system for equation solving. |
|
411 |
|
412 \subsection{Algorithms for cancellation of multivariate polynomials} |
|
413 The most appropriate book for implementing the required algorithms in this thesis is \cite{Winkler:96}. TODO.WN111104 welche noch ? |
407 |
414 |
408 \section{Thesis structure} |
415 \section{Thesis structure} |
409 The proposed table of contents of the thesis on the chapter level is as follows: |
416 The proposed table of contents of the thesis on the chapter level is as follows: |
410 \begin{enumerate} |
417 \begin{enumerate} |
411 \item Introduction (2-3 pages) |
418 \item Introduction (2-3 pages) |
412 \item Computer Algebra Systems (CAS) (5 - 7 pages)\\ |
419 \item Computer Algebra Systems (CAS) (5 - 7 pages)\\ |
413 Which different CAS exists and whats the focus of them. |
420 Which different CAS exists and whats the focus of them. |
414 \item The \sisac-Project (5 - 7 pages)\\ |
421 \item The \sisac{}-Project (5 - 7 pages)\\ |
415 This chapter will describe the \sisac-Project and the goals of the project. |
422 This chapter will describe the \sisac{}-Project and the goals of the project. |
416 \item Univariate Polynomials (15-20 pages)\\ |
423 \item Univariate Polynomials (15-20 pages)\\ |
417 This chapter will describe different Algorithms for univariate polynomials, with different coefficients. |
424 This chapter will describe different Algorithms for univariate polynomials, with different coefficients. |
418 \item Multivariate Polynomials (20-25 pages)\\ |
425 \item Multivariate Polynomials (20-25 pages)\\ |
419 This chapter will describe different Algorithms for multivariate polynomials, with different coefficients |
426 This chapter will describe different Algorithms for multivariate polynomials, with different coefficients |
420 \item Functional programming and SML(2-5 pages)\\ |
427 \item Functional programming and SML(2-5 pages)\\ |
421 The basic idea of this programming languages. |
428 The basic idea of this programming languages. |
422 \item Implimentation in \sisac-Project (15-20 pages) |
429 \item Implimentation in \sisac{}-Project (15-20 pages) |
423 \item Conclusion (2-3 pages) |
430 \item Conclusion (2-3 pages) |
424 \end{enumerate} |
431 \end{enumerate} |
425 %\newpage |
432 %\newpage |
426 |
433 |
427 \section{Timeline} |
434 \section{Timeline} |