统计问题的量词消除
本研究提出了一种 Skolem 化算法来解决模型计数问题,扩展了一阶模型计数器的适用范围,使其能够用于概率逻辑程序等有向模型,同时还简化了抬升模型计数算法的设计。
Dec, 2013
该论文提出了一种将概率论和第一阶逻辑相结合的方法,在有限域内具有 Herbrand 解释的情况下,定义了概率证明定理及其推广问题,然后提出了能够同时拥有图模型推理和一阶定理证明的完整能力的方法,并开发了一种高效算法。实验表明,当逻辑结构存在时,该算法远优于目前已有的方法。
Feb, 2012
本文介绍了一种基于 Peirce 的存在图推理和蕴含图的命题逻辑简化演算法,该算法可以应用于嵌套形式的命题逻辑公式,保持等价性、保证变量、子句和文字数量的单调递减,并最大限度地保留结构问题信息;同时,提出了一个系统化应用两个规则(EPR 和 TWSR)的简化过程,可用于简化大型布尔可满足性问题和任意形式的命题公式,并对其在空间和时间方面进行了算法复杂性的形式分析;最后,展示了如何通过引入一种新的 n 元蕴含图扩展我们的规则,以涵盖所有已知的等价性保持预处理过程。
May, 2024
本文详细研究了量化可布尔逻辑以及其存在量化和全称量化变量的相关应用,特别是在可解释人工智能方面的应用,提出了一种新的量化语义,并探讨了变量 / 文字与存在性 / 普遍性量化之间的相互作用。此外,我们还确定了一些布尔公式和电路类别,其中量化可以有效地完成。
Aug, 2021
介绍了一种形式化自然语言中量词的方法,运用于人机交互的背景下,该方法基于带有变量基数表示能力的一阶逻辑,类似于广义量词的操作;通过设计了一个端到端系统,能够接收自然语言输入,将其转换为形式逻辑表示,进行评估,并返回结果或向模拟机器人发送命令来演示该方法。
Aug, 2023
该研究旨在解决将命题公式转化为任意格式的等价公式的问题,使用量子布尔公式编码的方法可以有效地解决此类问题,因为这种方法远优于使用暴力方法或者 SAT 求解器进行转化。
Mar, 2023
本文调查了实代数几何算法理论的新、旧发展,主要涵盖关于真实数的一阶理论中的量词消除和计算半代数集拓扑不变量等问题,重点分析了这些算法的复杂性和背后问题的计算难度,并对一些近年来越来越受欢迎的半定规划数值方法进行了讨论。
Sep, 2014
该研究提出了一种新的最小解算器系统性生成方法,通过消除不出现在线性方程的未知数并通过升级实现线性化对完全非线性问题问题的求解,我们成功地提出了三个部分标定相机相对姿态计算问题的更有效解决方案,同时还发现了部分标定相机的基础矩阵的新约束关系。
Mar, 2017