一阶谓词公式关联矩阵的构造方法

Construction method of incidence matrix to first-order predicate expression

一阶谓词逻辑可以借助关联矩阵进行有效推理。为了提高关联矩阵的构造效率,从而提高一阶谓词逻辑推理的效率,提出一种由一阶谓词公式构造对应关联矩阵的递归方法。该方法利用二叉树的递归性质,对任意一个一阶谓词公式,在化去量词后直接构造关联矩阵。该方法为借助关联矩阵实现一阶谓词逻辑的自动化推理提供了可能。

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.