The discipline of Computer Theorem Proving (TP) distinguishes itself by formal rigor in doing mathematics in various application domains [1]. This short paper is, however, not on TP but on educational software based on TP components. Such software promises advantageous features [7] some of which are demonstrated by a prototype [3] called Isac. Isac is based on the TP Isabelle [2] and generates dialogues similar to interaction with chess software: moves in chess are considered as rigorous formal as steps in calculations are when solving problems in engineering disciplines. Isac checks input of students by use of Isabelle's automated provers, which in turn are provided with necessary logical context by Lucas-Interpretation [6]. This interpreter also allows to propose next steps towards a solution, so roles can be arbitrarily switched between student and system. This paper reports work in progress in cooperation with universities of applied sciences in Austria. The work concerns a feasibility study on how Isac could serve in engineering education at these universities. Since Isac has been designed for \pure" mathematics, the study encounters several challenges. Below one running example presents three major challenges for discussion; the example is from [9] and slightly changed for reasons discussed in x2: Given is a system with two oscillating masses, m = 2 kg, connected by linear springs with length l0 = 0:3 m and damped with d = 0:4 Nms as shown in Fig.1. The respective spring constants are c1 = 0:11 Nm and c2 = 0:22 N . The masses are located such that x1 = x2 = 0 with m relaxed springs; initially the masses are dislocated with x1 = x2 = 0:05 m and have velocities v1 = 0:1 ms and v2 = 0:2 ms respectively. The right mass is excited by force F = 0:6 sin (3t) N . Change the given spring constant c2 such that the left mass becomes a vibration absorber for the right one (i.e. make the masses oscillate in opposite directions such that the system shows no vibration to the outside).
A formal speci cation in the sense of [4] makes the input Given and the output Find to a system's model explicit as shown below; it restricts input by a pre-condition Where and relates input with output by a post-condition Relate. The rst subproblem of the running example is formally speci ed as follows: The Problem in line 21 is named such, that a reference into Isac's knowledge base is given 1. The other References addressed by line 2112 point to a theory, which imports language elements like x, and to a method which can create a Solution, are collapsed here (as well as the pre-conditions in Where). The notation M (m) establishes a literal connection between Given and Find; the notation is up to discussion. The post-condition in 21114 comprises an 9 not relevant for engineers and might be omitted.
In interactive construction of a Solution the challenge for students is to relate forces, for instance
And for the task of relating the forces, gures like Fig.2 are used to capture coordinates and forces. Now the
problem with Isac's design is, that such gures capture relations in a precise representation, but this
representation is geometric, not formal | and Isac is designed to work with formulas (which would be clumsy in capturing
geometric structure here), which can be handled by Isabelle's components in the background. So the section's
headline advocates \intutition" as opposed to formal speci cation.
1http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html
{ and these cannot be planned from outside an individual brain; so, a lecture on the behaviour of two oscillating
masses (e.g. [
So, how to cope with these challenges in learning to comprehend abstraction? Good old LATEX provided wide margins for personal notes in papers and textbooks again and again; interactive media can do better nowadays, if they are designed appropriately. And it appears obvious: the more such media cover the process of problem solving, the better. Isac claims to cover the whole process; x1 showed, how problem speci cation is covered by Isac. Below is shown, what else can be done.
Include creation of models into concrete examples as done with the running example: The problem statement on p.1 contains a concrete request for a particular value of c2 (below folded into Specification in order to save space) | nevertheless the Solution should comprise the creation of the underlying abstract model as follows: Since above the modelling process is included into the Solution, students are enabled, not just to advocate some formula from somewhere (which seduces to use formal models without understanding). A student can regard the (sub-)Problems as black-boxes, of course (if not forced by Isac's dialog guide to actively do the step). But Isac is designed to elicit experimentation, for instance to experiment with di erent input values to a problem in order to approximate a solution by trial and error. Since solving the above problem with trials soon turns out hopeless, a student might be motivated to make the sub-Problems white-boxes, look into them, study details and to rework creation of the abstract model.
In the above calculation the concrete result c2 = 1:2345 N was possible, because the Specification contains the concrete values given on p.1, which were input at the beginning of the calculation: . Problem [absorber, 2-mass-oscillator] 1 Specification: 2 Solution: 21 Problem [determine, 2-mass-oscillator, Di Eq] 22 [2x1 + 0:4x_ 1 + 3:3x1 0:22x2 = 0; 2x2 + 0:4x_ 2 0:22x1 + 3:3x2 = 0:6] 23 Problem [solution, 2-mass-oscillator, homogen, Di Eq] 24 [x1(t) = 0:05e 0:1t(cos 0:81t + 3:85 sin 0:81t);
x2(t) = 0:05e 0:1t(cos 0:81t + 3:85 sin 0:81t)] 25 Problem [particular, solution, 2-mass-oscillator, Di Eq] 26 [x1(t) = 0:05e 0:1t0:59 sin 1:69t; x2(t) = 0:05e 0:1t0:59 sin 1:69t] 27 Problem [complete, solution, 2-mass-oscillator, Di Eq] 28 [x1(t) = 0:05e 0:1t(cos 0:81t + 3:85 sin 0:81t 0:59 sin 1:69t);
x2(t) = 0:05e 0:1t(cos 0:81t + 3:85 sin 0:81t + 0:59 sin 1:69t)] Note that above also intermediate results are numeric values (copied from a Mathematica notebook): both representation, symbolic and numeric, have their advantages: the rst tells about the structure of the model, the latter tells about concrete results (which can be observed in dynamic simulation of the enclosed di erential equations, ultimately, see [5]).
Switching between symbolic representation and numeric representation can be done by computer software: this
novel feature seems of utmost importance for learning, so it shall be included to Isac within the next development
phase. Realisation requires to extend Isac's Lucas-Interpreter [
Both design features together, the feature to include models into concrete examples and the feature to switch levels of abstraction, lead to radically new learning scenarios
The student is o ered to review the construction of the abstract model any time (every example concerning,
for instance, the two-mass-oscillator includes the respective model: this is accomplished by copy& past for
some sub-problems in the respective program [
The student is not bothered by unwanted details: he or she can skip in a calculation whatever steps they
want to (if the dialog [
This way questions like \What for do we learn this method" are anticipated in an unobtrusive way. 3
22 m 0 Above the numbers at the left do not belong to an Isac calculation, they are for referencing only. In the middle there are the formulas of the calculation (with tree-like indentation). On the right there are the justi cations for the formulas.
In the lines 2127 and 2129 above there are tactics which contribute to formal deduction in the Solution. But the lines 2121, 2123 and 2125 do not contribute to the formal semantics, they are arguments addressing intuitive understanding of physical aspects of modelling. In line 212b there is even a non-physical argument, useful just for structuring the calculation.
The two latter kinds of arguments are not contained in Isac's original design. But now requirements analysis
suggests to extend Isac's programming language with an additional tactic for textual arguments; this extension
seems simple. For details, how Isac guides the student during step-wise construction of a calculation and how
this guidance is generated automatically, see [
The paper demonstrated examples from mechanics in order to show, that Isac's original design is appropriate for education also in engineering disciplines. Requirements analysis in cooperation with experts in engineering education identi ed additional requirements, which appear realizable with reasonable e ort due to TP's power. In particular, Isac as a prototype for TP-based educational systems seems ready for the following three extensions, which have been introduced in x1, x2 and x3 respectively: 1. An interactive graphics-component for input of coordinates, arrows and associated identi ers at certain positions in a gure, while correctness is checked by use of hidden \formalisations" already present in Isac | this shall support geometric intuition in creating physical models. 2. Extension of Isac's Lucas-Interpreter such that the interpreter's environment not only takes identi er-value pairs, but associates identi ers with lists of values (symbolic and numeric) | this shall support comprehending abstract models by switching levels of abstraction. 3. An additional tactic, which plays no role in formal deduction in a calculation, but displays informal arguments for certain steps of calculation | this shall support additional arguments for intuitive understanding. As soon as these features are implemented, Isac can be considered a \system that explains itself" also for mathematics applied to various engineering disciplines | a system which promises to establish novel learning scenarios in the eld.
Several experts from the Universities of Applied Sciences in Wels, Hagenberg and Salzburg are involved in the current requirements engineering: Stephan Dreiseitl, Gunther Eibl, Klaus Schiefermayr, Wolfgang Steiner and Stefan Sunzenauer. The author owes these persons a great debt of gratitude for their precious time spent and the novel ideas contributed to the design of Isac and to this paper.
There was no time asking the mentioned experts to review the paper at hand; so any aws and mistakes in the paper are in full responsibility of the author. [1] Archive of Formal Proofs. http://afp.sourceforge.net. [2] Generic proof assistant \Isabelle". http://isabelle.in.tum.de/. [3] Isac-project. http://www.ist.tugraz.at/isac/History. [4] Dines Bj rner (2006): Software Engineering. Texts in Theoretical Computer Science 1,2,3, Springer, Berlin,
Heidelberg. [5] Sarah Lichtblau: Motion of Two Masses Connected by Springs. http://demonstrations.wolfram.com/
MotionOfTwoMassesConnectedBySprings/. Wolfram Demonstrations Project.