Requirements-engineering for educational software [14] raised the question, how much e orts would be required for implementing substantial material from mechanics [16, 17] in a system based on technology from Computer Theorem Proving (TP). The question appears relevant for several kinds of \users": for decision makers, for course designers and last not least for sta from faculties of engineering, who is interested to implement their own examples and exercises in the future. Since TP is new in the eld, there are some general informations about how to implement material in a TP-based system: First there needs to be a so-called \theory" which collects or imports all de nitions used in the material and which formalizes respective theorems and proofs. The system under consideration is Isac [3], a prototype based on the TP Isabelle [2]. Isabelle's standard distribution contains most of the mathematics required, multivariate analysis 1 etc. Further material is in the Archive of Formal Proofs [1]. And what is not yet covered by these sources, can be de ned as axioms preliminarily, see for instance2 . Speci cation of problems is not much e ort, see some prototype implementations3 . The focus of the paper are the methods solving the problems.
An interpreter of a programming language works as sketched in Fig.1 on p.2: The interpreter reads a statement at a certain location in a program; the statement is interpret ed such that the location moves on to another statement to be read next; the interpreter also maintains an environment, which pairs identi ers encountered in statements with respective values; a step of interpretation updates the environment according to the interpreted statement.
A Lucas-Interpreter (LI) extends the above with additional elements and actions: First a step of calculation is constructed by each step of interpretation. Guarantee of correctness for steps in calculations is the purpose of the additional elements; for logical details see [12], here follows a general explanation according to Fig.1:
A theory provides the language elements for certain logical expressions collected in a context [
The scope of environments with respect to programs with nested sub-programs has been clari ed in the
discipline of compiler-construction. However, the scope of contexts in the presence of theories and \locales" is
not yet settled [
The execution of the program's statements is done by rewriting, as usual with functional programs (where one speaks about \evaluation" of \functions" instead of \execution" of \programs" as we do here). In the present state of Isac's prototype there are lots of evaluators: for list-expressions in programs, for normalisation of user input (for checking correctness). for pre-conditions, etc. Compiling these evaluators is an elaborate, expensive and error-prone task. So migration of Isac's programming language to Isabelle's function package [5] shall free the programmer from these tasks. As soon as this integration is done, all the functions available for Isabelle/HOL are ready for LI, including those which implement computer algebra (see for instance [7, 13]).
A program is accompanied by a \guard"; guard and program together are called a \method" in Isac. The
guard is not contained in Fig.1; below an example is copied from [
Guard:
Given: Masses m = 2 kg, Length l0 = 0:3 m, Consts fc1 = 1:1 ks2g ; c2 = 2:2 ks2g g, Damper d = 0:4 Nms Where: 0 < m ^ l0 < 0 Find: Matrixes fM (m); D(d); C(c1; c2)g, Di Eq M x + D x_ + C x = F
Relate: 9x: 8t: t > 0 ) M x + D x_ + C x = F Given in line 11 lists the concrete input items to the program, Find declares the output item(s). Where is the precondition, which shows, that the Guard is a conjunction of predicates restricting input (and restrictions imposed by physical contants could be added here as well). In Relate the post-condition relates input and output (in the sense of [4]); this particular post-condition can be proved by the theory of di erential equations, but it is not immediately useful for an engineer, who wants the solution of an equation and not only some promise by 9. 2
Isac's programming language has been implemented [9] before the \function package" [5] has been introduced to Isabelle. But Isac's language has been designed such, that it anticipated the function package and now the former can be explained in terms of the latter.
Functions in Isabelle/HOL must be total in order to keep the logic consistent. Isac's programs are not total in general, their input is restricted by pre-conditions as shown in x1. Thus Isac's programs are declared as partial function in Isabelle.
A major di erence between Isabelle and Isac concerns the purpose of functions: while the former is built for proving properties of functions, for evaluating them and probably generating e cient code from them, the latter is built for stepwise construction of calculations solving problems in (applied) mathematics. Construction of calculations comprises interactively specifying and solving the respective problem. Below the guard from x1 above is re-used by the Specification (thus not shown again and folded in) for a Problem with a Solution as follows: . partial function di eq 2 mass oscil (m, l 0, [c 1, c 2], d, springs, dampers, sums) = 1 let 11 begin parallel 1101 springs = Take springs \forces of springs" 111 parallel 1111 dampers = Take dampers \forces of dampers" 112 parallel 1121 sums = Take sums \mass times acceleration equals sum of all forces" 12 end parallel 13 di eq = Take sums \" 14 di eq = Substitute [ springs, dampers ] 15 di eq = Rewrite Set normalise 16 di eq = Rewrite Set vectorify \switch to vector representation" 2 in 21 di eq The partial function di eq 2 mass oscil gets the arguments (m, l 0, [c 1, c 2], d, springs, dampers, sums) from the preceeding speci cation phase. The rst lines 2122..2126 of the calculation could have been constructed in arbitrary order; this is re ected by the lines 11..12 in the above function: the statement parallel models parallel execution, while the remaining statements 13..17 represent a sequence.
Above there are speci c statements, called \tactics" in weak analogy to TP: Take, Substitute and Rewrite Set as examples for some dozen others. Tactics are handled by LI like \break points" by debuggers: interpretation halts at the tactics and passes control to the dialog component, which decides how to pass control back to LI, see the next section. 3
As shown in x2 by example, a program in Isac is purely functional as is an Isabelle function, without side-e ects and without input or output. However, LI creates side-e ects in a speci c way and cooperates with a dialogue component. The architectural design is shown in Fig.2. The WorksheetDialog implements the observer pattern [6] and listens to two active components: the Worksheet as interface to the user on the one side and to the MathEngine as interface to LI on the other side; the latter is active in the sense, that response may be delayed due to heavy prover activity:
Here come some details, how automated dialog generation works, by use of the running example: LI starts after successful completion of interactive speci cation, reads line 11 in the function on p.2 and halts at the tactic
In the present state of development the DailogRules are implemented only to an extent which allows demonstration of LI by Isac's prototype. A general machinery [8] is ready to cope with the complexity of interaction expected in the future. Respective \dialog authoring" will be an e cient investment: interactions in doing mathematics are considered independent from various areas of mathematics; also di erences in behaviour of novices versus experts are considered the same in all areas.
The present state of development, the UserModel is still a stub. The stub is designed such, that each student is assigned an indiviual data set, which can be preset as well as updated during a session: error rates on speci c knowledge items (rule, problem, method, example), preferences in interaction and current dialog mode. Three modes are envisaged at least: investigation, exercise, examination (the modes are subsets of DailogRules ).
Relevant in the context of questions about e orts for implementation of interactive TP-based course material is: the implementation of functions is not concerned with interaction at all, a \mathematics author" can focus mathematics and nothing else. 4
In spite of higher complexity of TP-based systems with Lucas-Interpretation as compared with a Computer Algebra System, the implementation of course material does not require more e orts in principle, as soon as Isac's programming languages has migrated to Isabelle's function package. Purely functional programs are speci cally interpreted by so-called Lucas-Interpretation (LI), which generates steps of calculation and respective dialogue guidance as side-e ects of steps in interpretation.
Lucas-Interpretation maintains a context, which provide the most powerful technology available with logical facts for checking correctness of user-input. Thus there is maximal freedom for input { for algorithmic sequences as well as for formula representation: equivalence modulo a theory is checked with maximal reliability. The ability to propose a next step in calculations is the novel feature contributed by Lucas-Interpretation.
No additional e orts are required when programming methods to solve engineering problems: checking steps and proposing steps is done by Lucas-Interpretation automatically and in cooperation with a dialogue module user-guidance is generated automatically.
Finally, after fteen years of conceptual work and of prototyping, a successful proof of concept [
Heidelberg. [5] Lukas Bulwahn, Alexander Krauss, Florian Haftmann, Levent Erkk & John Matthews (2008): Imperative Functional Programming with Isabelle/HOL. In Otmane Mohamed, Csar Muoz & So ne Tahar, editors: Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 5170, Springer Berlin / Heidelberg, pp. 134{149, doi:10.1007/978-3-540-71067-7 14. Available at http://dx.doi.org/10.1007/ 978-3-540-71067-7_14. [6] Ralph Johnson Erich Gamma, Richard Helm & John M.Vlissides (1994): Design Patterns: Elements of
Reusable Object-Oriented Software. Addison-Wesley. [7] Florian Haftmann, Andreas Lochbihler & Wolfgang Schreiner (2014): Towards abstract and executable multivariate polynomials in Isabelle. Isabelle Workshop 2014, http://www.infsec.ethz.ch/people/andreloc/ publications/haftmann14iw.pdf. [8] Markus Kienleitner (2012): Towards \NextStep Userguidance" in a Mechanized Math Assistant. Master's thesis, IICM, Graz University of Technology. Bakkalaureate Thesis. [9] Walther Neuper (2001): Reactive User-Guidance by an Autonomous Engine Doing High-School Math. Ph.D. thesis, IICM - Inst. f. Softwaretechnology, Technical University, A-8010 Graz.
http://www.ist.tugraz.at/projects/isac/publ/wn-diss.ps.gz. [10] Walther Neuper (2006): Angewandte Mathematik und Fachtheorie. Technical Report 357, IMST { Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.
http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte_Mathematik_und_Fachtheorie. [11] Walther Neuper (2007): Angewandte Mathematik und Fachtheorie. Technical Report 683, IMST { Innovationen Machen Schulen Top!, University of Klagenfurt, Institute of Instructional and School Development (IUS), 9010 Klagenfurt, Sterneckstrasse 15.
http://imst.uni-klu.ac.at/imst-wiki/index.php/Angewandte_Mathematik_und_Fachtheorie_2006/2007. [12] Walther Neuper (2012): Automated Generation of User Guidance by Combining Computation and Deduction. pp. 82{101, doi:10.4204/EPTCS.79.5. http://eptcs.web.cse.unsw.edu.au/paper.cgi?THedu11.5. [13] Walther Neuper (2014): GCD | A Case Study on Lucas-Interpretation. In: Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM, Coimbra, Portugal. http://ceur-ws.org/Vol-1186/paper-17.pdf.