适应性混合主动教育交互验证规划

理论计算机科学电子笔记103（2004）105-120www.elsevier.com/locate/entcs适应性混合主动教育交互验证规划Andreas Meier Erica Melis Martin PolletFachbereichInformatik，UniversitüatdeSaarlandes，anddDFKISaarbrücken，66041Saarbruücken，Germany电子邮件：{ameier|melis}@dfki.de，pollet@ags.uni-sb.de摘要今天，大多数定理证明系统要么由它们的开发人员使用，要么由（一小群）受过特别训练和熟练的用户使用。为了使定理证明功能对更大的客户有用，我们必须问出于教育目的，定理证明器可以用于不同的场景，可以为有不同需求的学生提供服务。因此，用户界面以及底层证明器的功能选择必须适应上下文和学习者。在本文中，我们提出了证明规划作为交互式证明练习的后台引擎，一个交互控制台，它是我们图形用户界面的一部分。基于校对计划情况，控制台向学习者提供校对步骤的建议。这些建议可以被动态地调整，例如，用户和教学标准使用教学知识的创建和建议的呈现保留字：数学教育，自适应GUI，自适应定理证明1动机到目前为止，开发自动定理证明系统的主要目标一直是输出真/假的陈述制定在一些逻辑或交付证明对象。交互式定理证明系统旨在支持用户以不同方式完成的证明构造，它们通过对证明步骤提出有效建议来限制搜索空间（选择），它们建议适用的引理，或者它们自动产生整个子证明。这些功能是有用的，例如，用于检查学生当目标是1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.07.001106A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-学习如何在定理证明系统的帮助下证明数学定理。什么是必要的，以支持学习数学证明？一些可用性特征已经过研究，例如，被认知科学。这些研究[15]表明，学生在理解和生成证明方面的数学能力不足与学生自我引导的探索性学习能力不足以及在解决问题时缺乏（自我）解释有关。这种探索性学习可以通过工具来支持。此外，实证结果表明，使用证明规划方法（明确编码数学步骤）的教学可能是一种优于数学证明的跨学科学习的学习方法[8]。这激发了证明规划器[13]与用户自适应学习环境ACTIVEMATH[7]的集成。然而，仅仅提供这一工具对教育是不够的，因为要有效地学习，还必须满足更多的要求。一般来说，教育环境需要额外的功能（与单纯的辅助系统相比），例如• 对学习者的适应性[4]，• 允许错误的证明尝试，其（教练）发现和修复是学习的主要来源[16]，• 对学习者活动的反馈适应性和个性化可能会影响内容、可能的或首选的问题解决策略、证明的详细程度、外观等。例如，关于具体序列极限的练习可以依靠仅使用极限定义的策略或使用应用极限定理的策略来解决。证明思想的选择应取决于学习者的能力和知识。另一个必须适应学习者的维度是介绍可用的方法。一个能力较差的学生将有更多的困难来选择许多方法，在这种情况下，猜测的可能性增加。适应也可能取决于学习者的活动历史。例如，当学生最近几次无法应用该方法时，系统应该做出反应。已经证明，成功的学习确实主要发生在学生发现失败或陷入僵局并设法从中恢复的时候[16]。因此，对于学习来说，一个特别有趣的问题是，是否以及如何利用学生的错误行为从错误中A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-107以及如何应对错误。错误的情况或错误的建议是不适合的系统，旨在解决问题的援助。 然而，对于一个学习工具来说，总是只给出正确的建议可能不是最好的主意，因为学生可能只是点击建议，而不是学习任何东西。例如，当学生应该通过应用定理来证明序列的极限，并且她已经熟悉这些定理时，那么只提出适用的定理就太受限制了当然，何时提出错误建议的决定将取决于学生学生的能力（都在ACTIVE MATH因此，建议应根据学生模型和教学策略动态生成。文章的结构如下。在第2节中简要介绍了证明规划和主动规划之后，我们在第3节中介绍了应用证明规划器的四个学习场景在第4节中，我们将重点介绍一个场景的实现，即交互式证明规划场景，以及它的使用示例特别是，这一节解释了练习如何这个控制台与部分证明计划的多模态显示一起是我们当前用于证明练习的GUI。第5节是总结和今后的工作。2预赛2.1证明计划对于交互式证明练习，采用了大型证明计划器[13]的两个功能：自动证明计划[9]和基于代理的命令建议机制[1]对交互式证明计划在本节中，我们将分别介绍这两种机制稍后（第4节），我们将描述它们的组合。2.1.1自动打样计划Proofplanning最初是为了自动化定理证明而设计的，旨在通过在方法级别证明来减少搜索空间，这可以封装复杂的证明步骤，并通过引入元级别指导[2，10]。证明计划从一个目标开始，这个目标代表了108A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-证明和证明假设。它通过应用满足应用条件的方法继续下去，这会产生新的目标或将目标减少为子目标，直到没有目标。实例化方法的结果序列构成解决方案证明计划。通常，证明构造可能需要构造数学对象，即，通过见证项实例化存在量化变量。 在证明规划元变量被用作见证项的占位符，并且规划过程继续进行，直到收集到足够的信息来证实元变量。特定于域的约束求解器可以帮助构造作为特定域的元素的数学对象。在证明规划过程中，约束求解器检查元变量上的约束的一致性，并在约束存储中收集一致的约束。然后，它计算满足所收集的约束的元变量的实例化[11]。为了构建证明规划方法的库并使证明规划过程更加分层，已经引入了策略[9]。一个简单的证明规划策略由一组方法和搜索算法指定。不同的证明规划策略对应并实现不同的证明思想。证明计划有一个自动和交互模式。在自动模式中，证明计划器搜索解决方案证明计划，即，在每个中间状态中，它搜索可应用的方法和有效的实例。以数学为导向的数学指导这一搜索。在交互式证明计划中，用户必须做出所有的搜索决策，包括策略和方法的选择以及元变量的实例化2.1.2命令建议机制最初，开发命令建议机制是为了支持用户在使用策略进行证明构建时使用MySQL [1]。所有用户与VMWARE系统的通信都是通过命令执行的，除其他外，还通过应用策略来操纵验证计划。命令建议机制计算并建议指定可应用策略的命令，以及将策略应用于当前证明状态所需的所有参数，即，到哪个证明节点和用哪个参数。这将用户从搜索适用的策略中解放出来。建议机制由代理实现。命令与策略相关联，具有策略输入的参数。对于每个参数，有一个代理检查是否有合适的（即，匹配）当前证明上下文中的参数的实例化。代理程序同时运行，一旦代理程序运行，A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-109作为一名特工，他是成功的。例如，考虑=Subst策略，它将具有等式a=b的证明节点应用于具有公式F[a]的证明节点（其中a是F的子项），并导出具有公式F[b]的新证明节点。 与此策略相关联的是命令=SUBST-COMMAND。此命令具有参数“proof node withequation to apply” 、 “proof node to apply equation to” 和 “position to apply theequation to”（如果出现多次）在F[a]中，有不同的可能性用b）代替a。对于这些参数中的每一个，可以指定一个代理，该代理在当前证明计划中搜索参数的合适实例。 例如，与第一个参数相关联的代理搜索带有等式的证明节点。时 查找实例，它将它们记录为命令=黑板上的SUBST-COMMAND。一旦有了对方程的建议，另外两个参数的代理就会活跃起来，然后它们会尝试为它们的参数找到实例，完成对命令=SUBST-COMMAND的建议。部分建议已经呈现给用户。当用户选择一个部分建议时，她必须完成缺少的参数。命令建议机制不限于创建战术应用的建议。在第4节中，我们描述了如何使用相同的机制来创建方法应用程序的建议以及元变量实例化的建议。此外，请注意，应用策略（或方法）的命令的每个参数都不一定有代理。如果某个参数的代理缺失，那么所有创建的建议都是部分的，用户必须指定缺失的部分。2.2一种主动式方法及其用户模型主动数学是一个基于网络的学习环境（数学）[7]。它通常集成了几个用于练习和探索性学习的后台引擎主动式数学自适应地生成（数学）学习材料，即，取决于学习者自适应性基于学生模型，包括• 学习者行为的历史• 她的偏好• 她对概念和技能的掌握程度在0到1之间。学生模型通过对阅读和问题解决等学习活动的诊断来更新。一个学生110A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-并将评估传递给学生模型以更新它。3Proof Planner今天• 证明应该在相对抽象的层次上进行，而不是在逻辑演算的层次上进行。• 在先前的定理证明应用中的若干活动在学校或大学的学习水平上不是严格必要的。例如，加载理论留给更高级的级别，例如理论描述。• 应该启用对学习有效的某些活动，即使它们在典型的定理证明系统及其用户界面中不可用。这包括· 浏览方法描述，· 浏览约束状态，· 请求元级信息，· 适用步骤的有限建议，· 不适用或无用的步骤的可能建议。在数学推理的学习环境中使用证明计划的原因是方法代表了数学推理中的典型步骤。因此，这些方法的交流和教学应该使学生能够扩展和提高他们的推理能力[6]。我们确定了几个基于教学动机的情景，用于教育应用程序，这些情景在整体学习目标和使用的功能方面有所不同。演示和演示现有的演示计划（或演示计划的一部分）被呈现给学习者。证明计划可以一次性或逐步提出本方案旨在了解个别方法的应用效果以及几种方法如何应用于阳离子结合到一个证明计划。在这种情况下，学习者交互式证明计划学习者为给定问题构建证明计划，或者必须通过选择和应用方法以及确定元变量的对象（A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-111元变量）。我们希望在这里，学生可以学习如何应用方法和算法来证明各种定理，以及使用工具来简化数学对象的确定。学习者的主要活动是选择要应用的方法和指定方法的期望应用以及确定数学对象（此外，浏览当前的证明计划并请求附加信息，例如，约束状态）。岛屿规划学习者必须为给定的问题构建一个证明草图。我们希望这种情况下，以支持创造性的证明技能，并认为这是最重要的模式，计算机支持的学习数学证明。此外，这种情况可能有助于理解证明的层次组合。在忽略细节的同时，学习者可以表达一个证明的想法，发现中间目标，并建议目标如何相互依赖。此场景中的主要用户交互是添加证明岛和链接（即，依赖性）（浏览当前岛计划并请求附加信息也发生）。自由探索学习者可以完全交互式地访问大型系统。她可以上传证明过程的理论，可以定义问题，并启动证明过程。此外，她可以自由地访问所有各种证明操作（方法的应用、Meta变量的实例化、岛的推测这种情况只适用于高级学习者。我们希望这种情况促进探究学习。波利亚提出了一个在数学问题解决中教授Meta推理的框架。他的著名著作这是一个公式，一套以简短的问题和命令的形式构成的问题解决策略，其框架包括四个问题解决阶段：（1）理解问题。(2)想个计划。(3)执行计划。(4)回头看看解决方案。（2）的一些问题和命令是，例如：你知道一个相关的问题吗？你使用了所有的数据吗？根据波利亚我们希望这个场景能培养元认知能力。所有这些场景都需要在证明GUI中有相应的外观例如，交互式验证规划和岛屿规划的GUI对象和功能对学习者和上下文的用户自适应性是我们基于我们的证明规划器的教育工具的关键设计目标112A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-4交互式校样规划方案实现的第一个场景是演示和演示证明计划以及交互式证明计划。目前，这两个场景都使用了LUI[14]的扩展版本，这是IBM带有Omega的练习在ACTIVE MATH这种表示包括文本和/或图形表示，定理的形式化，以及特定于练习的设置。当学生决定在ACTIVE MATH会话期间执行一个大型练习时，ACTIVE MATH会启动带有其（扩展）用户界面的大型练习在ACTIVEM路径中，在MYSQL和代理之间建立双向XML-RPC通信。当练习完成时，一些关于超级会话的信息被发送到ACTIVEMATH例如，返回相关方法的成功和错误方法应用的数量以及剩余目标的数量在下文中，我们将把我们的描述限制在交互式证明规划场景以及它如何适应上下文和学习者。此外，我们讨论了一个交互控制台，扩展的LUI的交互式证明规划方案。4.1交互式验证规划首先，简要介绍了交互式验证计划方案的技术实现及其参数，这些参数取自演习演示或在发射时动态确定。交互式证明规划场景结合了大型证明规划器和基于代理的命令建议机制。它使用代理机制来自适应生成方法和元变量配置，即，它采用计算方法和元变量建议的命令和代理的集合。因此，一组命令和代理是场景的第一个参数。该场景并发运行独立代理。 这允许交互式校样规划场景的任何时间行为，其立即向用户报告建议，用户然后可以决定应用建议中的一个或等待其他建议。当学习者选择一个建议时，未完成的建议计算的耗时过程OMEGA尝试应用所选择的建议，该建议要么是错误的并且导致新的证明状态和对学习者的新建议，要么是失败的并且导致对学习者的一些失败反馈交互式验证规划方案的另外两个参数是策略和自动化水平。证明规划战略实施的差异-A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-113证明的想法。也就是说，包含不同方法的不同策略以不同的方式解决证明规划问题。如果为手头的问题选择了一个策略，那么对于该策略的每个方法，必须至少有一个命令和相应的代理策略的某些方法不应该显示给学习者选择，而是应该自动应用。自动应用的策略方法也称为自动化水平交互式验证规划场景的完整实例化称为配置。配置包括• 一个战略，• 命令和代理，• 自动化水平4.2配置的适应性接下来，我们将讨论具体的交互式证明规划练习的配置实例化如何能够适应学习者和上下文。特别是，方法，命令和代理之间的区别允许控制与证明计划器交互的自由度这种设置或多或少具有约束性，或多或少具有引导性，并能实现一定的教学策略。例如，可能导致僵局的建议可以故意引入选择。如下所述，通过配置的不同部分实现自适应4.2.1选择战略该配置可以确定验证规划策略的偏好。可以有不同的证明规划策略可用于证明问题，即，对这个问题有不同的证明思路。例如，考虑关于剩余类的性质的问题[5]。剩余类是整数的等价证明问题包括剩余类的代数性质，如结合性或逆元的存在性，以及剩余类的同构。至少存在三种策略来解决剩余类问题：第一种策略试图通过应用已知定理来解决问题，第二种策略将剩余类问题简化为一组方程，然后必须求解策略的决定取决于学习者的知识（她是否知道作为第一个策略的先决条件的定理，她是否知道策略所使用的方法）和她的知识。114A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-在先前练习中的表现（例如，当其他策略已经被训练时）。这种配置策略可以通过教学规则来编码例如（为了更好的理解而简化）如果studentKnowledge（premises（firstStrategy））> medium且studentKnowledge（firstStrategy）medium然后present exercise-for（firstStrategy）如果studentKnowledge（firstStrategy）> mediumANDstudentKnowledge （ secondStrategy ） >medium AND studentKnowledge （ thirdStrategy ）medium则呈现针对（thirdStrategy）的练习4.2.2命令和代理的选择基于代理的命令建议机制可以通过根据学习者、她的用户模型和练习的学习目标来调整命令和代理的集合来进行配置命令和代理的配置逻辑也可以通过教学规则进行编码一般来说，命令和代理可以编码不同程度的指导和限制。命令和代理的具体选择可以取决于与练习和学习者相关的不同方面。例如，智能体可以根据学习者的经验计算或多或少完整的命令建议：（1）初学者开始时会有很多支持和（几乎）完全指定的建议。(2)后来，这种支持可能会消失，需要学习者提供更多的输入，以便让她在应用方法时进行更多的思考并克服误解。此外，代理可以计算适用的或错误的命令建议：（1）如果目标是快速证明一个猜想（如在纯证明辅助情况下），那么代理被选择，检查适用性并只提供完全指定的适用建议。(2)如果学习者应该理解为什么一种特定的方法是适用的，这种特定的方法实际上是做什么的，以及它是为了什么目的而应用的，那么代理人就被选择了，这些代理人为这种方法的应用提供了错误的建议。 这样，学生可能会遇到典型的错误，并获得帮助，以避免随后的错误。在下文中，我们将讨论可以自动计算哪些类型的方法建议命令和代理，以及练习作者可以提供哪些类型的命令和代理可以从方法规范自动生成具有相应代理集的初始命令集。自动生成的代理可以不同。它们是否为特定参数提供输入A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-115或者是否需要学习者输入一个方法的命令，它有一个目标和前提作为参数，可以有建议代理的前提或离开选择的前提学习者。例如，群同态的练习旨在教授抽象群的性质和群之间的同态。相关的属性是，例如， 群运算的结合性、单位元的存在性和逆元的存在性。对于每个 属 性 ， 都 存 在 一 个 应 用 该 属 性 的 方 法 。 例 如 ， 方 法 Group-Is-Asynchronous应用关联性，即，它将目标F[（（g1g2）g3）]简化为一个目标F[（g1<$（g2<$g3））]，如果存在前提群（G，<$）（其中G是一个集合，<$是一个二元运算）且gi∈G，i=1， 2， 3. 需要5名特工为了计算针对Group-Is-Assumption的建议，一个用于目标，四个用于方法的前提。根据该方法的具体说明，可以自动创建五个相应的代理。当所有这些代理都被使用时，就会为该方法创建完全指定和适用的建议。如果省略了一些代理，那么只会创建部分指定的建议，这样学生就必须指定缺少的输入。具有实现特定建议的代理的对应集合的其他命令，例如，一个建议，不导致一个解决方案或一个代表一个典型的错误，为一个特定的学习目标，必须添加到一个积极的数学练习的作者的练习。附加的命令和代理将被评估并与自动生成的命令和代理合并如上所述，自动生成的代理仅创建适用的建议。在同态射练习中还有什么其他有趣的建议吗？同态练习通常涉及两个群结构（G，n）和（GJ，nJ），其中一个结构是同态h的域结构，另一个是h的上域结构。想要教导区分h的余域和域的作者可以指定代理，其混合两种结构的元素，例如，提出了一个应用群Is Asynchronous的目标F[（g1<$g2）<$g3）]的前提（群（GJ，<$J）和gi∈G，i=1， 2， 3.此外，一个作者谁想要教不同的群体性质，当他们适用于-电缆可以指定代理，其建议与方法的目标不匹配的方法的应用，例如，建议将群-Is-Assoc应用于目标F[g1g1−1]。授权者指定的命令和代理也可以提供过度指定的建议。过度指定的建议不仅包括应用方法所需的所有输入的指定由于应用该方法而产生的证明状态中的新假设和目标例如，考虑一种方法，116A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-它使用计算机代数系统通过执行算术简化来简化目标中的项。自动生成的命令只包含一个参数，这是应该应用简化的目标。想要教学习者执行简化的作者可以为简化的结果指定一个带有附加参数的命令。然后，学习者必须在方法应用的建议中为该论点提供输入，并且方法应用的结果可以随后与学习者的输入进行比较4.2.3自动化水平某些方法的自动化应用避免了学习者对证明步骤的具体化的困扰，她已经知道了。分解逻辑数量词和连接词的方法是自动化方法的典型示例。此外，如果学习者被诊断为理解这些方法的结果，则4.3交互控制台目前，交互式验证计划练习的用户界面是由图1所示的交互控制台丰富的LUI。该图的屏幕截图显示了GUI在一个阶段，其中方法已经应用于初始问题。学习者与交互式证明计划场景的交互仅通过交互控制台进行，如图2所示。这个相对简单的对话框窗口提供了方法和元变量的选择，而不是MYSQL交互控制台呈现由交互式证明规划场景计算的建议。学习者可以从交互控制台的第一列“目标”中选择一个目标。这个目标的可用方法建议显示在第二列，“操作”列中。当学习者从第二列中选择动作时，她可能会被要求附加参数，例如，哪些假设应该被用作前提。交互控制台的第三列最后一列，“撤销”列，允许删除证明步骤和删除元变量的实例化。交互窗口顶部带有计算机符号的按钮启动自动校对计划步骤，以防学习者在校对构建过程中完全卡住为了使最频繁的用户交互易于执行，这些交互只需要很少的击键。遵循这一哲学意味着A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-117Fig. 1.具有图形校样演示、校样线序列和交互控制台的用户界面。图二.用于交互式打样规划的交互控制台。选择一个方法的名字来输入比输入完整的方法名字要快。此外，记住一个名字会比认出这个名字更加重工作记忆的负担。因此，再次118A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-从列表中选择一种方法会减少对实际学习和理解证明的注意力。然而，在某些学习情况下，对于某些学习者来说，记住一种方法或查找它可能是重要的在课程材料中使用它之前。也就是说，选择菜单并不总是合适的（类似于多项选择题，可能不足以满足学习目的）。5结论在这篇文章中，我们讨论的应用程序的大型系统作为一种工具，学习数学证明。我们确定了几个设计目标，从教学的角度来看，例如，适应学习者的需求和能力（我们将其确定为教育用途的关键设计目标），促进探索性学习，以及允许错误的证明尝试，这通常是大多数交互式定理证明器无法满足的。出于这些要求，我们设计了四个场景，学习者可以与PINTERMEGA互动。到目前为止，我们实现了其中的两个场景，演示和重放证明计划以及交互式证明计划。交互式校对规划场景的适应是通过配置来实现的，配置可以包括不同的校对规划策略、不同的建议代理和不同的自动化水平。建议代理实现不同程度的指导和约束，他们可以提供建议，这可能会导致错误。可以根据学习者的知识和掌握水平来选择配置。配置导致以下对学习有用的功能：• 复杂性，• 互动的动态建议• 错误的建议可以用来触发从失败中学习，今后工作所描述的VMWARE和ACTIVEMATH的集成尚未包括实现教程要求所需的所有适配和功能。例如，交互式验证规划方案的配置目前是在开始时选择的，然后在整个练习期间固定这防止了对学习器性能的动态适应。在练习过程中需要调整的主题是策略（当学习者不能应用最初选择的策略时，然后选择替代策略），A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-119卢卢伊建议的具体性（当学习者未能为未具体化的建议提供输入时，则提供更具体的建议）和反馈的可用性当前的GUI不适应证据，建议和反馈的呈现，以满足不同学习者的需求。这将是不久的将来的目标。此外，我们目前正在研究自动生成错误和过于具体的建议的可能性。引用[1] C. BenzmüllerandV. 好极了。ABlackboardArchitecturererGuid i ngInteractveProofs. 在人工智能：方法，系统和应用程序。 第8届国际会议（AIMSA'98），LNAI第1480卷，第102-114页。Springer-Verlag，1998.[2] A. 邦 迪 使 用 明 确 的 计 划 来 指 导 归 纳 证 明 。 在 Proc.9th International Conference onAutomated Deduction（CADE-9），LNCS的第310卷，第111Springer-Verlag，1988.[3] M. 科尔哈塞OMDOC：走向管理、分发和管理的互联网标准数学知识的教学在Proceedings AISC[4] H. Mandl，H.Gruber和A.伦克尔《心理学的酶学》，第4卷，第436Hogrefe，1997年。[5] A. Meier和V. Sorge。探索剩余类的性质。第八届符号计算与机械化推理集成研讨会（Calculemus-2000）。 AK彼得斯，纽约，纽约，美国，2000年。[6] E. 我的。为什么要为您的客户提供帮助？ InFestschriftin Honor orofJo？gSiekmann，LNAI.Springer-Verlag，2003.[7] E. Melis，J.Buedenbender，E.Andres，A.Frischauf，G.Goguadse，P.Libbrecht，M.Pollet，以及C.乌尔里希一个积极的方法：一个通用的和适应性的基于网络的学习环境。《人工智能与教育》，12（4）：385[8] E.梅利斯角马奇马赫角Ullrich，and P. Gerjets.教学设计的自动化证明规划。认知科学学会年会，第633-638页，2001年[9] E. Melis和A.梅尔用多种策略证明规划。第一届国际计算逻辑会议，LNAI，1861卷，第644-659页。Springer-Verlag，2000.[10] E. Melis和J.西克曼基于知识的证据规划。Arti ficial Intelligence，115（1）：65[11] E. Melis，J. Zimmer和T. Müller. 解决方案的成本转移问题。在欧洲人工情报会议，2000年，第229-233页[12] G.波利亚 如何解决它。普林斯顿大学出版社，普林斯顿，1945年。[13] J. S iekm ann，C. Ben zmüller，V. Brezhn ev，L. Cheikhr o uh ou，A. Fiedler，A. Franke，H. 好吧，M. Kohlhase，A.Meier，E.梅利斯，M。莫施纳岛Normann，M.Pollet，V.佐尔格角乌尔里希，C.P. Wirth和J. Zimmer。用MEGA进行验证开发。第18届自动演绎会议论文集（CADE-18），LNAI第2392卷，第144-149页。Springer-Verlag，2002.[14] J. S iekm a nn，S. Hess，C. Benzmüllerr，L. C h eikhr o uh o u，A. Fie d ler，H. Horacek，M.Kohlhase，K. Konrad，A.Meier，E.梅利斯，M。Pollet和V.抱歉： 奥夫利·梅加先生接口。Formal Aspects of Computing，11（3）：326120A. Meier et al. / Electronic Notes in Theoretical Computer Science 103（2004）105-[15] K.R eisss ， F.他 会 给 我 打 电 话 ， 还 有 J 。你 好 。Indiv idulleundschulischeBedingingungsfaktorenfur？rgummentatinenundBeweiseimMathematikunterricht.InBildungsqualitétvonSchule ： Schulische und außerschulische Bedingungenmathematischer，naturwissenschaftlicherunduüberfachlicherKompetenzen.BeiheftderZeitschriftfur？rP？dagogik，pages51-64. 2002年，贝尔·T·Z。[16] K. VanLehn，S.锡勒角默里，T. Yamauchi和W.B.巴格特人类辅导：为什么只有一些事件会导致学习？认知与教学，2001年。