\chapter{The example for reference}\label{AK:APP:exref}\label{use-expl}

This example intended to illustrate interaction with \isac{} is quoted from \cite{wn:matheng99}.

\sisac{} features a new kind of calculations in applied mathematics, and it is an issue to make the novel functionality of this software as clear as possible. In order to meet this issue, an example is given to be referenced by the use-cases within this document. The example is taken from a calculus course at highschools; thus it should not pose problems to understand the underlying mathematics. Nevertheless the example covers all major features offered by \sisac.

\section{Description, formalization and modeling phase}

The {\bf description} of an {\bf example}\footnote{These {\bf terms} are defined in the appendix of \cite{isac:appendices} 'List of Terms used in the \sisac-project'} may consist of text, formulas and figures:

\begin{center}\begin{minipage}{4.2in}\it 

Given a circle with radius $r=7$, inscribe a rectangle with

length~u and width~v. Determine u and v such that the rectangles area~A is a maximum.

\end{minipage}\end{center}

\begin{figure} [htb]

\centerline{\includegraphics[width=5.0cm]{fig/coil-kernel-uv}}

\caption{Figure for the maximum example}

\label{fig.coil-kernel-uv}

\end{figure}

The inital step in solving such an example is, to construct a {\bf model} from the description. The respective model looks like this, if all items are input:\label{model}

\begin{tabbing}

1234,\=relate \=: \= \=\kill

%\>Problem [maximum, calculus, optimization] \\

\>given\>: $[$ Constants $\;$ \framebox{$r=7$} $]$\\

\>where    \>: $\,0\leq 7$ \\

\>find X \>: $[$ Maximum $\;$\framebox{$A$},\\

\>       \>\>AdditionalValues $\;$\framebox{$[u,v]$} $]$\\

\>with  \>:{\tiny  $\;A=2uv-u^2 \;\land\; (\frac{u}{2})^2+(\frac{v}{2})^2=r^2 \;\land$} \\

\>\>\>{\tiny $\;\forall \;A^\prime\; u^\prime \;v^\prime.\;A^\prime=2u^\prime v^\prime-(u^\prime)^2 \land

(\frac{u^\prime}{2})^2+(\frac{v^\prime}{2})^2=r^2 $\\

\`$\Longrightarrow A^\prime \leq A$} \\

\>relate\>: $[$ \framebox{$A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2$} $]$

\end{tabbing}

The boxes mark the items meant for input by the user, whereas the surrounding information is provided by the system and serves user guidance. If the model is perfect, \sisac{} can solve the example autonomously.

In order to provide userguidance already in the model phase, each example is accompanied by a {\bf formalization} prepared by an author and normally hidden from the user:

{\it

\begin{tabbing}

1234,\=$F_{III}$\=$\equiv\;\;(\;$\=\kill

\>$F_I$\>$\equiv\;\;(\;$\>$\{r=7\},\;\; \{ A,[u,v]\},\;\;$\\

\>\>\>$\{0\leq\frac{u}{2}\leq r,\;\; 

   \{A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\}\;)$\\

\\

\>$F_{II}$\>$\equiv\;\;(\;\{r=7\},\;\; \{ A,[u,v]\},\;\;$\\

\>\>\>$\{0\leq\frac{v}{2}\leq r,\;\; 

   \{A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2\}\;)$\\

\\

\>$F_{III}$            

\>$\equiv\;\;(\;\{r=7\},\;\; \{ A,[u,v]\},\;\;$\\

\>\>\>$\{0\leq\alpha\leq\frac{\pi}{2},\;

   \{A=2uv-u^2,\frac{u}{2}=r\sin\alpha,\frac{v}{2}=r\cos\alpha\})$

\end{tabbing}}

In this case the formalization comprises three variants, $F_I, F_{II}, F_{III}$, which presumerably cover all possibilities students would consider in a particular course. All of such formalizations for {\em one} example together are called 'formalization' in the sequel.

Given such a formalization and a specification (see below) , \sisac{} can solve an example autonomously {\em and} in stepwise interaction down to the result.

\\

If \sisac{} is being used to solve an example unknown to the system (i.e. without a hidden specification and formalization prepared by an author) \sisac{} cannot provide user guidance at the beginning of this phase (see \ref{START:from_scratch}). In particular, the items {\it Constants}, {\it Maximum} and {\it AdditionalValues} have to be found in the theory {\it Descript.thy}.

\section{Knowledgebase and specification phase}

The knowledge base comprises three parts, theories, problems and methods.

\paragraph{Theories} contain the knowledge deduced from axioms and definitions by formal proof (done by the interactive theorem prover Isabelle). For the example at hand knowledge is prepared like the following:

\begin{verbatim}

   theory 'calculus'

   consts

     d_d         :: "[real, real]=> real"

   rules         

     diff_sum    "d_d bdv (u + v) = d_d bdv u + d_d bdv v"

     diff_prod   "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"

     diff_quot   "Not (v = 0)     ==> (d_d bdv (u / v) =

                        (d_d bdv u * v - u * d_d bdv v) / v ^ 2)"

     ...

\end{verbatim}

\paragraph{Problems} capture the aspect of application of knowledge.

{\it\begin{tabbing}

123\=4512345\=\=4512345\kill

\>\> $|$\\

\>\> \nod e\=quation \\

\>\> $|$\>\nod u\=nivariate\\

\>\> $|$\>$|$   \>\nod linear \\

\>\> $|$\>$|$   \>\nod p\=olynomial \\

\>\> $|$\>$|$   \>\nod rational\\

\>\> $|$\>$|$   \>\nod \dots\\

\>\> \nod function \\

\>\> $|$\>\nod make \\

\>\> $|$\>      \>\nod by\_elimination \\

\>\> $|$\>      \>\nod by\_new\_variable \\

\>\> $|$\>\nod differentiate \\

\>\> $|$\>$|$   \>\nod for\_maximum \\

\>\> $|$\>$|$   \>$|$  \>\nod on\_interval\\

\>\> $|$\>$|$   \>\nod \dots \\

\>\> $|$\>\nod integrate \\

\>\> $|$\>      \>\nod \dots \\

\>\> \nod optimization \\

\>\> $|$\>\nod linear \\

\>\> $|$\>$|$   \>\nod \dots \\

\>\> $|$\>\nod calculus \\

\>\> $|$\>      \>\nod maximum \\

\>\> $|$\>      \>$|$  \dots \\

\end{tabbing}}

The example at hand shall be described by the {\it problem [calculus, optimization]} (note the reverse order w.r.t. the hierarchy above, which seems more usual in many cases, e.g. {\it [linear, univariate, equation]}), and will be broken down into the subproblems {\it [make, function]}, {\it [on\_interval, for\_maximum, differentiate, function]} and {\it [tool, find\_values]}. The root-problem of the example looks like

{\it 

\begin{tabbing}

1234,\=relate \=: $\equiv$\= ${\it let}\:$ \=$\exists m\_$\kill

\>Solve\_problem [maximum, calculus, optimization] \\

\>given\>: $[$ Constants fix\_ $]$\\

\>where    \>: ${\it map}\;(\$\,0\leq\,\$)\; {\it fix\_}$ \\

\>find  \>: $[$ Maximum m\_\\

\>       \>\>AdditionalValues vs\_ $]$\\

\>with  \>: ${\it let}\:x_1 = \{{\it m\_}\}\cup\{{\it vs\_}\}\cup({\it Vars}\:{\it rs\_});$\\

\>\>\>\>$x_2 = {\it map}\:{\it primed}\:x_1;$\\

\>\>\>$\:{\it in}\;\,{\it map}\:({\it op}\land)\:{\it rs\_}\:\$\: \land\:\$$ \\

\>\>\>\>$\forall\,\$\,x_2\,\$.\,(\,\lambda\,\$\,x_1\,\$\,.\,\$\,{\it map}\,({\it op}\land)\,{\it rs\_}\,\$\,)\,\$\,x_2\,\$\, $ \\

\>relate\>: rs\_

\end{tabbing}}

This problem is {\bf matched} with the formalization and yields the model shown above.

\paragraph{Methods} describe the algorithms solving the problems. The method solving the example calls the subproblems mentioned:

{\it\begin{tabbing}

123\=123\=123\=123\=123\=123\=\kill

\>  {\tt Script} Maximum\_value (fix\_::bool list) (m\_::real) (rs\_::bool list)     \\

\>\>\>\>\>         (v\_::real) (itv\_::real set) (err\_::bool) =                       \\

\>\>     ({\tt let}\\

\>\>\>        e\_ = (hd o (filter (Testvar m\_))) rs\_;                        \\

\>\>\>        t\_ = ({\tt if} \#1 $<$ Length rs\_                                        \\

\>\>\>\>                {\tt then} (Subproblem (Reals,[make, funtion],no\_met) [m\_, v\_, rs\_]) \\

\>\>\>\>                {\tt else} (hd rs\_));                                         \\

\>\>\>        mx\_ = Subproblem (Reals,[on\_interval, for\_maximum, differentiate, \\

\>\>\>\>\>                 function], maximum\_on\_interval) [ t\_, v\_, itv\_ ]   \\

\>\>      {\tt in} (Subproblem (Reals,[tool,find\_values],find\_values)               \\

\>\>\>\>\>              [ mx\_, (Rhs t\_), v\_, m\_, (dropWhile (ident e\_), rs\_])))\\

\end{tabbing}}

An example is given a {\bf specification} ('it is specified') by three pointers into each of the three parts of the knowledge base, i.e. a pointer to a theory, to a problem and to a method. For the example this is {\it (Differentiate, [calculus, optimization], Maximum\_value)}. 

\section{Interaction on the worksheet and the browsers}

Within a calculation the centre of interaction with the user is a so-called {\bf worksheet}. At certain points the user may want to view the knowledge base in a so-called {\bf browser-window} and/or select some knowledge, or the dialog presents such a window.

\paragraph{In the modeling phase} the user inputs formulas on the worksheet, and on the worksheet they get most of the feedback. After a while the worksheet could look like this:

{\it

\begin{tabbing}

123\=123\=123\=relate...\=123\=\kill

\>Solve\_problem [maximum, calculus, optimization] \\

\>\>Model\\

\>\>\>given: \>$[$ Constants $r=7\;]$\\

\>\>\>where: \>$\,0\leq r$\\

\>\>\>find:  \>$[$ Maximum, AdditionalValues $[u,v]\;]$\\

\>\>\>relate:\>$[A=2uv,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\;\frac{u}{2}=r\sin{\alpha}\;]$

\end{tabbing}}

where {\it Solve\_problem [maximum, calculus, optimization]}, {\it Constants}, {\it Maximum}, {\it AdditionalValues}, and $0\leq r$ have been supplied by the system, and several items are marked: {\it Maximum} with 'missing', $A=2uv$ with 'incorrect', and $\frac{u}{2}=r\sin{\alpha}$ with 'superfluous'. Regarding this kind of feedback\label{model-feedback} users may successfully complete modeling; if they are not capable to do it, they just hit a 'go-on' button and \sisac{} gets the correct model from the hidden formalization and specification. For the following let us assume, that the model is completed correctly:

{\it

\begin{tabbing}

123\=123\=123\=relate...\=123\=\kill

\>Solve\_problem [maximum, calculus, optimization] \\

\>\>Model\\

\>\>\>given: \>$[$ Constants $r=7]$\\

\>\>\>where: \>$\,0\leq r$\\

\>\>\>find:  \>$[$ Maximum , AdditionalValues $[u,v]\;]$\\

\>\>\>relate:\>$[A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\frac{u}{2}=r\sin{\alpha}]$\\

\>\>Specification\\

\>\>\>Theory: \>\>%Reals

\\

\>\>\>Problem:\>\>%[maximum, calculus, optimization]

\\

\>\>\>Method: \>\>%[make\_fun, by\_elimination]

\end{tabbing}}

The superfluous item $\frac{u}{2}=r\sin{\alpha}$ does not matter, below there are the {\bf specification-fields} to be determined (i.e. input by the user) within the specification phase.

\paragraph{The specification phase} requires data from the knowledge base in general. In the case of the examples model above the decision is required, which kind of problem the given model can be matched with: {\it[linear, optimization]}, or {\it[calculus, optimization]}, or some other problem. The information necessary for this decision can be found in the hierarchy of problems.

Learners can {\bf browse} the hierarchy of problems (theories, methods) and they can {\bf apply} the problem (theory, method); the latter transfers the problem (theory, method) to the respective field below the model on the worksheet.

For instance, applying the problem {\it[linear, optimization]} would cause this display on the worksheet:

{\it

\begin{tabbing}

123\=123\=123\=relate...\=123\=\kill

\>Solve\_problem [maximum, calculus, optimization] \\

\>\>Model\\

\>\>\>given: \>$[$\underline{Constants $r=7$}$]$\\

\>\>\>where: \>$\,0\leq r$\\

\>\>\>find:  \>$[$Maximum , \underline{AdditionalValues $[u,v]$}$]$\\

\>\>\>relate:\>$[\underline{A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\frac{u}{2}=r\sin{\alpha}}]$\\

\>\>Specification\\

\>\>\>Theory:\\

\>\>\>Problem:\>\> [linear, optimization]\\

\>\>\>Method:

\end{tabbing}}

\noindent where some items in the model would be marked with some\underline{ error-feedback}. For instance, applying a theory even might cause the feedback 'syntax-error' when the model contains function constants not defined in the theory or in one of the theories parents.

Browsing problems (when started from a model on the worksheet) matches the problem selected with the model on the worksheet, i.e. on the browser-window the same feedbacks are given as for the model on the worksheet described on p.\pageref{model-feedback}.

\section{The solving phase and subproblems}

Before we describe \sisac s features for the solving phase, we fix one correct model and one specification (out of several possible ones) as follows:

{\it

\begin{tabbing}

123\=123\=123\=relate...\=123\=\kill

\>Solve\_problem [maximum, calculus, optimization] \\

\>\>Model\\

\>\>\>given: \>$[$Constants $r=7]$\\

\>\>\>where: \>$\,0\leq r$\\

\>\>\>find:  \>$[$Maximum $A$, AdditionalValues $[u,v]]$\\

\>\>\>relate:\>$[A=2uv-u^2,\;(\frac{u}{2})^2+(\frac{v}{2})^2=r^2,\frac{u}{2}=r\sin{\alpha}]$\\

\>\>Specification\\

\>\>\>Theory: \>\>Reals\\

\>\>\>Problem:\>\>[maximum, calculus, optimization]\\

\>\>\>Method: \>\>[make\_fun, by\_elimination]

\end{tabbing}}

The following worksheet shows the whole calculation without the respective models and specifications; this short-presentation could stem from an interaction, where the user is merely interested in the result and let the system calculate autonomously:

{\it\small 

\begin{tabbing}

1234\=123\=123\=123\=123\=123\=123\=123\=123\=\kill

\>Solve\_problem [maximum, calculus, optimization] \\

\>\>1.\>SubProblem (DiffAppl, [make, function]) \\

\>\>\>1.\>${\it solve\_univariate}\;\left(\left(\frac{u}{2}\right)^2+\left(\frac{v}{2}\right)^2=r^2\right)\;u$\\

\>\>\>1'.\>$L = \left[u=2\sqrt{r^2-\left(\frac{v}{2}\right)^2},\;u=-2\sqrt{r^2-\left(\frac{v}{2}\right)^2}\right]$\\

\>\>\>2.\>$L_1= \left[u=2\sqrt{r^2-\left(\frac{v}{2}\right)^2}\right]$\\

\>\>1'.\>$A_1= 2\cdot 2\sqrt{r^2-\left(\frac{v}{2}\right)^2}\cdot v - v^2$\\

\>\>2.\>SubProblem (DiffAppl, [on\_interval, for\_maximum, differentiate, function])\\

\>\>\>1.\>$\frac{d}{dv}\left( 2\cdot 2\sqrt{r^2-\left(\frac{v}{2}\right)^2}\cdot v - v^2 \right)=$\\

\>\>\>1'.\>$A_1^\prime = 2\sqrt{r^2-\left(\frac{v}{2}\right)^2} - \frac{v^2}{2\sqrt{r^2-\left(\frac{v}{2}\right)^2}} - 2v$\\

\>\>\>2.\>${\it solve\_univariate}\;\left(2\sqrt{r^2-\left(\frac{v}{2}\right)^2} - \frac{v^2}{2\sqrt{r^2-\left(\frac{v}{2}\right)^2}} - 2v =0\right)\;v$\\

\>\>\>2'.\>$L = [v=234.567]$\\

\>\>3.\>SubProblem (DiffAppl, [find\_values, tool])\\

\>\>3'.\>$[u=123.456, v=234.567]$\\

\>$[u=123.456, v=234.567]$

\end{tabbing}}