Automated Generation of User Guidance by Combining Computation and Deduction
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 assistant...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-02-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1202.4832v1 |
| _version_ | 1818268828917825536 |
|---|---|
| author | Walther Neuper |
| author_facet | Walther Neuper |
| author_sort | Walther Neuper |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-12T20:44:42Z |
| format | Article |
| id | doaj.art-31d1dbd398c641d49a80152c670843ac |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-12T20:44:42Z |
| publishDate | 2012-02-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-31d1dbd398c641d49a80152c670843ac2022-12-22T00:12:36ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-02-0179Proc. THedu 20118210110.4204/EPTCS.79.5Automated Generation of User Guidance by Combining Computation and DeductionWalther NeuperHerewith, 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.http://arxiv.org/pdf/1202.4832v1 |
| spellingShingle | Walther Neuper Automated Generation of User Guidance by Combining Computation and Deduction Electronic Proceedings in Theoretical Computer Science |
| title | Automated Generation of User Guidance by Combining Computation and Deduction |
| title_full | Automated Generation of User Guidance by Combining Computation and Deduction |
| title_fullStr | Automated Generation of User Guidance by Combining Computation and Deduction |
| title_full_unstemmed | Automated Generation of User Guidance by Combining Computation and Deduction |
| title_short | Automated Generation of User Guidance by Combining Computation and Deduction |
| title_sort | automated generation of user guidance by combining computation and deduction |
| url | http://arxiv.org/pdf/1202.4832v1 |
| work_keys_str_mv | AT waltherneuper automatedgenerationofuserguidancebycombiningcomputationanddeduction |