关于Henschen和Wos推测的证明

Ｈｅｎｓｃｈｅｎ和 Ｗｏｓ在［２］中的定理 １和定理 ２分别证明了不可满足的 Ｈｏｒｎ集有严 格－正的－单元反驳和严格－输入反驳，如果子句（ｃｌａｕｓｅ）集合Ｓ是一个Ｒ－不可满足的 Ｈｏｒｎ集，该集合包含子句Ｒｘ，ｘ和它的函数反身公理，当Ω由调换（ｐａｒａｍｏｄｕｌａｔｉｏｎ）、 归结（ｒｅｓｏｌｕｔｉｏｎ）和因子（ｆａｃｔｏｒｉｎｇ） 三个推理规律组成时，Ｈｅｎｓｃｈｅｎ 和 Ｗｏｓ在［２］中的 定理 ３证明了：利用这三个推理规律从该子句集可以得到一个输入反驳（ｉｎｐｕｔ ｒｅｔｕｔａｔｉｏｎ） Ｄ１和一个单元反驳（ｕｎｉｔ ｒｅｆｕｆａｔｉｏｎ）Ｄ２，而且他们认为如 Ω’由调换和归结两个规律 组成时，利用这二个规律从上述子句集合有可能得到一个严格－正的－单元反驳和一个 严格－输入反驳，本文证明了这一估计是对的。     

Horn集上的语义正单元归结

Ｌ． Ｈｅｎｓｃｈｅｎ证明了语义归结对 Ｈｏｒｎ集是完备的［１］。但是语义归结不是正单元归结。本文的主要结果是不可满足的Ｈｏｒｎ子句集合Ｓ有这样一个反驳，对于这个反驳的每一个归结来说，或者一个祖先子句是正单元，而且该正单元在 Ｉ上是假的；或者一个祖先子句是正单元，而且从另一个祖先子句和这个归结式中删去他们的正义字后剩下的子句在 Ｉ上都是假的．其中 Ｉ是 Ｓ的任何一个解释。     

自动定理证明中RUE-NRF单元输入和锁的演绎

本文在RUE-NRF推理规则的基础上,定义了RUE-NRF输入归结、RUE-NRF单元归结及RUE-NRF锁归结的概念,证明了RUE-NRF输入反驳与RUE-NRF单元反驳的关系,以及RUE-NRF锁反驳的完备性。     

在最坏情况下Horn集上的单元反驳长度

１９７４年Ｃｏｏｋ和Ｒｅｃｋｂｏｗ讨论了命题演算中的证明长度。本文作者曾讨论了最好情况下基本Ｈｏｒｎ集上的单元反驳与输入反驳长度及最坏情况下基本Ｈｏｒｎ集上的输入反驳长度。本文讨论了在最坏情况下基本Ｈｏｒｎ集上的单元反驳长度上界．这一上界对某些Ｈｏｒｎ集来说是可达到的．     

RUE-NRF演绎与使用归结和调解的演绎

本文证明了在一定条件下,RUE-NRF演绎可以重写为使用归结和调解的演绎;通过反例说明RUE-NRF输入反驳与RUE-NRF单元反驳不等价及RUE-NRF线性反驳的不完备性.     

格值命题逻辑系统Ln ×2P(X)中广义文字的α-归结性

归结自动推理是人工智能领域的一个重要研究方向.以格蕴涵代数为真值域的格值逻辑中的α-归结方法提供了一种处理带有模糊性和不可比较性信息的自动推理问题的工具,能对格值逻辑系统的α-不可满足子句集给出反驳证明,用α-归结原理证明格值逻辑中广义子句集的α-不可满足性,必须首先研究两个广义文字是否可以进行α-归结.研究了格值逻辑...     

一种新的输入格式

采用消解法的定理证明程序,通常都是按子句格式输入。该格式虽然便于消解,但是它与普通逻辑公式或者日常语句差异皆较大,因此运用时相当不便。 为了兼备日常用语及子句格式的优点,本文提出一种新的输入格式——公式子句格式。简记为FC格式。该格式不仅接近于日常的判断语句,而且不难转换为子句格式,     

并行单元归结

给出了基于神经网络的单元归结算法.首先将子句集S表示为δ形,并且用算子对(⊙, )引入两种类型的神经元,然后用这两种神经元构造子句集S的神经网络结构,而后给出基于Horn子句集的神经网络的归结算法,最后证明了该算法的完备性,并用实例进行了验证.     

基于子句抽取的文本摘要自动提取算法

TextRank算法及SWTextRank等改进算法在抽取式摘要生成中得到了广泛的应用,但它们都没有有效地解决抽取式摘要所存在的冗余性问题。为此,提出一种基于子句抽取的文本摘要自动提取算法（PTextRank）。首先,使用Sinica Treebank(STB)对每个句子进行语法标记,进而基于子句设置抽取单元;接着,使用BERT(Bidirectional Encoder Representation from Transformers)构建标题和每个子句的特征向量,并计算子句特征向量间的相似性,将其存放在相似度矩阵中;最后结合子句位置、子句与标题的相似度等调整子句相似度矩阵,迭代计算直至收敛,进而选取得分最高的子句作为最终摘要。实验分析表明,PTextRank算法有效地避免了多个句子中存在的冗余信息,且相比于TextRank和SWTextRank,PTextRank生成摘要的准确率至少提高6%,同时生成的摘要质量更好。     

基于重启策略的学习子句优化方法

以学习子句数据库优化为背景，在原MiniSAT求解器的基础上提出了一种新的学习子句的优化方法.该方法基于博弈论的思想，在若干次重启后，根据当前求解器的实时反馈信息改进MiniSAT原有的增长参数，尽可能靠近学习数据库中子句存储量的均衡点，从而使学习库的存储量尽可能达到Pareto最优.实验表明:所提的优化方法是有效的，并在随机SAT问题上胜过现有优化方法.该方法既不会因为学习数据库的子句过多而影响单元传播速度，也不会因为学习数据库中的子句过少而破坏学习的整体性.     

谓词公式输入的定理证明

子句格式是广泛采用的定理证明的一种输入格式,然而,人们从抽象实际问题中得到的却常常是谓词公式。因此使用谓词公式直接输入来做定理证明是相当有意义的。作者于1984年2月以LISP语言的形式在PDP11/03微机上实现了这种输入格式的定理     

命题知识库演化中的新知识特征（英文）

逻辑差概念在表征基于逻辑的知识库中起到重要作用,这些知识库持续受到动态变化的影响,它们之间存在实质性差异。这一概念与遗忘密切相关,它在各种逻辑中得到了广泛探讨。针对命题理论的相关符号,提出了3种差概念——逻辑差异、子句差异和素子句差异,以分别捕获逻辑推理、子句推理和素子句推理的差异;研究了它们的性质和计算复杂性。结果表明,涉及逻辑差的各种决策问题在多项式层次结构中比相应的可满足性问题高一个层次,除了2-CNF理论,其相关决策问题是易处理的。随机3-CNF、2-CNF和Horn理论的大量实验结果揭示了子句差和素子句差的一些有趣现象：在随机3-CNF理论和2-CNF理论中,子句和素子句差的子句数量都表现出与它们的可满足性类似的相变特征。然而,在随机Horn理论中,尽管子句差的子句数量表现出与其可满足性类似的相变,但素子句差的子句数量与子句差情形十分不同,这些结果揭示了随机命题知识库演化中其可满足性相变现象的新特征：在相变阈值附近的知识库演变会产生更多的差异。     

基于逗号的汉语子句识别研究

根据篇章分析的任务和实践, 结合传统研究, 提出汉语的基本篇章单位为子句, 并从结构、功能、形式等方面给出其定义。分析了逗号与子句的关系, 并在标注语料上进行了基于逗号的汉语子句识别研究。首先手工标注了CTB6.0中前100篇文档的逗号是否为子句边界的信息, 在标注结果中抽取句法、词汇、长度等特征进行实验, 子句识别准确率为90%。然后利用信息增益选出贡献最大的9个特征, 使用它们也可获得较高的子句识别准确率。最后仅使用词法信息, 子句识别准确率可达84.5%。实验证明子句的定义合理, 基于逗号的子句识别在理论上和实验上均可行。     

判断基本子句集合不可满足性的一个方法

一个子句(或基本子句集合)的非模型是不满足该子句(或基本子句集合)的解释.本文给出计算有限基本子句集合的非模型个数的一种方法,并使用概率的观点从理论上加以证明.     

使用引理的锁语义归结原理——LI-归结原理

为了改进对于一阶逻辑中子句集是完备的2型IDI-归结原理的一个缺点,即在IDI归结中,只对其中一个亲本子句的归结文字有所限制,对另一个亲本子句的归结文字没有任何限制,本文提出了锁语义归结,简称LI-归结。即在这种语义归结原理中,象锁归结过程一样,每一次归结的两个亲本子句中的归结文字,都是该子句中有最小锁的文字,并证明了以一种固定的配锁方法,LI-归结原理对于一阶逻辑中的子句集是完备的。 使用引理的概念,将LI-演绎进行线性整理,从而引进了TLI-演绎的概念。     

级联型中高压变频器主电路结构及工作原理

级联型中高压变频器将若干个独立的低压功率单元的输出串联,实现高压输出。电网电压经过移相变压器降压后给功率单元供电,每个功率单元分别由输入隔离变压器的一个二次绕组供电,变压器二次绕组之间相互绝缘。功率单元为三相输入的整流电路和单相输出的交-直-交电压源型逆变器结构,将相邻的功率单元串联起来构成单相,三相输出Y型联结。     

re-Horn子句集的Horn化及可满足性判定方法

在命题逻辑中给出将re-Horn子句转化成Horn子句的条件与方法,用同态的方法证明转化前后2个子句集的可满足性或不可满足性的一致性,给出re-Horn子句集的可满足性的判定方法。     

Horn集上的HOI消解与HOL消解

OI消解法对一般子句集是不完备的,甚至对基子句集都不完备,多年来,人们在寻求提高消解效率方面作了许多努力,诸如改进消解策略、限制不可满足的子句集等。Renschen与Wos提出了一类子句集,称Horn集,许多机器证明问题都可归结为     

有限元法的数化仪输入

采用数化仪直接输入有限元结构分析的网格图数据有很大的优越性,它避免了采用一般的间接输入方式时可能出现的差错。 本文论述了利用数化仪输入图形的基本概念,并介绍了笔者开发的数化仪前处理程序GNDGTZ的主要功能。着重讨论了几个关键问题,即第3座标的输入、结点的生成、结点的即时显示、单元的数化、空间模型的单元输入和单元的生成。     

子句级别的自注意力机制的情感原因抽取模型

情感原因抽取(ECE)是情感分析领域的一项重要子任务,旨在识别给定文档中某种情绪表达所对应的原因.现有的一些工作将该任务定义为子句分类任务,关注了文档和子句之间的联系,而忽略情感描述子句与情感原因子句的直接语义联系,同时存在标签不平衡问题,使得情感原因子句位置难以定位.因此,提出了一个基于子句的自注意力机制同时结合了子...