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 Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Herewith, a fairly old concept is published for the first time and named"Lucas Interpretation". This has been implemented in a prototype, which hasbeen proved useful in educational practice and has gained academic relevancewith an emerging generation of educational mathematics assistants (EMA) basedon Computer Theorem Proving (CTP).  Automated Theorem Proving (ATP), i.e. deduction, is the most reliabletechnology used to check user input. However ATP is inherently weak inautomatically generating solutions for arbitrary problems in appliedmathematics. This weakness is crucial for EMAs: when ATP checks user input asincorrect and the learner gets stuck then the system should be able to suggestpossible next steps.  The key idea of Lucas Interpretation is to compute the steps of a calculationfollowing a program written in a novel CTP-based programming language, i.e.computation provides the next steps. User guidance is generated by combiningdeduction and computation: the latter is performed by a specific languageinterpreter, which works like a debugger and hands over control to the learnerat breakpoints, i.e. tactics generating the steps of calculation. Theinterpreter also builds up logical contexts providing ATP with the datarequired for checking user input, thus combining computation and deduction.  The paper describes the concepts underlying Lucas Interpretation so that openquestions can adequately be addressed, and prerequisites for further work areprovided.

Automated Generation of User Guidance by Combining Computation and Deduction