Logging of High-Level Steps in a Mechanized Math Assistant
Franz Kober · 2012
This Baccalaureate Thesis is joint work with [Kie12]the comprehensiveness of the task to reorganise the dialog of ISAC which is under development at TUG. The goal of the reorganisation is to allow non-programmers to adapt learners’ interaction with ISAC; these non-programmers probably will be called “dialog authors” and shall be able to concentrate on cognitive science and educational theories. The challenges expected for dialog authors result from the power of an emerging new generation of educational mathematics assistants ISAC where is a prototype of. These assistants are based on Theorem Proving (TP) technology. TP-based systems are expected to cover the whole range of stepwise solving mathematical problems, to check free user input generously and reliably and to be able to automatically generate a next step. These features raise questions like: Which parts of the next step shall be presented to the learner, the rule to apply or the formula ? Which part of formula or rule should be omitted according to error patterns ? In which situations is the learner allowed to request a next step (not in exams) ? Etc. Implementation work which wants to seriously cope with such questions cannot cope with Java programming at the same time. Such implementation work requires an appropriate development environment for future dialog authors. The two theses together accomplish decisive steps towards such a development environment for dialog authors. The theses review the history and the state-of-the-art in the architecture of dialog-based applications, research a considerable collection of available tools and select two tools for implementation in ISAC. One of the tools is a rule-engine which allows to describe the sequence of interactions by simple rules. The rule-engine is the core of an expert system which is commercially applied in the development of business solutions, but the rule-engine is free. The other tool is a standard relational database which shall serve as a first approach to a user history enabling simple operations on the history. This thesis focuses the second tool, the database. After a careful analysis of the existing dialog architecture and of the implementation in ISAC a UserLogger has been implemented. Both steps, analysis and design as well as implementation are described in detail. The variant found for implementation is very code saving variant and also appropriate for dialog authors: each record in the database is a high-level step of interaction. A step comprises the user (in the multi-user system), the input of the user and the response of the system checking the user input. Such a step is called “high-level” for good reasons: a step promotes the construction of a solution within a logical context (and a user not aware of the context will fail to do such a step). Or such a step concerns a lockup in the underlying mathematics knowledge, which is also sensitive to the context. The thesis provides preliminary elements of guidelines for future dialog authors and an extensive bench of use cases implemented for various experiments. The thesis concludes with a preview on tasks for dialog authors which are expected to succeed based on the technology provided by this thesis.