Automated Generation of User Guidance by Combining Computation and Deduction

Details Automated Generation of User Guidance by Combining Computation and Deduction Automated Generation of User Guidance by Combining Computation and Deduction

2012-02-22

arxiv.org/abs/1202.4832v1

EPTCS 79, 2012, pp. 82-101

Computer Science

Logic in Computer Science

In Proceedings THedu'11, arXiv:1202.4535

Scientific paper

10.4204/EPTCS.79.5

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.

Affiliated with

Also associated with

No associations

Rating

Automated Generation of User Guidance by Combining Computation and Deduction does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Automated Generation of User Guidance by Combining Computation and Deduction, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Automated Generation of User Guidance by Combining Computation and Deduction will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-414697