谓词/变迁系统对一阶谓词公式的建模

Modeling of First-Order Predicate Expression by Using Predicate/Transition System

研究了利用谓词/变迁系统对一阶谓词公式建模的方法。借助于软件工程中"由粗到细,逐层分解"的思想,定义了对各种逻辑联结词进行处理的基本模型。给出了一阶谓词公式的二叉树表示方法,进而利用二叉树的递归性质,提出了递归构造一阶谓词公式对应的谓词/变迁级的"事实变迁"表示的方法,克服了已有相关建模方法中存在的不足,为一阶谓词公式的自动化建模提出了新的思路。最后,探讨了一阶谓词公式的谓词/变迁系统模型在谓词逻辑推理领域的应用及其意义。

This paper studies the modeling of first-order predicate expression by using predicate/transion system. Based on the idea of ＂analyze stage by stage, from coarse to minute＂ in software engineering, the basic models of processing all kinds of logic connectives are defined. The binary tree describing first-order predicate expression is given, furthermore the method which recursively constructs ‘fact transition＇ of predicate/transion system for first-order predicate expression using recursive property of binary tree is proposed. The method overcomes some shortcomings in the existent modeling method. A new idea to automatically modle first-order predicate expression is provided. In the end, the application and significance of predicate/transition system modeling of first-order in the area of predicate logic reasoning is discussed.