探索基于petri网模型的归结自动推理研究

《探索基于petri网模型的归结自动推理研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、西南交通大学博士学位论文基于Petri网模型的归结自动推理研究姓名：夏世芬申请学位级别：博士专业：交通信息工程及控制指导教师：徐扬20061201西南交通大学博士研究生学位论文第1页摘要知识表示、知识推理和知识应用是人工智能的核心问题。目前，基于非经典逻辑的自动推理系统由于它加速了人工智能的发展而越来越引起人们的广泛重视。为了处理不同信息的推理，人们提出并发展了多种数学理论、方法和工具。如归结原理、经典逻辑、模糊逻辑、格值逻辑、Rough逻辑以及Petri网理论等，这些理论和方法为自动推理提供了强有力的支持。本文在自动推理领域中，进一步发展了现有的理论和方法，研究了基于Petri网模型的归

2、结自动推理系统，并取得了如下主要研究成果：1．给出了子旬集的矩阵表示形式，根据单文字规则与纯文字规则，讨论了矩阵的化简策略，并定义了子句集矩阵的初等变换，研究了变换的性质。根据Pe矗网中T_不变量推理判定法的思想，并结合输入归结、单元归结以及支撑归结，提出了多种矩阵归结的推理方法，证明了推理算法的完备性。2．给出了基于Horn基子句集、一般基子句集和一阶Horn子句集的Petri网模型。根据Petd网中标识的流动规则，结合归结原理，给出了基于Petri网模型的删除归结推理算法，证明了算法的完备性。并将删除归结推理算法与T-不变量推理算法进行了比较，得到重要的结论：T-不变量推理算法简单，但

3、使用范围有限，推理过程不直观；删除归结推理算法具有普适性，‘有直观的推理过程，推理具有高效性，结构表示具有简洁性等优点。这些研究结果为基于Petfi网模型的归结自动推理提供了简单有效的推理方法。3．提出了算子命题逻辑系统，讨论了算子命题逻辑系统中的名-恒假、A-归结以及旯．归结演绎等的逻辑性质，证明了彳．归结演绎的完备性。讨论了命题子旬的极简规则型范式，给出了算子命题公式的Petri网模型，提出了算子命题逻辑系统中的两种归结推理算法一T_不变量推理算法与删除归结推理算法，证明了推理算法的完备性。4．针对一类推理模型，提出了一种更一般的算子逻辑系统即算子模糊逻辑系统，讨论了算予模糊逻辑系统中

4、的丑．归结以及五．归结演绎的逻辑性质，给出了算子模糊逻辑系统中的提升引理，由此证明了五．归结演绎的完备性。讨论了算子模糊逻辑系统中算子模糊子句的Horn型及一般型两种Petri网模型，给第Ⅱ页西南交通大学博士研究生学位论文出了基于表示模型的T-不变量推理算法和删除归结推理算法，证明了推理算法的完备性。所有这些表示方法和推理算法，为模糊逻辑系统的推理提供了新的方法与思路。5．为了进一步研究非经典逻辑系统的自动推理，特别是较直观的推理形式，给出了格值命题逻辑系统LP(X)中公式的Petd网模型及基于Petri网模型的归结推理算法。讨论了格值命题逻辑系统LP()()中公式的规则型范式，定义了极简

5、规则型子句的MP归结以及(4，口)．归结演绎，证明了归结演绎的可靠性与弱完备性。讨论了极简规则型子句集的Petri网模型以及任意公式的Petri网模型。详细给出了四值非链格值命题逻辑系统LP400的Petri网推理模型及推理算法，进一步给出了格值命题逻辑系统LP(X)中公式的Petri网推理模型以及基于Petri网模型的T-不变量推理算法和可达性推理算法，证明了推理算法的完备性，得到了有意义的结论，从而为研究格值命题逻辑系统中的自动推理提供了切实可行的方法。关键词：Petri网；归结推理；算子命题逻辑：算予模糊逻辑：格值命题逻辑西南交通大学博士研究生学位论文第lII页AbstractThe

6、reisnodenyingthat∞prcsem鲥on，refe枷∞andapplicationofknowledgearekeyquestionsinartificialintelligence．Inrecentyears,automateddeductionbasedonnon-classicallogics,whichspeedupthedevelopmentofartificialintelligence,hasattractedmanyresearch盯’Sattention．Inordertodeal晰tllinferenceofdifferentinformation,peo

7、plehas—oposedanddevelopedmanymathematicaltheories,methodsandtools，suchastheoryofresolution，classicallogic，fuzzylogic,lattice-valuedlogic，Roughlogic，PetrinetandSOon．Thesetheoriesandmethodsplayallimportantroleinpro