摘要
一阶谓词逻辑可以借助关联矩阵进行有效推理。为了提高关联矩阵的构造效率,从而提高一阶谓词逻辑推理的效率,提出一种由一阶谓词公式构造对应关联矩阵的递归方法。该方法利用二叉树的递归性质,对任意一个一阶谓词公式,在化去量词后直接构造关联矩阵。该方法为借助关联矩阵实现一阶谓词逻辑的自动化推理提供了可能。
Incidence matrix can be applied in the process of first-order predicate logical reasoning. In order to improve the construction efficiency of incidence matrix, so as to improve the efficiency of first-order predicate logical reasoning, a recursive method by which the incidence matrix of first-order predicate expression can be constructed is proposed. For any first-order predicate expression, the incidence matrix can be generated directly using the recursive property of binary tree after logical connectives are eliminated in the method. The method provides possibility to realize automatic reasoning of first-order predicate logic by means of incidence matrix.
出处
《计算机工程与应用》
CSCD
2014年第3期36-41,共6页
Computer Engineering and Applications
基金
国家自然科学基金(No.61170079
No.61201252)
教育部科技论文快速共享项目(No.2012107)
山东省优秀中青年科学家奖励基金(No.BS2009DX012)
关键词
一阶谓词公式
关联矩阵
逻辑推理
二叉树
递归方法
first-order predicate expression
incidence matrix
logical reasoning
binary tree
recursive method