共查询到19条相似文献,搜索用时 54 毫秒
1.
归结原理(resolution principle)是计算机自动推理的重要原理之一。将XML加入到使用归结原理的证明过程中,利用XML结构与语义自描述的特性,简化归结过程的计算机实现,并给出相应基于XML的算法。 相似文献
2.
算子Rough逻辑及其归结原理 总被引:6,自引:2,他引:6
本文基于Rough集理论定义了算子η及其合成运算,并用它作用于Rough逻辑公式,从而得到了带算子的Rough逻辑.讨论了这种逻辑公式的真值、语义模型、性质、归结原理及完备性定理和它的证明. 相似文献
3.
归结演绎推理是一种在计算机上得到较好实现的基于归结原理的推理技术,介绍归结原理的基本思想以及它在自动推理中的应用。 相似文献
4.
进一步深入研究了基于格蕴涵代数的格值一阶逻辑系统 LF(X )的多元α-归结原理的基本理论,给出了在基于 LF(X )的多元α-归结演绎中参与多元α-归结的广义文字个数随着归结演绎的推进而动态变化的基本原则。对基于 LF(X )的多元α-归结原理的有效性进行了一定分析;这为建立基于 LF(X )的多元α-归结方法以及构造多元α-归结算法建立了理论基础。 相似文献
5.
Cialdea一阶模态归结系统的不完备性及其改进 总被引:4,自引:1,他引:3
Cialdea的-阶模态D逻辑归结系统具有符号冗余较少和机器上较容易实现等优点,但它是不完备的。本文中,我们改进了Cialdea归结系统,引入了两个可能算子约束的公式间的归结规则,得到了一种新的一阶模态D逻辑的归结系统,记为FMRD.FMRD很好地保持了Cialdea归结系统的优点,同时,我们证明了FMRD的可靠性与完备性。 相似文献
6.
主要讨论DFL谓词描述下的归结推理方法,它是一种机器化的可在计算机上加以实现的推理方法。首先介绍DFL命题下结方法。最后介绍DFL的归结原理及方法。 相似文献
7.
中介谓词逻辑系统的λ-归结 总被引:9,自引:0,他引:9
给出中介逻辑谓词演算系统MF的一种无穷值语义解释,即无穷值的(解释,将λ-归结方法引入到MF中,讨论了MF的λ-归结原理,并证明了它的完备性. 相似文献
8.
潘给出的中介谓词逻辑系统MF的无穷值语义解释,不同于MF的其他任何语义解释。但在该无穷值语义解释下,“当A fuz时~A真”这种情况并未得到反映,并且该解释在模糊知识推理中必须作适当的修改才能更符合客观思维。给出了中介谓词逻辑系统MF一种真值域为(0,1-λ)[∪](1-λ,λ)[∪](λ,1)(λ[∈](0.5,1))的无穷值语义解释,重新定义了MF的文字,提出了一种新的MF的λ-归结原理,证明了其完备性。该解释进一步表明用中介逻辑作为模糊知识的表示与推理的工具是可行的。 相似文献
9.
10.
1973年,Chang和Lee将线性归结与有序归结相结合,提出了有序线性归结,即OL归结,极大地提高了线性归结的效率和机械性。然而,OL归结并不是一种完备的归结方法。在OL归结的约化条件的基础上提出了强约化的概念。强约化条件对中心有信息有序子句的约化做了进一步的限制,且该强约化条件是约化条件的一种特例。在强约化条件的基础上,还提出了一种改进的OL归结——SOL归结,并证明了其完备性。 相似文献
11.
12.
13.
14.
Part machining is a discrete manufacturing process. In order to evaluate the manufacturing process, an intelligent modeling method based on the first-order predicate logic is proposed. First, the basic predicate formula is defined according to the machining method, and the predicate and variables are illustrated in detail. Thus, the process representation is completed. Second, to construct the process model, the modeling element is put forward, which includes three nodes. Components of modeling element are, respectively, discussed, as well as the mapping relationship between modeling element and predicate. After the definition of modeling predicate formula, five basic inference rules are established. Consequently, the manufacturing process model is constructed. Third, on the basis of the process model, the process simulation is carried out to evaluate the manufacturing performances, such as the production efficiency, the utilization rate of machining equipment, the production bottleneck, etc. Finally, a case study is conducted to explain this modeling method. 相似文献
15.
Albert Visser 《Journal of Logic, Language and Information》1998,7(1):21-52
In this paper we introduce a notion of context for Groenendijk & Stokhof's Dynamic Predicate Logic DPL. We use these contexts to give a characterization of the relations on assignments that can be generated by composition from tests and random resettings in the case that we are working over an infinite domain. These relations are precisely the ones expressible in DPL if we allow ourselves arbitrary tests as a starting point. We discuss some possible extensions of DPL and the way these extensions interact with our notion of context. 相似文献
16.
由于必然模态词□的引入,谓词模态逻辑的公式在一个可能世界中的真假值可能依赖于其可达的可能世界.在谓词模态逻辑中存在个体跨可能世界相等问题.针对这一问题,Lewis提出了对应物理论,并且在对应物理论中用对应物关系来表示个体跨可能世界相等.但是,当一个对象具有一个以上的对应物时,谓词模态逻辑中的跨可能世界相等关系无法与对应物关系建立一一对应.通过限制谓词模态逻辑中全称量词∀的范围,给出了一种公式分层的谓词模态逻辑.它是谓词模态逻辑的一个子逻辑,并且其语言与谓词模态逻辑的语言是相同的.但其公式是分层定义的,使得∀可以出现在□的范围内,并且□不能出现在∀的范围内.由于任意形如∀x□φ(x)的表达式都不是该逻辑的公式,以量词开头的公式在一个可能世界w中的真假值只依赖于w,该逻辑避免了个体跨可能世界相等问题.给出了该逻辑的语言、语法和语义,并证明了该逻辑是可靠的和完备的. 相似文献
17.
《离散数学》谓词逻辑中前柬范式的求解一直是一个难点。对前柬范式求解步骤进行分析和总结,对两种换名规则和换名情况进行分类和研究.结合实例帮助学生更好地掌握整个前束范式的求解过程,并在实际教学过程中起到很好的教学效果。 相似文献
18.
利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高. 相似文献
19.
Stefano Ferilli 《Journal of Intelligent Information Systems》2016,47(1):33-55
Three relevant areas of interest in symbolic Machine Learning are incremental supervised learning, multistrategy learning and predicate invention. In many real-world tasks, new observations may point out the inadequacy of the learned model. In such a case, incremental approaches allow to adjust it, instead of learning a new model from scratch. Specifically, when a negative example is wrongly classified by a model, specialization refinement operators are needed. A powerful way to specialize a theory in Inductive Logic Programming is adding negated preconditions to concept definitions. This paper describes an empowered specialization operator that allows to introduce the negation of conjunctions of preconditions using predicate invention. An implementation of the operator is proposed, and experiments purposely devised to stress it prove that the proposed approach is correct and viable even under quite complex conditions. 相似文献