通过结合计算与演绎自动生成用户引导

在此，一个相当古老的概念首次被发表并命名为“Lucas 解释”（Lucas Interpretation）。该概念已在一个原型中实现，并在教育实践中证明是有用的，随着基于计算机定理证明（CTP）的新一代教育数学助手（EMA）的出现，它获得了学术相关性。自动定理证明（ATP），即演绎，是用于检查用户输入的最可靠技术。然而，ATP 在自动生成应用数学中任意问题的解方面天生较弱。这一弱点对 EMA 至关重要：当 ATP 检查用户输入不正确且学习者陷入困境时，系统应能建议可能的下一步。Lucas 解释的关键思想是按照用一种新颖的基于 CTP 的编程语言编写的程序来计算计算步骤，即由计算提供下一步。用户引导是通过结合演绎和计算生成的：后者由特定的语言解释器执行，该解释器的工作方式类似于调试器，并在断点处将控制权交给学习者，即生成计算步骤的策略。该解释器还构建逻辑上下文，为 ATP 提供检查用户输入所需的数据，从而将计算与演绎结合起来。本文描述了 Lucas 解释的基本概念，以便能够充分解决悬而未决的问题，并为后续工作提供了前提条件。