论文部分内容阅读
知识表示、知识推理和知识应用是人工智能的核心问题。目前，基于非经典逻辑的自动推理系统由于它加速了人工智能的发展而越来越引起人们的广泛重视。为了处理不同信息的推理，人们提出并发展了多种数学理论、方法和工具。如归结原理、经典逻辑、模糊逻辑、格值逻辑、Rough逻辑以及Petri网理论等，这些理论和方法为自动推理提供了强有力的支持。本文在自动推理领域中，进一步发展了现有的理论和方法，研究了基于Petri网模型的归结自动推理系统，并取得了如下主要研究成果： 1．给出了子旬集的矩阵表示形式，根据单文字规则与纯文字规则，讨论了矩阵的化简策略，并定义了子句集矩阵的初等变换，研究了变换的性质。根据Petri网中T-不变量推理判定法的思想，并结合输入归结、单元归结以及支撑归结，提出了多种矩阵归结的推理方法，证明了推理算法的完备性。 2．给出了基于Horn基子句集、一般基子句集和一阶Horn子句集的Petri网模型。根据Petri网中标识的流动规则，结合归结原理，给出了基于Petri网模型的删除归结推理算法，证明了算法的完备性。并将删除归结推理算法与T-不变量推理算法进行了比较，得到重要的结论：T-不变量推理算法简单，但使用范围有限，推理过程不直观；删除归结推理算法具有普适性，有直观的推理过程，推理具有高效性，结构表示具有简洁性等优点。这些研究结果为基于Petri网模型的归结自动推理提供了简单有效的推理方法。 3．提出了算子命题逻辑系统，讨论了算子命题逻辑系统中的λ-恒假、λ-归结以及λ-归结演绎等的逻辑性质，证明了λ-归结演绎的完备性。讨论了命题子句的极简规则型范式，给出了算子命题公式的Petri网模型，提出了算子命题逻辑系统中的两种归结推理算法—T-不变量推理算法与删除归结推理算法，证明了推理算法的完备性。 4．针对一类推理模型，提出了一种更一般的算子逻辑系统即算子模糊逻辑系统，讨论了算子模糊逻辑系统中的λ-归结以及λ-归结演绎的逻辑性质，给出了算子模糊逻辑系统中的提升引理，由此证明了λ-归结演绎的完备性。讨论了算子模糊逻辑系统中算子模糊子句的Horn型及一般型两种Petri网模型，给