共查询到18条相似文献,搜索用时 734 毫秒
1.
归结方法是定理自动证明的重要工具。为了简化直觉模糊命题逻辑的归结过程,基于直觉模糊命题逻辑归结原理的一般形式,提出了子句(αβ)-可满足和(αβ)-归结式的概念。研究了广义子句与其归结式的可满足性。在直觉模糊命题逻辑系统中给广义子句配锁,规定在做归结时各子句中被消去文字在该子句中的序号最小,由此建立了(αβ)-广义锁归结方法,并证明了该方法的可靠性和完备性。给出了直觉模糊逻辑的广义锁归结算法步骤,并通过实例说明了该方法的有效性。 相似文献
2.
3.
广义模糊逻辑和锁语义归结原理 总被引:9,自引:0,他引:9
将命题的真值取在格上的模糊逻辑,我们称为广义模糊逻辑。本文讨论了这种广义模糊逻辑的性质,并证明了,对于一阶谓词公式,在广义模糊逻辑中的不可满足性和在二值逻辑中的不可满足性是等价的。还证明了原始的归结原理在广义模糊逻辑中是完备的。 最后,在模糊逻辑中讨论了涉及子句真值的语义归结原理,对于在广义模糊逻辑中的不可满足配锁子句集,在任意一个模糊解释下,使用语义归结原理,总可演绎出空子句。 相似文献
4.
命题模态归结的一种变型 总被引:2,自引:1,他引:1
本文给出了模态子句集的标准子句集概念,提出了一种基于标准子句集的模态归结方法的变型,称之为标准模态归结,证明了任意模态子句集恒假当且仅当存在从它的标准子句集出发,使用标准模态归结推出空子句的演绎,从而证明了对于不可满足标准子句集、标准模态归结是完备的,这种标准模态归结,揄规则简单、直观且容易实现。 相似文献
5.
检测和消除命题逻辑公式中的冗余文字,是人工智能领域广泛研究的基本问题。针对命题逻辑的子句集中子句的划分,结合冗余子句和冗余文字的概念,将命题逻辑的子句集中的文字分为必需文字、有用文字和无用文字3类,并分别给出其定义。讨论3种文字与无冗余等价子集的性质,给出其等价子集的等价描述方法。得到题逻辑的子句集中必需文字、有用文字和无用文字的判定方法,借助子句集的可满足性得到3种文字与子句集的可满足性的等价条件。上述结果对命题逻辑中文字属性的判断提供了多种可选择方法,同时为命题逻辑公式的化简奠定了理论基础。 相似文献
6.
一阶逻辑定理证明是人工智能的核心基础,研究一阶逻辑自动定理证明器的相关理论和高效的算法实现具有重要的学术意义。当前一阶逻辑自动定理证明器首先通过子句集预处理约简子句集规模,然后通过演绎方法对定理进行判定。现有的应用于证明器中的子句集预处理方法普遍只从与目标子句项符号相关性角度出发,不能很好地从文字的互补对关系中体现子句间的演绎。为了在子句集预处理时从演绎的角度刻画子句间的关系,定义了目标演绎距离的概念并给出了计算方法,提出了一种基于目标演绎距离的一阶逻辑子句集预处理方法。首先对原始子句集进行包含冗余子句约简并应用纯文字删除规则,然后根据目标子句计算剩余子句集中的文字目标演绎距离、子句目标演绎距离,并最终通过设定子句演绎距离阈值来实现对子句集的进一步预处理。将该预处理方法应用于顶尖证明器Vampire,以2017年国际一阶逻辑自动定理证明器标准一阶逻辑问题组竞赛例为测试对象,在标准的300 s内,加入提出的子句集预处理方法的Vampire4.1相比原始的Vampire4.1多证明4个定理,能证明10个Vampire4.1未证明的定理,占其未证明定理总数的13.5%;在证明的定理中,提出的子句集预处理方法能对77.2%的子句集进行约简,最大子句集约简规模达到51.7%。实验结果表明,提出的一阶逻辑子句集预处理方法是一种有效的方法,能有效地约简一阶逻辑子句集的规模,提高一阶逻辑自动定理证明器的证明能力。 相似文献
7.
给出了格值命题逻辑系统L9P(X)上的放缩原理和放缩归结原理,基于放缩归结原理,给出了一种判断L9P(X)上子句集S为M-可满足的自动推理算法(这里M为L9上的中界元),并证明了其可靠性和完备性。 相似文献
8.
RLD演绎及子句蕴含与子句包含关系的非等价性 总被引:1,自引:1,他引:1
软件复用的一个主要任务是可复用软件构件的表示与检索,由于一阶逻辑能够描述软件构件的计算语义,因此用一阶逻辑表示构件及用基于归结原理的自动定量证明技术检索构件的研究在软件工程领域得到了足够的重视,为了简化基于演绎的构件检索技术的程序设计结构及提高演绎效率,提出了最右线性演绎RLD(rightmost linear deduction),并证明了它的完备性,同时,指出了子句蕴含与子句包含关系的非等价性,并给出了由子句蕴含关系推出子句包含关系成立的一个充分条件。 相似文献
9.
主要研究命题逻辑公式中的冗余子句和冗余文字。针对子句集中必需的、有用的、无用的子句,分别给出了一些等价描述方法,进而讨论子句集的无冗余等价子集。另外,得到了子句集中冗余文字的判别方法,借助可满足性给出了冗余子句的一种等价条件。上述结果为命题逻辑公式的化简奠定了一些理论基础。 相似文献
11.
以一阶谓词逻辑为基础,讨论约束满足问题.着重研究一阶逻辑公式可满足性的局部搜索法,并与命题逻辑中的可满足性过程加以比较.以皇后问题和哈密顿回路问题为例,说明基于一阶逻辑的方法能处理较大的问题实例. 相似文献
12.
Extended IF 逻辑是一阶逻辑的扩张,其主要特点是可表达量词间的相互依赖和独立关系,但其命题部分至今没有得到公理化.基于Cirquent 演算方法,给出了一个关于Cirquent 语义(命题水平)可靠完备的形式系统.该系统能够很好地解释和表达命题联结词间的相互依赖和独立关系,从而使Extended IF 逻辑在命题水平得到了真正意义上的公理化. 相似文献
13.
Paolo Liberatore 《Artificial Intelligence》2008,172(11):1317-1359
14.
Marin Vlada 《Artificial Intelligence Review》2001,15(3):153-163
The present paper presents algorithms for testing satisfiabily of clausalformulas in the propositional logic and the firs-order logic. The algorithmbased on the enumeration of solutions for testing the satisfiability ofpropositional formula, has already been given by K. Iwama, O. Dubois. Theoriginality in this paper is to combine this algorithm to other procedures,especially with the pure-literal literal and the one-literal rule, and also theone which consists in changing any formulas in formulas bounded. Thealgorithm based on the enumeration of the solution combined to theseprocedures is more efficient. The algorithm based on the concept ofresolutive derivation from Skolem normal form of formula in first-order logic, has already been given. The idea in present's paper is tocombined to this algorithm to process of elimination of tautological clausesand process of elimination of subsumed clauses. 相似文献
15.
Allen Van Gelder Fumiaki Okushi 《Annals of Mathematics and Artificial Intelligence》1999,26(1-4):113-132
This paper describes new “lemma” and “cut” strategies that are efficient to apply in the setting of propositional Model Elimination.
Previous strategies for managing lemmas and C-literals in Model Elimination were oriented toward first-order theorem proving.
The original “cumulative” strategy remembers lemmas forever, and was found to be too inefficient. The previously reported
C-literal and unit-lemma strategies, such as “strong regularity”, forget them unnecessarily soon in the propositional domain.
An intermediate strategy, called “quasi-persistent” lemmas, is introduced. Supplementing this strategy, methods for “eager”
lemmas and two forms of controlled “cut” provide further efficiencies. The techniques have been incorporated into “Modoc”,
which is an implementation of Model Elimination, extended with a new pruning method that is designed to eliminate certain
refutation attempts that cannot succeed. Experimental data show that on random 3CNF formulas at the “hard” ratio of 4.27 clauses
per variable, Modoc is not as effective as recently reported model-searching methods. However, on more structured formulas
from applications, such as circuit-fault detection, it is superior.
This revised version was published online in June 2006 with corrections to the Cover Date. 相似文献
16.
This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14, 329–353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural deduction system for first-order hybrid logic can be extended with additional inference rules corresponding to conditions on the accessibility relations and the quantifier domains expressed by so-called geometric theories. We prove soundness and completeness and we prove a normalisation theorem. Moreover, we give an axiom system first-order hybrid logic. 相似文献
17.
18.
Robert E. Shostak 《Artificial Intelligence》1976,7(1):51-64
A graph-theoretic characterization of truth-functional consistency is introduced, providing a clear perspective on some resolution-based for deciding formulas in propositional and first-order logic. Various resolution strategies are analyzed in terms of “walks” about specially defined graphs. A new procedure—called Graph Construction—is presented that improves on the Model Elimination and SL strategies. 相似文献