Computer algebra implemented in Isabelle's function package under Lucas-interpretation - a case study.
Walther Neuper · 2013
The relation of this paper to “Theorem-Proving (TP) components for educational software ” deserves explanation: TP technology is designed for mechanised justification of formalised facts — so educational software gains a prerequisite for being a “transparent system ” [12] which explains itself. Computer Algebra (CA), however, is not designed for justification (and thus leaves full responsibility