谓词逻辑推理中的Petri网应用

摘要

逻辑推理是人工智能的基础，而逻辑中的一阶谓词逻辑是使用较为广泛的知识表示方法，因此研究一阶谓词逻辑的推理问题是一项很有意义的工作。在前人研究的基础上，借助Petri网中的谓词/变迁(Pr/T)网为一阶谓词逻辑推理寻找新的有效方法，为人工智能中一阶谓词逻辑推理的研究开辟一个新的思路是本文研究的出发点。本文研究的主要内容包括以下几个方面：
　　1）针对现有的建模方法不方便于计算机实现以及建模过程的不确定性和不唯一性，本文提出了一种对一阶谓词公式直接建模的方法，只需将任意所给的一阶谓词公式化去量词后就可对其直接建模，建模过程更加简单明了，且克服了上述已有建模方法的不足。
　　2）提出了对一阶谓词公式的Pr/T网系统模型进行化简的方法，这样可以在利用Pr/T网系统对一阶谓词逻辑进行推理或有关的证明之前，尽早删除对推导无用的变迁，加快推理或证明的过程。
　　3）提出了一种由一阶谓词公式直接构造对应关联矩阵的方法，而省略了建立一阶谓词公式Pr/T网系统的过程。
　　4）本文找到了两个一阶谓词公式等价的一个充分条件以及一个能部分判定两个一阶谓词公式等价性的算法。另外，对于一阶谓词公式的一个常见子类——无自由变元单量词的一阶谓词公式，提出了一个判定这种一阶谓词公式等价性的充分必要条件和判定算法。
　　5）提出了两种用于一阶谓词逻辑推理的图形方法：目标制导的图形推理法和变迁框图形推理法。
　　6）借助Pr/T网系统的关联矩阵，提出关联矩阵初等变换法来实现一阶谓词逻辑推理。
　　7）对本文提出的两种图形推理方法以及关联距阵初等变换法，文中不仅将其应用于证明已知结果的正确性，而且用于求取实际问题的答案以及实现目标的可行方案，使得这些推理方法的适用面得到推广。

目录

封面

声明

中文摘要

英文摘要

目录

Contents

1 绪论

1.1 选题背景及意义

1.2 在一阶谓词逻辑推理中使用Petri网的理由

1.3 国内外研究现状

1.4 本文研究工作的主要内容

1.5 本文的组织结构

2 基本知识

2.1 Petri网

2.2 谓词/变迁系统

2.3 网逻辑与一阶谓词逻辑推理

2.4 小结

3 一阶谓词公式的建模及其关联矩阵的直接构造

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

3.2 一阶谓词公式的Pr/T系统模型化简

3.3 一阶谓词公式对应的关联矩阵的直接构造法

3.4 小结

4 一阶谓词公式等价性的证明

4.1 一阶谓词公式的等价前束合取范式唯一性的实现

4.2 两个一阶谓词公式等价性判定的充分条件

4.3 两个WFV-1Q一阶谓词公式等价性判定的充要条件

4.4 小结

5一阶谓词逻辑的图形推理法

5.1 目标制导的图形推理法

5.2 采用变迁框的图形推理法

5.3 小结

6 一阶谓词逻辑推理的关联矩阵初等变换法

6.1 关联矩阵初等变换法用于一阶谓词逻辑推理

6.2 小结

7 结论

7.1 本文的主要工作

7.2 进一步的研究

致谢

附录A

参考文献

作者在读期间的研究成果