1 (* this is evaluated BEFORE Test_Isac.thu opens structures*)
3 theory T3_MathEngine imports Isac begin
5 chapter {* ISACs mathematics engine *}
6 text {* This is a brief introduction to ISACs mathematics engine (ME). The
7 goal of the introduction is enabling authors to test new developments of
9 As an example we continue the previous one on rewriting. The previous
10 chapter raised questions about didactics and stated open developments problems.
11 So, let us assume, some additional knowledge has been added to solve some of
12 the open problems with '-' in simplification.
13 Now we want to test, if
14 Vereinfache (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)
16 3 - 2 * e + 2 * f + 2 * g
19 section {* Knowledge for automated solving the example problem *}
20 text {* ISAC wants to show possibilities for next steps, if learners get stuck.
21 So, at least ISAC needs to be able to solve a problem automatically. For this
22 purpose, ISAC requires three kinds of knowledge, (1) rules to apply (2) a
23 specification of the problem and (3) a method solving the problem.
25 ad (1) The rules required for simplifying our example are found in theory
26 ~~/Tools/isac/Knowledge/PolyMinus.thy.
28 ad (2) The problem of 'vereinfachen' is one of many other problems;
29 the function 'get_pbt' gets the one we need:
31 ML {* Specify.show_ptyps ();
32 Specify.get_pbt ["plus_minus", "polynom", "vereinfachen"];
34 text {* However, 'get_pbt' shows an internal format; for a human readable format
35 see http://www.ist.tugraz.at/projects/isac/www/kbase/pbl/index_pbl.html
36 Note, that in this tree you first lookup "vereinfachen", then "polynom" and
37 finally "plus_minus", the same as you see from 'show_ptyps ()'.
38 However, we call the problem "plus_minus - polynom - vereinfachen".
40 ad (3) The method solving the problem is also one of many others; the function
41 'get_met' gets the one we need:
45 Specify.get_met ["simplification","for_polynomials","with_minus"];
47 text {* For a readable format of the method look up the definition in
48 ~~/Tools/isac/Knowledge/PolyMinus.thy or
49 http://www.ist.tugraz.at/projects/isac/www/kbase/met/index_met.html
50 The path to the method "simplification - for_polynomials - with_minus" is
51 not reversed like the one to the problem, because the structure of the
52 methods' container is not yet clarified.
55 section {* Testing the example problem *}
56 text {* Now we have all the knowledge ISAC requires for guiding the learner:
57 (1) the theory "PolyMinus", (2) the problem ["plus_minus","polynom","vereinfachen"]
58 and (3) the method ["simplification","for_polynomials","with_minus"].
60 So we can start testing the example by calling 'CalcTreeTEST':
62 ML {* val (p,_,f,nxt,_,pt) =
63 Math_Engine.CalcTreeTEST
64 [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",
66 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
67 ["simplification","for_polynomials","with_minus"]))];
69 text {* The function 'CalcTreeTEST' returns the following values:
70 p: the position in the calculation
71 f: the formula produced by this step of calculation.
72 In this case 'f' is an incomplete model of the problem.
73 nxt: the tactic suggested to do the next step
74 pt: the _whole_ calculation in an internal format; the calculation 'pt'
75 will be fed back into the mathematics engine, the function 'me' below,
76 'me' is purely functional, no further data remains in the memory.
77 'me' returns the same data as 'CalcTreeTEST'.
79 The first tactic suggested by ISAC is 'Model_Problem', we use this tactic
80 (stored in 'nxt') and enter the 'specification phase'.
83 section {* Specifying the example problem *}
84 text {* Often the specification phase is hidden from the learner by the dialog
85 module; here we see the mathematics engine at work directly.
87 Only note the tactic 'nxt' suggested for the next step:
89 ML {* val c = [(*this is an unimportant, but necessary detail*)];
90 val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
91 val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
93 text{* The tactics 'Add_Given' and 'Add_Find' inserted the respective values
94 into the model. Then 'Specify_Theory' determines the knowledge item no.1 from
95 above, 'Specify_Problem' item 2 and 'Specify_Method' item 3.
98 val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
99 val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
100 val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
101 val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt;
103 text{* The final suggestion 'Apply_Method' completes the specification phase
104 and starts the 'solving phase', which is guided by the method determined.
107 section {* Solving the example problem *}
108 text {* Now let us observe, how the method ["simplification","for_polynomials",
109 "with_minus"] guides through simplification by rewriting. For that purpose
110 we increase the 'default_print_depth' (with the disadvantage of extending the output)
111 and print out the results by use of 'f2str'.
112 Please, note only 'nxt' close to the beginning of the output and the resulting
115 ML {* default_print_depth 40; *}
116 ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
117 ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
118 ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
119 ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
120 ML {* default_print_depth 3; *}
121 text{* And, please, note that the result of applying the 'nxt' ruleset is to be
122 found in the output of the next step !
125 section {* Completing the example problem *}
126 text {* The 'nxt' tactic suggested above was 'Check_Postcond'. That means, a
127 perfect mathematics engine has to prove the socalled 'postcondition' of the
128 current problem; this is not yet implemented in the current version of ISAC.
130 ML {* val (p,_,f,nxt,_,pt) = Math_Engine.me nxt p c pt; Math_Engine.f2str f; *}
131 text{* Now the mathematics engine has found the end of the calculation.
133 With 'show_pt' the calculation can be inspected (in a more or less readable
134 format) by clicking the checkbox <Tracing> on top of the <Output> window:
136 ML {* Chead.show_pt pt *}
139 section {* Test further examples *}
140 text{* Now it is easy to do further examples: just put another calculation into
143 ML {* val (p,_,f,nxt,_,pt) =
144 Math_Engine.CalcTreeTEST
145 [(["Term (1 + 2 + 3)", "normalform N"],
146 ("PolyMinus",["plus_minus","polynom","vereinfachen"],
147 ["simplification","for_polynomials","with_minus"]))];
149 ML {* val (p,_,f,nxt,_,pt) =Math_Engine.me nxt p c pt; *}
150 text{* and repeat this ML line as often as required ...*}