ISAC system

Introduction to ISAC

This introduction is a copy from the ISAC webpages.

The ISAC-project is an initiative at Graz University of Technology, started in 2002 and presently pursued at the Institute for Software Technology and the Institute for Information Systems and Computer Media.

The ISAC-system is an experimental software assembling open source components with as little glue code as possible. The system serves for demonstration of a novel kind of transparent single-stepping software for applied mathematics --- experimenting with concepts and technologies from computer mathematics (theorem proving, symbolic computation, model based reasoning etc) and e-learning (knowledge space theory, computer-supported collaboration, usability engineering etc).

Architecture of ISAC

From the beginning the tutoring system has been based on the theorem prover Isabelle:

ISAC's interpreter uses Isabelle's theory management, matching, parsing, pretty printing and of other functionality. A script provides the interpreter with knowledge of how to guide the learner towards the solution of a given problem. The interaction with the learner is accomplished via a 'worksheet' implemented in JavaSwing. The dialog component inbetween the GUI and the interpreter is not shown in the figure.

Presently ISAC is being stepwise integrated into Isabelle:

The communication between editor and ISAC's interpreter will rely on Isar's scala layer and the upcoming document model . The editor, jEdit, will take over the the functionality of the 'worksheet' in a plug-in parallel to the upcoming Isar/jEdit front-end. The interpreter will rely on Isar's contexts , which provide the logical environment at each step of problem solving, such that a step input by the user can be proven consistent with the current context.

jEdit is written in JavaSwing, and also several DGSs are written in JavaSwing; so it seems straight forward to combine the respective GUIs to unified front-ends for a mathematics engine integrating proof, construction and calculation.

Features of the tutoring system

The performance of ISAC as tutoring system is determined by the dialog component finally, which is under construction at IICM . Strengths of CTP for tutoring has not yet been acknowledged ; here this part is dropped and the underlying functionality of ISAC's knowledge interpreter is emphasized, which relies on Isabelle as a 'logical operating system'.

The following three points summarise the functionality provided by the interpreter:

• Check user input as generous and liberal as possible: Given a certain problem of applied mathematics (including geometric constructions!) by a formal specification, which initialises a context (in the sense of Isabelle/Isar) --- then input by the learner (=user) creates a proof situation for ATP : prove the input as a lemma derivable from the current context (in algebra) or prove the context created by the input equivalent to the current context (in geometry), see below.

• Guide the user step by step towards a solution: If the learner (=user) gets stuck, the system is capable to suggest the next step. This functionality is accomplished by the Lucas-interpreter : a program (called script in the figures above) is interpreted in the way a debugger works in single stepping mode; the breakpoints (i.e. steps) are defined as specific statements in the program, which inevitably contribute to the progress of the calculation or construction; at the breakpoints the learner is free to choose the next step as described in the previous point. The challenge for the Lucas-interpreter is to resume after arbitrary user-input, see below.

• Explain steps on request by the user: This challenge seems acchievable with respect to human-readable ITP-knowledge : Since all the knowledge is mechanised (theories, problems, methods), interlinking of knowledge items is no technical problem. However, the issues is a pedagogical one: how to filter the abundant wealth of knowledge and how to personalise access.

The core: Lucas-Interpretation

The concept of a Lucas-Interpreter (LucIn) presupposes a kind of program language , which combines computation and deduction in a specific way.

The program language is a functional language with additional features: it presupposes a formal specification of a program and uses the specification to initialise a context in the sense of Isabelle/Isar . At each step of computation the context is updated with partiality conditions and other logical data. The contexts provide provers with data required to handle user input at some step. See the example below.

User input, however, is shifted from the program language to the interpreter of the language: Being strictly functional the language has no statements for input and output. But the interpreter works like a debugger stepping from breakpoint to breakpoint. At the breakpoints control is handed over to a dialog module. Such an experimental dialog module is under construction at TUG, IICM . The interface between LucIn and dialog is surprisingly simple .

The breakpoints for the LucIn are tactics which indispensably contribute to the progress of a calculation (or a construction in geometry). So, tactics are the statements in the program language, which produce output and which also allow for input.

Let us give an example, already from the domain of geometry, but still handled without specific knowledge about geometry.

Example: construct the circumcenter of a triangle

The program constructs the center O of the circumcircle of a triangle A B C. The program takes all four points as formal arguments, which have names as actual values determined in the preceeding specification phase; the program could look like as follows:

 1  Program circumcenter A B C O =
 2    let (P_1, P_2) = Take \epsilon (Q_1, Q_2). Q_1 \in {A,B,C} \land
 3     	       	      	   	    	  	Q_2 \in {A,B,C} \land not Q_1 = Q_2
 4	 m_1 = Subproblem (Triangles, [geom, euclid, plane, median],
 5	       		  	      [geom, euclid, plane, 2circ]) P_1 P_2 m_1
 6	(P_3, P_4) = Take \epsilon (Q_1, Q_2). Q_1 \in {A,B,C} - {P_1,P_2} \land
 7     	       	      	   	    	  	Q_2 \in {A,B,C} \land not Q_1 = Q_2
 8	 m_2 = Subproblem (Triangles, [geom, euclid, plane, median],
 9	       		  	      [geom, euclid, plane, 2circ]) P_3 P_4 m_2
10    in O = Take \epsion O. m_1 \cap m_2

Here the tactics are Take and Subproblem, and these tactics either mark some of the given points A, B, C or produce and output a new geometric object: In lines

• 2-3 Take marks 2 different points P_1 P_2 selected from the set {A,B,C}.
• 4-5 Subproblem creates the perpendicular bisector m_1 of the selected points; how m_1 is created is left to the Subproblem. Subproblems carry in deduction, see below
• 6-7 select another pair of points (P_3, P_4)
• 8-9 create a second perpendicular bisector m_2 from (P_3, P_4)
• 10 intersects m_1 and m_2 yielding the circumcenter O, which is output as final result.

Specification of the example

Before interpretation of a program by a LucIn is started, a formal specification has to be completed. The specification of the current example could look like:

Text: Given a triangle by the points A, B, C in a plane, construct the circumcenter O of the triangle.

Formal specification:

• given : <math>\mathit{point}\; A,\; \mathit{point}\; B,\; \mathit{point}\; C</math>
• precondition : <math>\neg {\it collinear}\; A\; B\; C</math>
• find : <math>\mathit{point}\; O\;</math>
• postcondition : <math>\overline{OA} = \overline{OB} \;\land\; \overline{OB} = \overline{OC} \;\land\; \overline{OC} = \overline{OA}</math>

Specifications also come with subprograms, see the Subproblems in the above program. These both could be accompanied by the following specification:

• given : <math>point P, point Q </math>
• precondition : <math>P\not= Q </math>
• find : <math>line m </math>
• postcondition : <math>m = \{X.\;\overline{XP}=\overline{XQ}\} </math>

Subproblems combine computation and deduction

Subproblems are the most evident point where the combination of computation and deduction come to bear. Let us recall the example program:

4	 m_1 = Subproblem (Triangles, [geom, euclid, plane, median],
5	       		  	      [geom, euclid, plane, 2circ]) P_1 P_2 m_1

We see, Subproblems have two kinds of arguments:

1. a triple referencing mathematics knowledge, in partcular the references
   1. Triangles to a theory containing respective axioms, definitions, theorems and proofs
   2. [geom, euclid, plane, median] to a specification(-pattern: in the same way a program takes formal arguments, the specification of the program contains formal arguments to be instatiated by the actual arguments of the program; so we might call this a specification-pattern.
   3. [geom, euclid, plane, 2circ] to a method solving the specified problem; the (instantiated) specification acts as a guard for the method.
2. the formal arguments of the program

In the subsequent section we see, how preconditions and postconditions of Subproblems are handled by a LucIn during interpretation of the example program.

Contexts combine computation and deduction

Contexts in the sense of Isabelle/Isar combine an environment, pairing identifiers with respective values, and logical data. Let us pursue the growth of the context in our running example, <math>\mathit{ctxt\_i} = \mathit{env\_i} \cup \mathit{pred\_i}</math>:

 1  Program circumcenter A B C O =

<math>\mathit{env\_0} = \{(A,X), \;(B,Y), \;(C,Z), \;(O,M)\} </math> ... from the specification

<math>\mathit{pred\_0} = \{\neg \mathit{collinear}\;X\;Y\;Z\} </math> ... from the specification's precondition

 2    let (P_1, P_2) = Take \epsilon (Q_1, Q_2). Q_1 \in {A,B,C} \land
 3     	       	      	   	    	  	Q_2 \in {A,B,C} \land not Q_1 = Q_2

<math>\mathit{env\_1} = \mathit{env\_0}\cup\{(P_1,X),\;(P_2,Y) \} </math> ... the choice of <math>\epsilon</math>

<math>\mathit{pred\_1} = \mathit{pred\_0}\cup\{X\not= Y \} </math> ... deduced from <math>\neg \mathit{collinear}\;X\;Y\;Z</math>, required as precondition for subsequent Subproblem

 4	 m_1 = Subproblem (Triangles, [geom, euclid, plane, median],
 5	       		  	      [geom, euclid, plane, 2circ]) P_1 P_2 m_1

<math>\mathit{env\_2} = \mathit{env\_1}\cup\{(m_1, perpendBisector(X,Y))\} </math>

<math>\mathit{pred\_2} = \mathit{pred\_1}\cup\{ \{P.\;\overline{PX}=\overline{PY}\} \} </math> ... the postcondition of the previous Subproblem

 6	(P_3, P_4) = Take \epsilon (Q_1, Q_2). Q_1 \in {A,B,C} - {P_1,P_2} \land
 7     	       	      	   	    	  	Q_2 \in {A,B,C} \land not Q_1 = Q_2

<math>\mathit{env\_3} = \mathit{env\_2}\cup\{(P_3,Y),\;(P_4,Z) \} </math> ... the choice of <math>\epsilon</math>

<math>\mathit{pred\_3} = \mathit{pred\_2}cup\{Y\not= Z\} </math> ... deduced from <math>\neg \mathit{collinear}\;X\;Y\;Z</math>, required as precondition for subsequent Subproblem

 8	 m_2 = Subproblem (Triangles, [geom, euclid, plane, median],
 9	       		  	      [geom, euclid, plane, 2circ]) P_3 P_4 m_2

<math>\mathit{env\_4} = \mathit{env\_3}\cup\{(m_2, perpendBisector(Y,Z))\} </math>

<math>\mathit{pred\_4} = \mathit{pred\_3}\cup\{ \{P.\;\overline{PY}=\overline{PZ}\}, \neg(m_1\ || m_2) \} </math> ... the latter deduced from <math>\neg \mathit{collinear}\;X\;Y\;Z</math>

10    in O = Take \epsion O. m_1 \cap m_2

<math>\mathit{env\_5} = \mathit{env\_4}\cup\{(M,intersect(m_1,m_2))\} </math>

<math>\mathit{pred\_5} = \mathit{pred\_4}\cup\{\overline{MX} = \overline{MY} \;\land\; \overline{MY} = \overline{MZ} \;\land\; \overline{MZ} = \overline{MX} \} </math> ... deduced from the two postcondition above and transitivity of <math>=</math> .

This sequence shows the growth of a context during execution of a program (lines 1..10), and the interleaving of computation and deduction. Details are up to discussion, in particular the context's elements <math>perpendBisector(Y,Z)</math> and <math>intersect(m_1,m_2)</math> and the remarks '...deduced from'. This discussion is shifted to the appropriate section.

Experiences with ISAC from field tests

The tutoring system has been tested in two field tests. The field tests mark the edges of the range of application planned presently:

1. Several units of introduction to algebra for a class at age of 13 in a 'Hauptschule', i.e. a school for pupils who do not want to attend high-school. The test was supervised and evaluated within the framework of IMST and resulted in this report .

1. Several units under the topic 'bending lines' for a class at age of 19 in a 'HTL', an Austrian type of school at the level of a polytechnic university, within IMST with this final report .