automated theorem provers | BriefGPT

关键词automated theorem provers

搜索结果 - 5

学习引导的自动推理：简要调查
自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人
PDF4 months ago
迈向自动可读的直尺和圆规构造证明
本论文展示了我们的三角形构造求解器 ArgoTriCS 如何与一阶逻辑和连续逻辑的自动定理证明器合作，从而生成既可读性强的合成正确性证明，又具有形式化特性的构造解决方案。这些证明依赖于许多高级引理，我们的目标是从几何的基本公理中形式化证明它
PDF5 months ago
谁发现了短证明？使用高阶自动定理证明器探索 Boolos 的奇怪推理变体
应用高阶自动推理证明器探索 Boolos' Curious 推论，通过提供适当的简写符号以发现短证明所需的高阶引理，并提出全证明自动化的可能性。
PDF2 years ago
开放几何证明社区项目
本文描述了 Open Geometry Prover Community Project 的目标和实施步骤，旨在将不同自动几何定理证明工具的开发整合到一个共同的 “伞下”，以丰富人们的数学体验。
PDF3 years ago
Satallax 的内部指导
提出了一个基于给定句子算法的自动定理证明器的新的内部指导方法，该方法使用先前证明中的正负例影响未处理子句的选择。为此，提出了一种基于幺半群结构的类型广义标签出现次数的朴素贝叶斯分类的有效方案。将这种方法在高阶逻辑证明器 Satallax 中
PDF8 years ago