该文章回顾了自 1950 年以来数学逻辑和计算机科学之间相互影响的重大事件和里程碑。
Feb, 2018
通过引理归纳在正式验证和数学中发挥了关键作用,但其自动化仍然是计算机科学中长期存在的问题,使用定义量词我们开发了 sem_ind,它可以推荐需要通过归纳予以验证的参数
Sep, 2020
本研究中,我们探讨引理在自动定理证明中的重要作用,提出了一种结合学习技术的系统,该系统能够生成有用的引理来协助自动定理证明,并通过试验验证了该系统在几个代表性问题的解决方面的优越性,特别是成功解决了一系列难题,这些难题在过去 20 年间都未被任何系统解决。通过侧重简化附加问题的研究,我们得出了引理以及它们在证明搜索中的根本作用。
Mar, 2023
本文介绍了一种适用于给定形式语言中的任何逻辑语句并随时间精细调整概率的可计算算法,并证明了其在学习预测逻辑陈述中真实和虚假的模式、使用恰当的统计摘要预测具有伪随机的真值序列、拥有关于自身的精确信念、且在极限情况下,其信念有着一种自洽性的优势。
Sep, 2016
数学证明教育的关键词包括准时反馈、自然语言处理、自动分级自由形式数学证明、用户研究。
Jun, 2024
介绍了在中学引入自动推理系统面临的几个瓶颈,讨论了一个基于推理规则和自动方法的实现并使用其进行几何猜想的证明,旨在介绍几何定理的形式证明,以激发学生的兴趣。
提出并阐述了一种新的证明操纵和分析形式主义,为证明检索方式提高了效率,实现了较短证明的自动化,特别是在首阶问题上的历史证明中进行了一项全面的形式重建分析。
Feb, 2023
本文介绍了一个历经半个世纪的万能归纳和万能智能的数学理论,重点讨论了该理论面临的挑战和未解决问题,为研究智能算法提供了指导和标准。
Jul, 2009
该研究探索了自动规划在自动定理证明中的应用,研究了利用规划构建抽象代数中的基础证明,证明自动规划技术在自动定理证明领域是可行的。
Dec, 2023
本文讨论了关于人工智能算法的两种基础框架:归纳与达尔文进化,在此基础上,提出一种新的理解 AI 系统的方法,即全局达尔文主义,认为此方法更能解释 AI 系统的发展过程。
Oct, 2021