Feb, 2022

中学自动推理入门：四个几何问题

PDF
TL;DR本文探讨了在信息和通信技术的帮助下使用自动推理工具解决几何问题的实验，以解决在中学自动推理系统引入中所面临的难题。
automated deductionsecondary schoolgeometrylesson planict
发现论文，激发创造
  • 基于规则的定理证明器：中学证明入门

    介绍了在中学引入自动推理系统面临的几个瓶颈，讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明，旨在介绍几何定理的形式证明，以激发学生的兴趣。

    Mar, 2023

  • 使用 GeoGebra Discovery 自动演绎解决 Náboj 2023 竞赛中的几何问题

    使用计算机和 GeoGebra Discovery 等软件工具，我们解决了 N'aboj 2023 竞赛中的一些几何问题，并通过符号计算分析了输入机器的困难，设定了未来使此类竞赛问题更易解决的目标。

    Jan, 2024

  • 智能辅导系统中几何问题的自动合成

    该论文介绍了一个名为 GeoTutor 的智能辅导系统，它能自动合成证明问题及其解决方案，以及针对学生在欧几里得几何方面的缺陷提供个性化练习问题。

    Oct, 2015

  • 基于约束求解的合成几何陈述和证明的自动补全方法

    通过使用合一逻辑和约束求解，我们提出了一个框架，用于补充不完整的猜想和证明。该框架可以将具有缺失假设和不明确目标的猜想转化为正确的定理，并帮助完成草图式证明以使其适于人类阅读和机器检查。

    Jan, 2024

  • 自动形式化欧几里德几何

    本文介绍了一种自动形式化欧几里得几何的神经符号框架，该框架结合了领域知识、SMT 求解器和大型语言模型，这一框架的挑战之一在于通过定理证明器自动填充图形信息以简化模型，实验结果展示了自动形式化几何问题时最新的语言模型的能力和局限性。

    May, 2024

  • 用 GeoGebra Discovery 解决奥地利奥林匹克数学竞赛问题：从中获得的教训

    我们通过 GeoGebra Discovery 中的自动推理工具解决了奥地利数学奥林匹克 2023 年的一个问题，并且描述了其中的四种反馈形式：即时的自动解答、根据最新提案进行复杂性评估、找到给定命题的更一般化命题，以及使用 LocusEquation 命令时出现的大量退化情况的分析困难。

    Jan, 2024

  • 开放几何证明社区项目

    本文描述了 Open Geometry Prover Community Project 的目标和实施步骤，旨在将不同自动几何定理证明工具的开发整合到一个共同的 “伞下”，以丰富人们的数学体验。

    Jan, 2022

  • 抽象代数中的初等证明的自动规划技术

    该研究探索了自动规划在自动定理证明中的应用，研究了利用规划构建抽象代数中的基础证明，证明自动规划技术在自动定理证明领域是可行的。

    Dec, 2023

  • 几何中自动定理生成 / 发现的方法和度量考虑

    为了发现并判断几何定理的有趣性，本文针对自动发现几何定理和其性质的不同方法和度量进行讨论，并引入了一个不可判定性结果来证明判断定理生成程序是否能产生有趣定理是一个非确定性任务。此外，还强调了需要通过专家调查和相关度量和方法的研究明确定理生成程序和有趣几何定理之间的关系。

    Jan, 2024

  • 第 14 届国际自动几何推理会议论文集

    ADG 是一个关于几何和自动推理交叉领域的论坛，每两年举办一次，为交流思想、展示研究成果和进展，以及展示软件工具提供了平台，2023 年的 ADG 会议在塞尔维亚贝尔格莱德举办，并且特别关注于教育中的推理问题。

    Jan, 2024