equal
deleted
inserted
replaced
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, |
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, |
400 \begin{eqnarray} |
400 \begin{eqnarray} |
401 \exists x_s.\;x_s\in S &\Rightarrow& f(x_s) = 0 \\\label{is-solut} |
401 \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} |
402 x_s\in S &\Leftarrow& \exists x_s.\;f(x_s) = 0 \label{all-solut} |
403 \end{eqnarray} |
403 \end{eqnarray} |
404 \end{eqnarray} |
|
405 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}. |
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}. |
406 |
405 |
407 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. |
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. |
408 |
407 |
409 \section{Thesis structure} |
408 \section{Thesis structure} |
468 % \item |
467 % \item |
469 %\end{enumerate} |
468 %\end{enumerate} |
470 |
469 |
471 \end{document} |
470 \end{document} |
472 |
471 |
|
472 ALLES UNTERHALB \end{document} WIRD VON LATEX NICHT BERUECKSICHTIGT |
473 WN110916 grep-ing through Isabelle code: |
473 WN110916 grep-ing through Isabelle code: |
474 |
474 |
475 neuper@neuper:/usr/local/isabisac/src$ find -name "*umeral*" |
475 neuper@neuper:/usr/local/isabisac/src$ find -name "*umeral*" |
476 ./HOL/ex/Numeral.thy |
476 ./HOL/ex/Numeral.thy |
477 ./HOL/Tools/nat_numeral_simprocs.ML |
477 ./HOL/Tools/nat_numeral_simprocs.ML |