201 % impact of {\sisac}'s prototype on the issue and others. |
201 % impact of {\sisac}'s prototype on the issue and others. |
202 % |
202 % |
203 |
203 |
204 Traditional course material in engineering disciplines lacks an |
204 Traditional course material in engineering disciplines lacks an |
205 important component, interactive support for step-wise problem |
205 important component, interactive support for step-wise problem |
206 solving. Theorem-Proving (TP) technology can provide such support by |
206 solving. The lack becomes evident by comparing existing course |
|
207 material with the sheets collected from written exams (in case solving |
|
208 engineering problems is {\em not} deteriorated to multiple choice |
|
209 tests) on the topics addressed by the materials. |
|
210 Theorem-Proving (TP) technology can provide such support by |
207 specific services. An important part of such services is called |
211 specific services. An important part of such services is called |
208 ``next-step-guidance'', generated by a specific kind of ``TP-based |
212 ``next-step-guidance'', generated by a specific kind of ``TP-based |
209 programming language''. In the |
213 programming language''. In the |
210 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such |
214 {\sisac}-project~\footnote{http://www.ist.tugraz.at/projects/isac/} such |
211 a language is prototyped in line with~\cite{plmms10} and built upon |
215 a language is prototyped in line with~\cite{plmms10} and built upon |
212 the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002} |
216 the theorem prover Isabelle~\cite{Nipkow-Paulson-Wenzel:2002} |
213 \footnote{http://isabelle.in.tum.de/}. |
217 \footnote{http://isabelle.in.tum.de/}. |
214 The TP services are coordinated by a specific interpreter for the |
218 The TP services are coordinated by a specific interpreter for the |
215 programming language, called |
219 programming language, called |
216 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language and the |
220 Lucas-Interpreter~\cite{wn:lucas-interp-12}. The language |
217 interpreter will be briefly re-introduced in order to make the paper |
221 will be briefly re-introduced in order to make the paper |
218 self-contained. |
222 self-contained. |
219 |
223 |
220 The main part of the paper is an account of first experiences |
224 The main part of the paper is an account of first experiences |
221 with programming in this TP-based language. The experience was gained |
225 with programming in this TP-based language. The experience was gained |
222 in a case study by the author. The author was considered an ideal |
226 in a case study by the author. The author was considered an ideal |
294 %\includegraphics[width=140mm]{fig/isac-Ztrans-math} |
298 %\includegraphics[width=140mm]{fig/isac-Ztrans-math} |
295 \caption{Step-wise problem solving guided by the TP-based program |
299 \caption{Step-wise problem solving guided by the TP-based program |
296 \label{fig-interactive}} |
300 \label{fig-interactive}} |
297 \end{center} |
301 \end{center} |
298 \end{figure} |
302 \end{figure} |
299 If the student gets stuck and does not know the formula to proceed with, |
303 If the student gets stuck and does not know the formula to proceed |
300 there is the button \framebox{NEXT} proceeding to the next step. The |
304 with, there is the button \framebox{NEXT} presenting the next formula |
301 button \framebox{AUTO} immediately delivers the final result in case |
305 on the Worksheet. The button \framebox{AUTO} immediately delivers the |
302 the student is not interested in intermediate steps. |
306 final result in case the student is not interested in intermediate |
|
307 steps. |
303 |
308 |
304 Adaptive dialogue guidance is already under |
309 Adaptive dialogue guidance is already under |
305 construction~\cite{gdaroczy-EP-13} and the two buttons will disappear, |
310 construction~\cite{gdaroczy-EP-13} and the two buttons will disappear, |
306 since their presence is not wanted in many learning scenarios (in |
311 since their presence is not wanted in many learning scenarios (in |
307 particular, {\em not} in written exams). |
312 particular, {\em not} in written exams). |
309 The buttons \framebox{Theories}, \framebox{Problems} and |
314 The buttons \framebox{Theories}, \framebox{Problems} and |
310 \framebox{Methods} are the entry points for interactive lookup of the |
315 \framebox{Methods} are the entry points for interactive lookup of the |
311 underlying knowledge. For instance, pushing \framebox{Theories} in |
316 underlying knowledge. For instance, pushing \framebox{Theories} in |
312 the configuration shown in Fig.\ref{fig-interactive}, pops up a |
317 the configuration shown in Fig.\ref{fig-interactive}, pops up a |
313 ``Theory browser'' displaying the theorem(s) justifying the current |
318 ``Theory browser'' displaying the theorem(s) justifying the current |
314 step. All browsers allow to lookup all other theories, thus |
319 step. The browser allows to lookup all other theories, thus |
315 supporting indepentend investigation of underlying definitions, |
320 supporting indepentend investigation of underlying definitions, |
316 theorems, proofs --- where the HTML representation of the browsers is |
321 theorems, proofs --- where the HTML representation of the browsers is |
317 ready for arbitrary multimedia add-ons. |
322 ready for arbitrary multimedia add-ons. Likewise, the browsers for |
|
323 \framebox{Problems} and \framebox{Methods} support context sensitive |
|
324 as well as interactive access to specifications and programs |
|
325 respectively. |
|
326 |
|
327 There is also a simple web-based representation of knowledge items; |
|
328 the items under consideration in this paper can be looked up as |
|
329 well~\footnote{ |
|
330 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/\textbf{Inverse\_Z\_Transform.html}}~\footnote{ |
|
331 http://www.ist.tugraz.at/projects/isac/www/kbase/thy/\textbf{Partial\_Fractions.html}}. |
318 |
332 |
319 % can be explained by having a look at |
333 % can be explained by having a look at |
320 % Fig.\ref{fig-interactive} which shows the beginning of the interactive |
334 % Fig.\ref{fig-interactive} which shows the beginning of the interactive |
321 % construction of a solution for the problem. This construction is done in the |
335 % construction of a solution for the problem. This construction is done in the |
322 % right window named ``Worksheet''. |
336 % right window named ``Worksheet''. |