极小不可满足核及其提取

在极小不可满足公式和可满足公式的基础上给出极小不可满足核的定义,并给出用布尔可满足求解器提取不可满足公式的极小不可满足核的方法。     

一个极小不可满足公式子集的构造

对于极小不可满足公式和它的子类的研究是近年来兴起的一个热门方向.极小不可满足公式通过分裂得到的公式保持了极小不可满足性,它的子类的某些性质对于建立在分裂上的归纳证明是很有用的.找到了一个能递归构造的极小不可满足公式的子类M4X+,并证明这种递归构造方法具有可靠性和完备性,最后给出了一个构造实例.     

集合的某些子类间的包含关系

通过具体公式在增加或删去某些文字或子句后生成的新公式的可满足性来研究极小不可满足公式类的常见子类Dis-MU,HIT-MU,Unique-MU,MARG-MU,MAX-MU和之间的包含关系.     

一个极小不可满足公式子类改名的复杂性研究

改名规则在创建有效的满足性算法和简化某些消解难例的证明中起到了重要作用,对于一些具有对称结构的难例公式,可以通过改名来降低其证明的复杂性.研究了一个极小不可满足公式子类,给出了该子类的改名算法,并证明了对该子类中改名问题可以在多项式时间内判定.     

集合MU的某些子类间的包含关系

通过具体公式在增加或删去某些文字或子句后生成的新公式的可满足性来研究极小不可满足公式类的常见子类Dis-MU,HIT-MU,Unique-MU,MARG-MU,MAX-MU和SYM-MU之间的包含关系.     

MAX—MU（2）的结构和复杂度

SAT问题(可满足性问题)是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年的一个热点研究方向.文章主要利用(1,*)-消解和分裂方法研究了差为2的极大极小不可满足公式集(MAX-MU(2))的结构和复杂度.     

HIT—MU（2）的结构和复杂度

SAT问题(可满足性问题)是计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向. 本文主要利用1(,)*-消解和分裂方法研究了差为2的碰撞极小不可满足公式集()2(MUHIT-)的结构和复杂度.此前,只有G.Davydov, I.Davydova 和H.Kleine Büning对)1(MU和)2(MU的结构和复杂度得出了较好的结果.     

Unique-MU(2)和SYM-MU(2)的结构和复杂度

SAT问题(可满足性问题)是计算机科学的核心问题,研究问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向. 文章主要利用,(1,*)-消解和分裂方法研究了差为2的唯一极小不可满足公式集(Unique-MU(2))和差为2的对称极小不可满足公式集(SYM-MU(2))的结构和复杂度.     

Unique-MU（2）和ISYM-MU（2）的结构和复杂度

SAT问题（可满足性问题）是计算机科学的核心问题，研究SAT问题的方法很多，利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向．文章主要利用（1，＊）-消解和分裂方法研究了差为2的唯一极小不可满足公式集（Unique-MU（2））和差为2的对称极小不可满足公式集（SYM-MU（2））的结构和复杂度．     

LINGO在形式逻辑中的应用

LINGO是一套专门用于求解最优化问题的软件,利用该软件可以给出求合式公式的真值和判定合式公式可以满足的方法.     

辅助变元之于命题与量化布尔公式的作用

使用辅助变元来引入定义,在知识表达中是一个流行和有力的技巧,能够得到更短、更自然的编码而无需冗长的重复.这篇论文中,我们形式地定义了辅助变元的概念,检验了其表达力并讨论了有趣的相关应用.我们把以下两者联系起来:一是,反复使用中间结果而不通过定义重复;二是,布尔函数其他表达中的相似概念.特别的,我们表明带定义的命题逻辑与具有任意输出端的布尔线路以及约束变元满足Horn性质的存在量化布尔公式(记作(E)HORNb)具有相同的表达力.本文还考虑了定义结构的限制,以及命题定义的扩充.特别的,我们检验了正命题定义与带存在量化的正定义之间的关系(或等价地,检验了(E)HORNb公式和约束变元未被Horn限定的存在量化的CNF公式(记作(E)CNF*)之间的关系).对命题定义的进一步扩充,是允许在定义中使用任意的量词,或等价地,允许布尔公式的嵌入.我们还证明了,量化CNF公式中的约束变元的表达力,是由子句中被约束部分的极小不可满足子公式或极小假子公式的结构所决定的.     

基于判别规则的最小不一致知识子集识别

为解释本体中概念不满足的原因,利用2个对等转换（即公理细化和本体约减）与3个判别规则识别不满足概念C的最小不一致知识子集（MUPS）.其中,判别规则基于不满足概念的传递性,将MUPS分为3类：完全依赖于C（MUPSf）、传递依赖于C（MUPSt）和不确定依赖于C（MUPSu）.实验结果表明：在本体不满足概念的MUPS中,MUPSt往往占大多数,但只有MUPSf可以明确指出概念不满足的根本原因.本体建模人员和领域专家可以采用迭代修复方式,每一次修复只考虑MUPSf,以提高修复效率.所得分类结果对于从修复角度评价本体质量以及指导修复工作都具有重要意义.     

局部对称黎曼流形的极小子流形

本文将邱成桐的关于常曲率空间紧致极小子流形的一个Simons型公式推广到局部对称紧致黎曼流形的紧致极小流形中去     

物流设备更新改造决策方法的改进

物流设备（施）的更新改造决策是物流管理会计中的重要内容，因此，如何从经济角度对物流设备（施）进行适时更新显得尤为重要。本文较为深入地探讨了物流管理会计中物流设备（施）更新改造的基本公式，对原有的年均成本计算公式进行了变形，以便从经济含义角度更好地理解掌握；构建了企业考虑所得税时物流设备（施）更新改造的计算公式，并进行了验证。     

公交线路选择系统与算法

研究了公交线路自主查询系统的核心即线路选择的模型与算法问题．考虑到查询者的不同需求,文中针对系统设计中转乘次数、线路时间、线路费用等三个因素,建立了实现转乘次数最小、路线时间最小、线路费用最少的多目标最优化模型．     

核心素养引领下的"等比数列"教学设计

核心素养引领课堂教学最基本的路径就是以核心素养为导向进行教学设计,基于数学核心素养的教学设计有助于数学课堂教学在教学理念、教学模式等方面发生转变.以人教A版必修五第二章第四节"等比数列"的教学设计为例,从教学目标、教学流程、教学检测三方面呈现等比数列通项公式等相关知识内化为学生数学核心素养的过程与方法.     

Statistics using just one formula

This article advocates that introductory statistics be taught by basing all calculations on a single simple margin‐of‐error formula and deriving all of the standard introductory statistical concepts (confidence intervals, significance tests, comparisons of means and proportions, etc) from that one formula. It is argued that this approach will better emphasize the core concepts and commonality of statistics and range of statistical applications, without forcing the students to memorize lots of different equations.