自动定理证明中含有等词的Horn集上的输入半锁反驳

本文的主要结果是文献[1]的推广。 众所周知,等词(equality)由于它的自反性、对称性、可传性以及替换性,它在谓词演算中有着特殊的地位。这样的特殊性也反映在自动定理证明中,一个含有等词的E不可满足子句集,在各种反驳策略中,除了使用归结原理(resolution)以外,还必须使用调解(paramodulation)这一推理规则。尽管如此,我们仍然可以把不含等词的不可满足子句集上的许多性质和证明技术,推广到含有等词的不可满足子句集上去。例如在文献[2]的第八章中,就有相应的输入调解、单位调解和线性调解等等。     

关于拓扑熵的一点注记

Adler,Konheim和McAndrew于1965年在文献[1]中首次引进了拓扑熵的概念。稍后Bowen在文献[2]中证明了一个相当重要的结果,他指出,紧致度量空间自映射的拓扑熵等于这一映射在它的非游荡集上的限制映射的拓扑熵。在文献[3]中也可找到另一个证明。关于这一结果的所有已知的证明均强烈地依赖于所考虑的映射的定义域的可度量性。本文推广Bowen的上述结果,证明了下述定理。     

Horn集上的输入半锁归结原理

归结原理是1965年由Robinson提出的一种重要的定理机器证明方法。1970年,Loveland和Luckham提出了线性归结,这是对归结原理的重要改进。一种特殊的线性归结——输入归结在计算机上极易实现。可惜,输入归结是不完备的。1974年Henschen和Wos研究了一种特殊子句集,即所谓Horn子句集。输入归结对于Horn集是完备的。1981年,陆汝铃对Horn集上的正单项有序归结和有序输入归结进行了研究,并得到很好的结果。     

逆极限与σ-积的Lindelf度

1 重要结果本文的主要结果是下面三个定理。定理1与文献[1]的结果相关,定理2与3分别推广了文献[2]和作者的一些结果。下面Hausdorff拓扑空间简称空间,映射是连续的。给定集A,以|A|表A的基数。     

三维FDS非线性波动方程初值问题的整体解

一 在文献[1]中提出了一类由数量场形成的三维孤立于问题,指出了这类非拓扑性孤立子解存在的必要条件,建立了依量子力学稳定性的一般定理,并对特殊问题给出了数值结果。在文献[2]中将此问题推广到具有非Abel内部对称性的情况。正如在文献[3]中指出,文献[1]中研究的方程组为     

L~*中的典型赋值中介与公理系统的简化

出于为模糊推理奠定逻辑基础之需要,文献[1]提出了形式系统Ｌ.基于此文献[2～4]从语义的角度为ＦＭＰ及ＦＭＴ建立了严格的逻辑依据.为从语构的角度开展进一步的工作,本文首先证明了Ｌ中Ｆ(Ｓ)的典型赋值中介[Ｆ]的结构定理,然后将Ｌ中的14条公理作了简化,得出了仅含9条公理的等价系统Ｌ°.设Ｓ是无限集,是一元运算,∨与→是二元运算,以Ｆ(Ｓ)记由Ｓ生成的(,∨,→)型自由代数.称由Ｆ(Ｓ)、文献[1]中的14条公理(Ｌ1),(Ｌ3)—(Ｌ6),(Ｍ1)—(Ｍ9)以及ＭＰ规则与交推理规则组成的系统为Ｌ.设Ａ,Ｂ∈Ｆ(Ｓ),定义Ａ～Ｂ　　当且仅当├(Ａ→Ｂ)且├…     

格值模型论的Morley定理

本文在文献[1—5]的基础上引进了格值模型论的Skolem函数、不可辨元集、饱和模型、原子模型和α-稳定理论等概念,证明了在值格有限时的格值模型论的Morley定理。 本文所用符号取自文献[1—5]。要求值格适合(F_1)、(F_2)和强特征式及紧致性定理。     

关于两参数Markov过程的强芽Markov性

本文把文献[1]所定义的关于单参数Markov过程强芽Markov性的概念移植到两参数Markov过程(即文献[2]中的~*-Markov过程)中,并得到了~*-Markov过程关于停线的两种强芽Markov性.同时,也证明了~*-Markov过程具有文献[3]意义下的强Markov性,且更具普遍性。此外,在文献[4]的基础上,证明了两参数Markov过程关于平面上任何开集具有芽Markov性,从而得到了文献[2]所希望的结果。     

Banach压缩映象原理与空间的完备性表征

著名的Ekeland变分原理与Caristi不动点定理与空间的完备性是等价的,其直接证明见文献[1]和[2]间接证明见文献[3]。1983年Borwein指出:在赋范空间中Banach压缩映象原理与空间的完备性是等     

Fuzzy凸集的分离定理

文献[1]中Zadeh引进了两个Fuzzy集关于普通超平面的分离度的概念,在此基础上给出了R~n中Fuzzy凸集的分离定理。Weiss在文献[2]中通过一个反例,指出了Zadeh的分离定理有漏洞,并作了修正。他利用所引进的诱导Fuzzy拓扑概念,给出了普通拓扑线性空间中Fuzzy凸集的分离定理。     

模态模型论中Bowen若干定理的反例和内插定理的失败

Kit Fine在文献[1]中证明了对于包含S_5的一些模态谓词演算而言,内插定理不成立,这与Bowen的结论相矛盾,并说,由于文献[2]“关于Robinson的联合无矛盾性定理(此定理为内插定理的主要依据——作者按)未给出详细证明,我们难于了解其错误所在。”事实上,Bowen的错误不在于其联合无矛盾性定理(文献[3]定理11.1,文献[2]定理10.1)、内插定理     

不分明拓扑空间中的紧性

紧性是拓扑学中最重要的概念之一,如何把它推广到不分明拓扑空间,国内外已有不少研究。但是,到目前为止所引入的各种紧性都或多或少地有这样或那样一些缺点,不能令人十分满意,评论见文献[1—3]。文献[2]提出的良紧性比较理想,但它缺乏覆盖或重盖这一类的几何刻划,而且定义中涉及到赋值集[0,1]的拓扑结构,给推广到一般的L不分明拓扑空间带来     

良紧集的层次结构与不分明Wallace定理

文献[1]与[2]关于良紧性的工作无疑是L-不分明拓扑学中重要而漂亮的成果。对于良紧性,有一个自然而有趣的问题:良紧性的层次结构问题。我们证明了:对弱诱导的Hausdorff空间,上层空间中的不分明集A的良紧性等价于对每一并既约元α,A的α-水平截集在底空间中的紧性;满层的弱Hausdorff空间中的良紧集为闭集。另外在本文中,对良紧性我们证明了不分明Wallace定理,这一定理的一个特殊情形(n=2)在文献[1]中曾得到。     

关于判定问题的两个注记

1.在文献中Castaneda对Lewis模态命题演算S5证明了一条定理。此定理表明演算S5具有有穷模型性质,从而由之可推出S5的可判定性。略早于文献[1]时,著者在文献[2]中对于演算(?)_ε得到一条类似的定理,即文献[2]中的定理6。这里应指出,Castaneda在文献[1]中的定理和文献[2]中的定理6实质上是等价的。这里先对文献[2]中有关部分作一些修正。文献[2]的定理6陈述中的“B_0~()”应改为“B_0~(<2n>)”;相应地,该定理证明中     

格值模型论中常量构作法的两个应用

本文是文献[1]中开始的把2值模型论各主要结果向多值模型论推广工作的继续。有些基本概念及记号用法可参看该文。但所讨论的内容与文献[1]是各自独立的。本文主要是用常量构作模型的方法的两个应用。其一是用于证明某些有限值格时的紧致性定理(文献[1]中已用超积方法证明了有限值格时的紧致性定理),其二是用于证明某些值格时的省略型定理。     

可化为一个“积分小”系数的二阶泛函微分方程解的振动性质

文献[1,2]讨论具有一个“积分小”系数的二阶微分方程解的振动性质。文献[3]的结果包括和改进了文献[1,2]的相应结果。但文献[1-3]所讨论的方程都是二阶常微分方程。至于“积分小”系数的二阶泛函微分方程解的振动性结果,目前尚未见报道。本文为此建立了若干振动性定理。 考虑二阶泛函微分方程     

点到集映象族算法的弱收敛性

本文给出了点到集映象族算法具有弱收敛性的条件,这些条件仅与空间的拓扑性质有关,是文献[1—4]中相应结果的改进与推广。特别对于Zangwill的算法(一种闭点到集映象算法),它具备弱收敛性的充要条件。此外,我们还对文献[6]中提出的算法建立了相应的弱收敛性定理。     

一阶格值逻辑系统FM的语法问题

文献[1～3]建立了以丰富剩余格为真值域的命题逻辑系统,得到了一些结果.为研究更一般的格值逻辑系统,文献[4]提出了格蕴涵代数的概念,文献[5]讨论了以格蕴涵代数为真值域的命题逻辑,文献[6」建立了以格蕴涵代数为真值域的—阶逻辑系统FM,本文讨论FM的语法问题,得到了FM的可靠性定理、演绎定理及协调性定理.设L是一格蕴涵代数,F是系统FM的公式集合.定理1~[6]对于任意公式p,q,r及正整数m,n,下列公式都是有效公式:     

一类半p-交换p-群

我们在文献[1]中定义了半p-交换p-群,并且研究了半p-交换性和正则性的关系。在文献[2]中又引进了半p~s-交换p-群和强半p-交换p-群的概念,研究了它们的幂结构。本文将证明p-群是强半p-交换的一个充分条件(定理1),并应用这个定理推广Laffey的某些新近的结果,还将给出Feit,Thompson和Alperin等人关于p-群的几个著名定理的新证明。     

关于两参数马氏过程的一个反例

一、引言和定义 本文以一个简单的例子否定了文献[1]的定理1和命题3(c)(ii)等结论,证明了宽过去马氏性与*-马氏性是不同的,从而澄清了一些误解。 沿用文献[2]的记号。设为取值于可测空间(E,)的两参数(两指标)过程。将X延拓到平面R_2上,对z∈R~2\R_+~2,令x_z=c(常值)。设z=(s,t)∈R~2,