共查询到17条相似文献,搜索用时 62 毫秒
1.
考虑到模糊逻辑中定理自动证明的重要性以及目前主要研究具有一种否定的模糊逻辑的归结原理,文中对具有三种否定(矛盾否定、对立否定和中介否定)的模糊命题逻辑(FLCOM)的归结原理进行研究.基于FLCOM的一种无穷值语义解释提出λ-可满足的和λ-不可满足的概念.将λ-归结方法引入FLCOM,给出FLCOM的λ-归结演绎定义,讨论FLCOM的λ-归结原理,并证明FLCOM的λ-归结方法的完备性.基于λ-归结方法和已证明的结论给出实例以佐证文中λ-归结方法和结论的正确性和可行性.因此,在FLCOM范围内可判定任一模糊命题公式是否是λ-可满足的或λ-不可满足的. 相似文献
2.
在模糊知识表示与推理中,否定信息扮演了一个重要角色.从概念层面上区分了模糊知识中存在的3 种否定关系,即矛盾否定关系、对立否定关系和中介否定关系.为了建立能够完全描述这些不同否定关系的逻辑基础,提出一种区分矛盾否定、对立否定和中介否定的模糊命题逻辑形式系统FLCOM.讨论了FLCOM 特有的性质与意义,给出了FLCOM 的一种语义解释,并证明了可靠性定理.为了表明FLCOM 处理实际问题的适用性,进一步研究了FLCOM在一个模糊决策实例中的应用.具体地,基于FLCOM讨论了决策规则中的模糊命题及其不同否定的区分与形式表示,给出一种确定模糊命题及其不同否定的真值及其真值范围阈值的方法,并采用模糊产生式规则讨论了实例中的模糊推理与决策.从而表明,运用FLCOM 处理具有模糊性并且存在不同否定的实际问题是有效的. 相似文献
3.
FLcom是建立在模糊集FScom基础上的一种区分矛盾否定、对立否定和中介否定的模糊命题逻辑形式系统。在模糊推理中关于否定的认识和处理主要以经典逻辑为基础,为此在FLcom基础上研究了区分3种否定的模糊推理规则的表示,给出了基于FLcom的模糊推理规则的合成算法FLMP和FLMT规则,新算法推广了CRI算法中的蕴涵算子,并给出了模糊推理应用的实例对比。结果表明FLcom在区分不同否定的实际应用中是合理可行的。 相似文献
4.
张胜礼 《计算机科学与探索》2014,(4):494-505
对于模糊知识及其否定关系,潘正华指出应该明确地分为矛盾否定关系、对立否定关系和中介否定关系,并建立了一种具有矛盾否定、对立否定和中介否定的模糊集FScom(fuzzy sets with contradictory negation, opposite negation and medium negation),随后建立了一种改进的模糊集IFScom(improved FScom)。为给模糊集FScom及其改进IFScom提供一种逻辑工具,提出了一种带有矛盾否定、对立否定和中介否定的模糊命题逻辑演算系统FPcom,并在给定无穷值语义赋值模型以及可满足性定义下,证明了FPcom具有可靠性和完备性。FPcom在一定意义上可视为对中介命题演算系统的改进。 相似文献
5.
蔡思思 《计算机光盘软件与应用》2013,(16):302-303
模糊描述逻辑的提出是针对现实生活中存在的模糊现象,而模态逻辑解决的是现实生活中具有的状态和状态转换现象等。将模态逻辑中的模态思想和模糊逻辑中的模糊理论相结合,同时结合描述逻辑,形成模态模糊描述逻辑(M-FALC)。考虑不同论域中的可能存在的模糊概念,关系,公式等,本文给出M-FALC的形式化公理体系及其推理,既能解决现实问题中的状态现象又解决模糊现象。 相似文献
6.
格值模态命题逻辑及其完备性 总被引:2,自引:0,他引:2
文中以满足第一及第二无限分配律的完备格为工具,建立了格值模态命题逻辑的语义理论,并指出这种语义是经典模态命题逻辑语义理论及[0,1]值模态命题逻辑语义理论的共同推广.给出了QMR0代数的定义,并分别以Boole代数及QMR0代数为背景构建了Boole型格值模态命题逻辑系统B及QMR0型格值模态命题逻辑系统QML*,并证明了系统B及系统QML*的完备性. 相似文献
7.
命题模态归结的一种变型 总被引:1,自引:1,他引:1
本文给出了模态子句集的标准子句集概念,提出了一种基于标准子句集的模态归结方法的变型,称之为标准模态归结,证明了任意模态子句集恒假当且仅当存在从它的标准子句集出发,使用标准模态归结推出空子句的演绎,从而证明了对于不可满足标准子句集、标准模态归结是完备的,这种标准模态归结,揄规则简单、直观且容易实现。 相似文献
8.
基于模糊命题模态逻辑的形式推理系统 总被引:4,自引:0,他引:4
探讨基于可信度的模糊命题模态逻辑的形式推理,给出相关的模糊Kripke语义描述.其研究目的旨在解决基于模态命题逻辑的模糊推理的能行问题.在研究过程与方法上,以完全形式化的方法将模糊模态逻辑语法和语义统一在一个形式系统中,以模糊约束作为基本表达式,给出推理规则,建立了相应的模糊推理形式系统,并以形式系统中模糊约束集的可满足性来表示模糊推理的有效性,使模糊推理过程变得容易,为最终在计算机上实现基于模态逻辑的模糊推理打下了一定的基础.主要结论是证明了基于可满足性的模糊推理形式系统的可靠性与完备性. 相似文献
9.
10.
经典命题演算形式系统(CPC)中的公式只是一些形式符号,这些形式符号的意义是由具体的解释给出的.概率逻辑是在标准概率空间上建立的一种逻辑体系,是CPC的随机事件语义,对联结词的解释就是集合运算,对形式公式的解释就是事件函数,对逻辑蕴涵和逻辑等价的解释就是事件(集合)包含和事件相等=.由于不存在处处适用的真值函数(算子),概率逻辑不能在CPC内实现概率演算,但可在CPC内实现事件演算,CPC完全适用于概率命题演算. 相似文献
11.
研究基于可信度的模糊一阶模态逻辑,给出了基于常域的模糊一阶模态逻辑语义以及推理形式系统描述.为有效进行模糊断言间的推理,考虑了模糊约束的概念.模糊约束是一个表达式,其中既有语法成分又包含意义信息.模糊推理形式系统中的基本对象是模糊约束,针对模糊约束引进可满足性概念,研究模糊约束可满足性相关性质.利用模糊约束的概念,模糊断言间的推理可以直接在语义环境下加以考虑,因此,以模糊约束为基本元素的模糊推理形式系统随之建立.主要分析新产生断言有效性与模糊约束集可满足性之间的关系,并在此基础上给出了模糊推理形式系统的推理规则.进一步的工作可探讨模糊推理形式系统的可靠性与完全性,建立推理过程的能行机制.研究结果可在人工智能和计算机科学等领域得以应用. 相似文献
12.
Decidability by Resolution for Propositional Modal Logics 总被引:1,自引:0,他引:1
Renate A. Schmidt 《Journal of Automated Reasoning》1999,22(4):379-396
The paper shows that satisfiability in a range of popular propositional modal systems can be decided by ordinary resolution procedures. This follows from a general result that resolution combined with condensing, and possibly some additional form of normalization, is a decision procedure for the satisfiability problem in certain so-called path logics. Path logics arise from normal propositional modal logics by the optimized functional translation method. The decision result provides an alternative method of proving decidability for modal logics, as well as closely related systems of artificial intelligence. This alone is not interesting. A more far-reaching consequence of the result has practical value, namely, many standard first-order theorem provers that are based on resolution are suitable for facilitating modal reasoning. 相似文献
13.
14.
15.
Peter Balsiger Alain Heuerding Stefan Schwendimann 《Journal of Automated Reasoning》2000,24(3):297-317
A lot of methods have been proposed – and sometimes implemented – for proof search in the propositional modal logics K, KT, and S4. It is difficult to compare the usefulness of these methods in practice, since in most cases no or only a few execution times have been published. We try to improve this unsatisfactory situation by presenting a set of benchmark formulas. Note that we do not just list formulas, but give a method that allows us to compare different provers today and in the future. As a starting point we give the results we obtained when we applied this benchmark method to the Logics Workbench (LWB). We hope that the discussion of postulates concerning ATP benchmark helps to obtain improved benchmark methods for other logics, too. 相似文献
16.
We explain Stålmarck's proof procedure for classical propositional logic. The method is implemented in a commercial tool that has been used successfully in real industrial verification projects. Here, we present the proof system underlying the method, and motivate the various design decisions that have resulted in a system that copes well with the large formulas encountered in industrial-scale verification. 相似文献
17.
在基于命题逻辑的可满足性问题(SAT)求解器和基于一阶逻辑的定理证明器上,子句集简化一直是必不可少的步骤,而其中子句消去方法在这些子句集简化方法中是非常重要的组成部分。将命题逻辑中的子句消去方法归结隐藏恒真消去方法(RHTE)和归结隐藏包含消去方法(RHSE)提升到一阶逻辑上,并且利用蕴含模归结原则(IMR)证明了这种提升方式在一阶逻辑上具有可靠性(Soundness),即依据这两种子句消去方法删除一阶逻辑公式集中的子句,并不会改变公式集的可满足性或者不可满足性。此外,将这两个方法与一阶逻辑子句消去方法锁子句消去方法(BCE)和归结包含消去方法(RSE)进行组合推广,发展得到一阶逻辑上新型子句消去方法(BC+RHS)E、(RS+RHT)E和(RHS+RHT)E,并且证明了这3种子句消去方法在一阶逻辑上的可靠性。最后,分析比较了这些子句消去方法的有效性,并且证明了这3种新型子句消去方法比组成它们的原始子句消去方法均具有更高的有效性。 相似文献