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

摘要：

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

关键词： Petri网 谓词变迁系统 一阶谓词公式 逻辑联结词 二叉树 事实变迁 递归性质 自动化建模

作者: 耿霞 吴哲辉 张继军

作者单位: 山东农业大学信息科学与工程学院 山东泰安 271018;山东科技大学信息科学与工程学院 山东青岛 266510 山东科技大学信息科学与工程学院 山东青岛 266510 山东农业大学信息科学与工程学院 山东泰安 271018

会议类型: 国内会议

会议名称: 第十一届全国Petri网理论与应用学术年会

会议地点: 大连

会议语种:中文

页码: 9-15

在线出版日期: 2007-08-01（万方平台首次上网日期，不代表论文的发表时间）