基于归结反演的Petri网推理新方法

被引：6

作者：

周奕

吴时霖

机构：

[1] 伊里诺依大学芝加哥分校电子工程系，复旦大学计算机科学系

来源：

计算机学报 | 1997年 / 03期

关键词：

库所／变迁网; 谓词／变迁网; 逻辑推理; T－不变量; 归结反演;

D O I：

暂无

中图分类号：

TP301.6 [算法理论];

学科分类号：

摘要：

本文首先在命题逻辑的库所／变迁网模型中，提出四种新的证明目标命题成立的推理算法，即求包含目标变迁的Ｔ－不变量并同时求出变迁发生序列的算法，它们都源于归结反演系统中的改进策略．然后修改这些算法，并将它们推广到一阶谓词逻辑的谓词／变迁网模型中．这些算法都具有较高的效率，为逻辑推论的Ｐ／Ｔ网和Ｐｒ／Ｔ网模型的推理提供了新的有效的方法．

引用

页码：213 / 222

页数：10