[PRL] Automated Generation of User Guidance by Combining Computation and Deduction...

[Mitch]

FYI: I post these if the abstract suggests there's even some vague
connection to something we're interested in. Feel free to hit "delete".

Sent to you by Mitch via Google Reader: Automated Generation of User
Guidance by Combining Computation and Deduction. (arXiv:1202.4832v1
[cs.LO]) via cs.PL updates on arXiv.org by <a
href="http://arxiv.org/find/cs/1/au:+Neuper_W/0/1/0/all/0/1">Walther
Neuper</a> on 2/22/12

Herewith, a fairly old concept is published for the first time and
named "Lucas Interpretation". This has been implemented in a prototype,
which has been proved useful in educational practice and has gained
academic relevance with an emerging generation of educational
mathematics assistants (EMA) based on Computer Theorem Proving (CTP).

Automated Theorem Proving (ATP), i.e. deduction, is the most reliable
technology used to check user input. However ATP is inherently weak in
automatically generating solutions for arbitrary problems in applied
mathematics. This weakness is crucial for EMAs: when ATP checks user
input as incorrect and the learner gets stuck then the system should be
able to suggest possible next steps.

The key idea of Lucas Interpretation is to compute the steps of a
calculation following a program written in a novel CTP-based
programming language, i.e. computation provides the next steps. User
guidance is generated by combining deduction and computation: the
latter is performed by a specific language interpreter, which works
like a debugger and hands over control to the learner at breakpoints,
i.e. tactics generating the steps of calculation. The interpreter also
builds up logical contexts providing ATP with the data required for
checking user input, thus combining computation and deduction.

The paper describes the concepts underlying Lucas Interpretation so
that open questions can adequately be addressed, and prerequisites for
further work are provided.

Things you can do from here:
- Subscribe to cs.PL updates on arXiv.org using Google Reader
- Get started using Google Reader to easily keep up with all your
favorite sites
-------------- next part --------------
HTML attachment scrubbed and removed