English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

"Systems that Explain Themselves" appears a provocative wording, inparticular in the context of mathematics education -- it is as provocative asthe idea of building educational software upon technology from computer theoremproving. In spite of recent success stories like the proofs of the Four ColourTheorem or the Kepler Conjecture, mechanised proof is still considered somewhatesoteric by mainstream mathematics. This paper describes the process ofprototyping in the ISAC project from a technical perspective. This perspectivedepends on two moving targets: On the one side the rapidly increasing power andcoverage of computer theorem provers and their user interfaces, and on theother side potential users: What can students and teachers request fromeducational systems based on technology and concepts from computer theoremproving, now and then? By the way of describing the process of prototyping thefirst comprehensive survey on the state of the ISAC prototype is given as aside effect, made precise by pointers to the code and by citation of allcontributing theses.

Prototyping "Systems that Explain Themselves" for Education