一种算子命题逻辑系统及其T-不变量推理算法.pdfVIP

一种算子命题逻辑系统及其T-不变量推理算法 第六图书馆 定义一种只带原子命题以及命题算子的算子命题逻辑,讨论了该逻辑的λ-归结的相容性、完备性及其若干逻辑性质。为了实 现算子命题逻辑的归结推理。给出了算子命题逻辑的Petri网模型:Horn型,进一步讨论了推理算法:T-不变量算法,得到了算法 的完备性定理。定义一种只带原子命题以及命题算子的算子命题逻辑,讨论了该逻辑的λ-归结的相容性、完备性及其若干逻 辑性质。为了实现算子命题逻辑的归结推理。给出了算子命题逻辑的Petri网模型:Horn型,进一步讨论了推理算法:T-不变量 算法,得到了算法的完备性定理。λ-归结 Petri网 T-不变量 算子命题逻辑 归结推理模糊系统与数学夏世芬 徐 扬西南交通大学应用数学系,四川成都6100312007第六图书馆 第六图书馆 第 21卷第 6期 模 糊 系 统 与 数 学 VolI21．No．6 2007年 12月 FuzzySystemsandMathematics Dec．，2007 文章编号 ：1001—7402(2007)06—0018-06 一 种算子命题逻辑系统及其T一不变量推理算法 夏世芬 ，徐 扬 (西南交通大学 应用数学系 ，四川 成都 610031) 摘 要：定义一种只带原子命题以及命题算子的算子命题逻辑 ，讨论 了该逻辑的 一归结的相容性、完备 性及其若干逻辑性质 为 了实现算子命题逻辑的归结推理 。给 出了算子命题逻辑 的Petri网模型：Horn 型，进一步讨论 了推理算法：T一不变量算法 ，得到了算法的完备性定理。 关键词 ：一归结；Petri网；T一不变量 ；算子命题逻辑 ；归结推理 中图分类号 ：0141 文献标识码：A 自动推理及定理机器证明是人工智能理论和技术 中十分重要的研究课题。在 自动推理的研究 中，一个重要且很有前途的方 向是基于严密的逻辑基础建立相应推理理论和方法n ]，同时其它理 论与方法也深入 到 自动推理及定理机器证 明中如模糊逻辑 、神经网络、粗集理论 以及 Petri网 等L3]，共同推进人工智能向前发展。Petri网可以用于表示命题逻辑、一阶逻辑与模糊逻辑 一1， 第六图书馆 根据 Horn子句集的Petri网模型的T一不变量可以实现询问式推理L1。本文主要讨论基于Petri网 的算子命题逻辑系统 中自动推理方法的研究，为进一步研究基于非经典逻辑的定理 自动证明及其 应用软件的设计提供 了一定的理论和方法 。 1 算子命题逻辑系统OPL 定义 1．1 设 *，④及 是[0，1]上的两个二元运算以及一个一元运算，任取 日，b∈ro，1]，定义 ： *b--~-min{，b}， o b—max{，b}， 一 1一 日． 容易验证 (Eo，1]，*，o ，，0，1)是一个完备有余格 。 1．1 系统OPI的语言 (1)符号 系统OPI的符号包括下列五类 ：①命题变元集：x一 {户，q，r，…}；②个体常元集：L一 {0，1}； ③算子集 ：[0，1]；④逻辑连接词：V，^，～，一 ；⑤技术性符号 ：(，)。 (2)算子命题公式的构成 定义 1．2 设户是原子命题， ∈[O，1]，称 为命题原子，称 与～ ( )为命题文字，称 为命题算子 。 算子命题公式是如下递归定义的符号串：① 命题原子是算子命题公式；② 若 G是算子命题公 式 ，贝4～G是算子命题公式 ；③若G与 H是算子命题公式 ，则G ^H，GVH，G— H都是算子命 收稿 日期 ：2005—03—92；修订 日期：2006—06—06 基金项 目：国家 自然科学基金资助项 目(6047,t022)；西南交通大学基金资助项 目(2006B09) 作者简介 ：夏世芬(1968一)，女．西南交通大学应用数学系副教授 ．研究方向：Petri网。自动推理等；徐扬 (1956一)．男．西南交 通大