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 more and more 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 plut-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 currenct context.
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 [1], [i]; here this part is dropped and the underlying functionality of ISAC's knowledge interpreter 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 by a formal specification, the respective preconditions initialize an Isar context. (The specification can be hiddem from beginners.) The context is enhanced such, that a prover can check the derivability of user-input from the current context. The context is extended step by step of user-input until an object (and a context) has been acchieved, which can be proven to satisfy the specification's post-condition.
- 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 functional 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 a 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.
- Explain steps on request by the user: Lots of knowledge is required for a mechanized math assistant in order to solve a problem: definitions, axioms and theorems (gathered in theories), specification of (classes of) problems (gathered here, for instance) and programs to solve the problems). All this knowledge together is sufficient to generate explanations for each step automatically --- in principle; the knowledge is mechanized in (almost traditional) math notation, but it is an open question how not to overwhelm the learner and how to adapt to his or her level.
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:
- 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.
- 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.
What has ISAC to do with geometry ?
Finally once more the straight answer from the introduction: Presently ISAC has nothing to do with geometry, apart the claim that ISAC is 'a model of mathematics', and the fact that geometry is a part of mathematics.
Thus, showing up in this wiki, is a great challenge to check if ISAC's conception is as general as claimed. Some basic facts have been clarified in a paper; in section TODO we shall address some of the respective open questions.