MU(1)内公式改名的多项式可判定性

研究判定合取范式公式F和H之间是否存在一个改名φ使得φ(F)＝H的计算复杂性。公式的改名是将命题变元映到变元本身或变无的否定的一个映射，对于极小不可满足公式的子类射MU／(1)中的公式，我们证明了其改名判定问题在多项式时间内是可判定的。     

可满足公式到极小不可满足公式MU(1)的扩张复杂性

可满足合取范式（CNF）公式F到极小不可满足公式MU（1）的扩张是,对给定的CNF公式F,是否存在一个公式G满足条件var（G）包含var（F）并使得F＋G∈MU（1）。Horn公式到MU（1）公式的扩张问题可在多项式时间内解决,但对一般CNF公式F的扩张问题,至今尚未解决。这里我们将给出一个多项式时间的算法解决这一问题。     

NT-HIT(k)公式的存在性

一个合取范式(CNF)公式F是NT-HIT公式,如果F中的任意两个不同的子句中恰有一对互补文字。NT-HIT(k)是公式的子句数与变元数之差为k的NT-HIT公式类。通过构造一个命题公式Hn,m,我们证明了：(1)Hn,m可满足当且仅当存在一个含有n个变元和m个子句的NT-HIT公式。(2)对于NT-HIT(1)中的任意一个公式F,存在一个文字L,L在F中仅出现一次。进一步,我们证明了：对于k≥2,公式Hn,n k是一个不可满足公式。于是,对于k≥2,NT-HIT(k)是一个空集。从而就解决了[1]中的两个公开的问题。     

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

SAT问题(可满足性问题)是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向.本文主要利用(1,*)-消解方法研究了差为2的边缘极小不可满足公式集(MARG-MU(2))的结构和复杂度:在结构方面,MARG-MU(2)中的公式要么是F22,要么是某一文字在其中仅出现一次的公式;在复杂度方面,如果MARG-MU(2)对(1,*)-消解封闭,则某个含有n个变元和n+2个子句的公式是否为MARG-MU(2)中的公式的问题可以在时间0(n3)内被判定.     

MXX和MARG中公式改名的复杂性

研究了判定问题“对于命题CNF公式F和H,是否存在一个变元(或文字)改名(?),使得(?)(F)=H?”的复杂性．对于极小不可满足公式的子类MAX和MARG,我们证明了:其变元改名和文字改名的复杂性等价于图同构问题GI．     

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

SAT问题（可满足性问题）是理论计算机科学的核心问题,研究SAT问题的方法很多,利用极小不可满足公式的性质来研究SAT问题是近几年兴起的一个热点研究方向。本文主要利用（1,＊）-消解方法研究了差为2的边缘极小不可满足公式集（MARG-MU（（2））的结构和复杂度：在结构方面,胁MARG—MU（2）中的公式要么是F2^2,要么是某一文字在其中仅出现一次的公式;在复杂度方面,如果MARG-MU（2）对（1,＊）-消解封闭,则某个含有,1个变元和n＋2个子旬的公式是否为MARG-MU（2）中的公式的问题可以在时间O（n^3）内被判定。     

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

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

AFS结构上矩阵的幂等指数估计

在应用AFS结构(M，τ，x)研究故障诊断问题中，需要寻找正整数，使其满足Mτ^2r=Mτ^r，由于复杂系统对应的AFS结构上矩阵Mτ的阶数较大，为了减少计算量，需要估计出最小的r，就此问题，给出了基于集合M上的布尔矩阵的概念并得出其传递闭包的相关性质，进而在集合M上的布尔矩阵与(0，1)布尔矩阵之间建立一种同态映射并给出其证明，最后应用该映射对r的范围进行了估计。     

关于单元证明的几个结果

本文讨论了基本子句集合有单元(线性-单元、输入-单元、输入-正的单元)反驳的条件,证明了子句的文字不超过两个的不可满足的Horn集有输入-单元反驳.     

对称矩阵空间上的保秩1导出映射

设F是任意域,fij(i,j∈[n])是从F到自身的映射,Sn(F)是F上n阶对称矩阵全体所成集合,f是Sn(F)上由[fij]n诱导出的映射,本文研究Sn(F)上几种保秩1导出映射的形式.     

受控Lorenz系统的一些结果及其应用

首先考虑受控的Lorenz系统，利用Jacobin矩阵和平衡点的定义，给出了系统的控制项；再利用广义Lyapunov函数簇。给出了此系统的全局吸引集和正向不变集估计的方法和结果，并分析了此系统的稳定性；利用此系统简化椭球公式的证明，从而讧明了Leonov公式，将估计式统一在一个公式之中，新公式还可以派生出一系列其他的估计式；然后，利用几何学的交集的思想，获得全局吸引集和正向不变集的更佳结果；最后，采用线性反馈的方法构造了一个同步系统，在Matlab上进行了数值仿真，给出了系统的同步误差图，结果表明此方法是可行有效的．     

MAX+(k)中公式改名的多项式时间可判定性

MAX^ (k)是极小不可满足公式的一个子类。作者引入了MAX^ (k)中公式的一种递归构造方法,基于分裂技术并通过证明MAX(1)中公式改名问题在多项式时间内可以判定。证明了MAX^ (k)中公式的改名问题在多项式时间内可以判定。     

一个极小不可满足公式子类的等价结构

研究一个极小不可满足公式子类（MAX（1）的等价结构,考虑了MAX（1）上的变元改名问题和文字改名问题。此两个问题均可在O（nlog2(n))时间内可解。     

Horn集上的语义正单元归结

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

确定原子体系精细波函数的群论方法

原子体系的精细波函数是群ＳＵ２在各种首权下的不可约表示基。群ＳＵ２的约化，虽有一套完整的处理方法，但计算十分繁杂，且比较抽象。本文通过分析群ＳＵ２与转换群Ｓｎ间的同态对应关系，由转换群Ｓｎ的不可约基，得到群ＳＵ２的不可约基。本文以四（价）电子原子体系为例进行讨论，分三部：一、实验事实和量子力学一般结论；二、Ｓ４的约化系数矩阵及其不可约表示基；三、ＳＵ２在首权ｓ＝２，１，０下的不可约表示基－－四（价     

基于BL系统的演绎系统集代数的剩余格属性

在命题逻辑系统BL中提出了演绎系统的概念, 并且给出了由F(S)的子集生成演绎系统的方法, 证明了命题逻辑系统BL中演绎系统和结论之集的同一性; 其次, 在命题逻辑系统BL中证明了在包含偏序关系下所有演绎系统构成的集族D(F )中上, 下确界的存在性; 最后, 在D(F )中定义了二元运算∧,∨,*,→, 证明了集代数(D(F ),∧,∨,*,→,0,1)是满足可除性的完备剩余格。     

二元域上线性半群到任意域上线性半群的同态

群同态是群论研究的主要问题,F2上的半群同态也一直是群论研究者关注的热点问题.为探讨二阶线性半群间的同态问题,本文在引进标准型、延断型、平凡型概念的基础上,通过矩阵计算与群的定义关系,描述了F2上的线性半群Mn(F2)到任意域K上的线性半群Mm(K)的同态形式(n≥m2).给出了nm,乘法半群同态(不必保幺元)为In,s,r或为φ1的延断(其中:若X为GL2(F2)的2阶元,φ1(X)=-1;若X=I2或X为3阶元,φ1(X)=1);当n=m时,乘法半群同态(不必保幺元)除In,s,r外,为标准型或为线性非平凡解同态的延断.这些结果结合文献中已有的关于一般线性群及二阶线性半群的结果,完全描述了二元域上的线性半群到任意域上的线性半群的同态的形式.