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