子句集的神经网络归结

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

一种算子命题逻辑系统及其T-不变量推理算法

定义一种只带原子命题以及命题算子的算子命题逻辑,讨论了该逻辑的λ-归结的相容性、完备性及其若干逻辑性质。为了实现算子命题逻辑的归结推理,给出了算子命题逻辑的Petri网模型:Horn型,进一步讨论了推理算法:T-不变量算法,得到了算法的完备性定理。     

一种算子模糊逻辑系统及其Petri网推理算法

定义一种只带模糊文字以及模糊算子的模糊逻辑，讨论了该逻辑的λ-归结的相容性、完备性及其若干逻辑性质。为了实现算子模糊逻辑的归结推理，给出了算子模糊逻辑的Petri网模型：Horn型，进一步讨论了推理算法：T-不变量算法，得到了算法的完备性定理，最后用实例进行了验证。     

LP(X)中MP归结推理

首先讨论格值命题逻辑系统LP(X)中子句的规则型范式以及极简规则型子句集的形式,然后定义MP归结式以及(A,α)-归结演绎、α-逻辑推理以及α-不可满足,讨论了它们的一系列逻辑性质,最后证明了MP归结推理的可靠性以及弱完备性.     

格值命题逻辑系统中基于滤子的MP归结演绎

给出了格值命题逻辑系统中子句的极简规则型范式,定义了MP归结.结合格蕴涵代数中滤子的性质,对格值命题逻辑系统中基于滤予的MP归结演绎及其语义与语法性质进行了研究,证明了归结演绎的可靠性与完备性定理.为进一步研究格值逻辑的自动归结推理奠定了理论基础.     

格值命题逻辑LP(X)中不可分极简式的性质

基于格值命题逻辑LP(X)的α-归结原理及α-归结自动推理方法，能够较好地刻画具有可比较性和不可比较性的不确定性信息。LP(X)中的不可分极简式是一个非常重要的概念，本文对蕴涵运算个数小于3的不可分极简式的性质和判定方法进行了讨论，得到了一些重要结论。     

格值命题逻辑系统L_(2n+1)P(X)中基于半正则广义文字的自动推理算法

在格值命题逻辑系统L2n+1P(X)上,提出了半正则的正广义文字和半正则的负广义文字的概念,进一步给出了半正则广义子句和半正则广义子句集的定义,详细地讨论了L2n+1P(X)上以中界元M为归结水平的半正则广义文字之间的M-归结性,最后,给出了L2n+1P(X)上基于半正则广义文字的归结水平为M的归结自动推理算法,并验证了其可靠性和完备性.     

一类单极等熵流体动力学半导体模型的松弛极限

对一类有短的动量松弛时间的多维等熵流体动力学半导体模型的极限问题进行了讨论．首先构造非线性问题的有初始层的近似解,进而,在归结问题的解存在且有合适的正则性的假设下,证明了原非线性问题的局部古典解的存在性,并且证明了这个解在归结问题解的存在时间区间内收敛到形式近似解．     

一类单极等熵流体动力学半导体模型的松弛极限

对一类有短的动量松弛时间的多维等熵流体动力学半导体模型的极限问题进行了讨论.首先构造非线性问题的有初始层的近似解,进而,在归结问题的解存在且有合适的正则性的假设下,证明了原非线性问题的局部古典解的存在性,并且证明了这个解在归结问题解的存在时间区间内收敛到形式近似解.     

基于矩阵方法的Myerson值的一种规范化

在合作对策中,将一个值规范化意味着让其满足有效性.Hamiache利用矩阵方法得到了带图结构效用可转移合作对策Myerson值的一种规范化.通过给出一种新的满足最小划分唯一性的集合簇,本文利用矩阵方法得到了Myerson值的另一种规范化.特殊地,当所考虑的图结构在各连通分支上的限制均为完全图时,文中给出了带联盟结构效用可转移合作对策AumannDrèze值的一种规范化.与其它Myerson值规范化的比较分析表明本文规范化与van den Brink等的等价.由此van den Brink等的规范化与Hamiache的规范化都可用矩阵方法来描述,而它们之间的区别则被归结于满足最小划分唯一性的集合簇之不同.     

Some generalizations of the criss-cross method for quadratic programming

Three generalizations of the criss-cross method for quadratic programming are presented here. Tucker’s, Cottle’s and Dantzig’s principal pivoting methods are specialized as diagonal and exchange pivots for the linear complementarity problem obtained from a convex quadratic program

A finite criss-cross method, based on least-index resolution, is constructed for solving the LCP. In proving finiteness, orthogonality properties of pivot tableaus and positive semidefiniteness of quadratic matrices are used

In the last section some special cases and two further variants of the quadratic criss-cross method are discussed. If the matrix of the LCP has full rank, then a surprisingly simple algorithm follows, which coincides with Murty’s ‘Bard type schema’ in the P matrix case     

SAT graph-based representation: A new perspective

In this paper a new graph based representation of Boolean formulas in conjunctive normal form (CNF) is proposed. It extends the well-known graph representation of binary CNF formulas (2-SAT) to the general case. Every clause is represented as a set of (conditional) implications and encoded with different edges labeled with a set of literals, called context. This representation admits many interesting features. For example, a path from the node labeled with a literal ¬x to the node labeled with a literal x gives us an original way to compute the condition under which the literal x is implied. Using this representation, we show that classical resolution can be reformulated as a transitive closure on the generated graph. Interestingly enough, using the SAT graph-based representation three original applications are then derived. The first one deals with the 2-SAT strong backdoor set computation problem, whereas in the second one the underlying representation is used to derive hard SAT instances with respect to the state-of-the-art satisfiability solvers. Finally, a new preprocessing technique of CNF formulas which extends the well-known hyper-resolution rule is proposed. Experimental results show interesting improvements on many classes of SAT instances taken from the last SAT competitions.     

Semidefinite resolution and exactness of semidefinite relaxations for satisfiability

This paper explores new connections between the satisfiability problem and semidefinite programming. We show how the process of resolution in satisfiability is equivalent to a linear transformation between the feasible sets of the relevant semidefinite programming problems. We call this transformation semidefinite programming resolution, and we demonstrate the potential of this novel concept by using it to obtain a direct proof of the exactness of the semidefinite formulation of satisfiability without applying Lasserre’s general theory for semidefinite relaxations of 0/1 problems. In particular, our proof explicitly shows how the exactness of the semidefinite formulation for any satisfiability formula can be interpreted as the implicit application of a finite sequence of resolution steps to verify whether the empty clause can be derived from the given formula.     

Desingularization of quasi-excellent schemes in characteristic zero

Grothendieck proved in EGA IV that if any integral scheme of finite type over a locally noetherian scheme X admits a desingularization, then X is quasi-excellent, and conjectured that the converse is probably true. We prove this conjecture for noetherian schemes of characteristic zero. Namely, starting with the resolution of singularities for algebraic varieties of characteristic zero, we prove the resolution of singularities for noetherian quasi-excellent Q-schemes.     

Resolution and the integrality of satisfiability problems

A satisfiability problem can be regarded as a nondisjoint union of set covering problems. We show that if the resolution method of theorem proving is applied to the satisfiability problem, its constraint set defines an integral polytope if and only if the constraint sets of the set covering problems do. In this sense, resolution reduces the integrality question for the satisfiability problem to that for the set covering problem. Partially supported by ONR grant N00014-92-J-1028 and AFOSR grant 91-0287.     

Resolutions of Some Gorenstein Algebras with Nonunimodal Hilbert Functions

Given a compressed Artin level algebra A which satisfies certain properties, it is possible to use this algebra to construct a Gorenstein Artin algebra with a nonunimodal Hilbert function. We show how to construct a minimal free resolution for these algebras, using the minimal free resolution of A.     

An elementary coordinate-dependent local resolution of singularities and applications

An elementary classical analysis resolution of singularities method is developed, extensively using explicit coordinate systems. The algorithm is designed to be applicable to subjects such as oscillatory integrals and critical integrability exponents. As one might expect, the trade-off for such an elementary method is a weaker theorem than Hironaka's work [H. Hironaka, Resolution of singularities of an algebraic variety over a field of characteristic zero I, Ann. of Math. (2) 79 (1964) 109-203; H. Hironaka, Resolution of singularities of an algebraic variety over a field of characteristic zero II, Ann. of Math. (2) 79 (1964) 205-326] or its subsequent simplications and extensions such as [E. Bierstone, P. Milman, Canonical desingularization in characteristic zero by blowing up the maximum strata of a local invariant, Invent. Math. 128 (2) (1997) 207-302; S. Encinas, O. Villamayor, Good points and constructive resolution of singularities, Acta Math. 181 (1) (1998) 109-158; J. Kollar, Resolution of singularities—Seattle lectures, preprint; A.N. Varchenko, Newton polyhedra and estimates of oscillatory integrals, Funct. Anal. Appl. 18 (3) (1976) 175-196]. Nonetheless the methods of this paper can be used to prove a variety of theorems of interest in analysis. As illustration, two consequences are given. First and most notably, a general theorem regarding the existence of critical integrability exponents are established. Secondly, a quick proof of a well-known inequality of Lojasiewicz [S. Lojasiewicz, Ensembles semi-analytiques, Inst. Hautes Études Sci., Bures-sur-Yvette, 1964] is given. The arguments here are substantially different from the general algorithms such as [H. Hironaka, Resolution of singularities of an algebraic variety over a field of characteristic zero I, Ann. of Math. (2) 79 (1964) 109-203; H. Hironaka, Resolution of singularities of an algebraic variety over a field of characteristic zero II, Ann. of Math. (2) 79 (1964) 205-326], or the elementary arguments of [E. Bierstone, P. Milman, Semianalytic and subanalytic sets, Inst. Hautes Études Sci. Publ. Math. 67 (1988) 5-42] and [H. Sussman, Real analytic desingularization and subanalytic sets: an elementary approach, Trans. Amer. Math. Soc. 317 (2) (1990) 417-461]. The methods here have as antecedents the earlier work of the author [M. Greenblatt, A direct resolution of singularities for functions of two variables with applications to analysis, J. Anal. Math. 92 (2004) 233-257], Phong and Stein [D.H. Phong, E.M. Stein, The Newton polyhedron and oscillatory integral operators, Acta Math. 179 (1997) 107-152], and Varchenko [A.N. Varchenko, Newton polyhedra and estimates of oscillatory integrals, Funct. Anal. Appl. 18 (3) (1976) 175-196].