eJMT Abstract

Traditional course material in engineering disciplines lacks an important component, interactive support for stepwise problem solving. Theorem-Proving (TP) technology is appropriate for one part of such support, in checking user-input. For the other part of such support, guiding the learner towards a solution, another kind of technology is required.

Both kinds of support can be achieved by so-called Lucas-Interpretation which combines deduction and computation and, for the latter, uses a novel kind of programming language. This language is based on (Computer) Theorem Proving (TP), thus called a “TP-based programming language.”

This paper is the experience report of the first “application programmer” using this language for creating exercises in step-wise problem solving for an advanced lab in Signal Processing. The tasks involved in TP-based programming are described together with the experience gained from a prototype of the programming language and of its interpreter.

The report concludes with a positive proof of concept, states insufficiency usability of the prototype and captures the requirements for further development of both, the programming language and the interpreter.