The polynomial bounds of proof complexity in Frege systems

The concept of a determinative set of variables for a propositional formula was introduced by one of the authors, which made it possible to distinguish the set of hard-determinable formulas. The proof complexity of a formula of this sort has exponential lower bounds in some proof systems of classical propositional calculus (cut-free sequent system, resolution system, analytic tableaux, cutting planes, and bounded Frege systems). In this paper we prove that the property of hard-determinability is insufficient for obtaining a superpolynomial lower bound of proof lines (sizes) in Frege systems: an example of a sequence of hard-determinable formulas is given whose proof complexities are polynomially bounded in every Frege system.     

Does truth-table of linear norm reduce the one-query tautologies to a random oracle?

In our former works, for a given concept of reduction, we study the following hypothesis: “For a random oracle A, with probability one, the degree of the one-query tautologies with respect to A is strictly higher than the degree of A.” In our former works (Suzuki in Kobe J. Math. 15, 91–102, 1998; in Inf. Comput. 176, 66–87, 2002; in Arch. Math. Logic 44, 751–762), the following three results are shown: The hypothesis for p-T (polynomial-time Turing) reduction is equivalent to the assertion that the probabilistic complexity class R is not equal to NP; The hypothesis for p-tt (polynomial-time truth-table) reduction implies that P is not NP; The hypothesis holds for each of the following: disjunctive reduction, conjunctive reduction, and p-btt (polynomial-time bounded-truth-table) reduction. In this paper, we show the following three results: (1) Let c be a positive real number. We consider a concept of truth-table reduction whose norm is at most c times size of input, where for a relativized propositional formula F, the size of F denotes the total number of occurrences of propositional variables, constants and propositional connectives. Then, our main result is that the hypothesis holds for such tt-reduction, provided that c is small enough. How small c can we take so that the above holds? It depends on our syntactic convention on one-query tautologies. In our setting, the statement holds for all c < 1. (2) The hypothesis holds for monotone truth-table reduction (also called positive reduction). (3) Dowd (in Inf. Comput. 96, 65–76, 1992) shows a polynomial upper bound for the minimum sizes of forcing conditions associated with a random oracle. We apply the above result (1), and get a linear lower bound for the sizes.     

Resolution over linear equations modulo two

We consider an extension of the resolution proof system that operates with disjunctions of linear equalities over ${\mathbb{F}}_2$; we denote this system by Res(⊕). It is well known that tree-like resolution is equivalent in behavior to DPLL algorithms for the Boolean satisfiability problem. Every DPLL algorithm splits the input problem into two by assigning two possible values to a variable; then it simplifies the two resulting formulas and makes two recursive calls. Tree-like Res(⊕)-proofs correspond to an extension of the DPLL paradigm, in which we can split by an arbitrary linear combination of variables modulo two. These algorithms quickly solve formulas that explicitly encode linear systems modulo two which were used for proving exponential lower bounds for conventional DPLL algorithms.We prove exponential lower bounds on the size of tree-like Res(⊕)-proofs. We also show that resolution and tree-like Res(⊕) do not simulate each other.We prove a space vs size tradeoff for Res(⊕)-proofs. We prove that Res(⊕) is implicationally complete and also that Res(⊕) is polynomially equivalent to its semantic version.We consider the proof system $\text{Res}(\oplus ;⩽k)$ that is a restricted version of Res(⊕) operating with disjunctions of linear equalities such that at most k equalities depend on more than one variable. We simulate $\text{Res}(\oplus ;⩽k)$ in the OBDD-based proof system with blowup $2^k$ and in Polynomial Calculus Resolution with blowup $2^{nH(2k/n)}poly(n)$, where n is the number of variables and $H(p)$ is the binary entropy; the latter result implies exponential lower bounds on the size of $\text{Res}(\oplus ;⩽\delta n)$-proofs for some constant $\delta >0$. Raz and Tzameret introduced the system R(lin) which operates with disjunctions of linear equalities with integer coefficients. We show that Res(⊕) can be p-simulated in R(lin).     

单调线性互补问题的Mehrotra型预估-校正算法的迭代复杂性

Mehrotra型预估-校正算法是很多内点算法软件包的算法基础,但它的多项式迭代复杂性直到2007年才被Salahi等人证明.通过选择一个固定的预估步长及与Salahi文中不同的校正方向,本文把Salahi等人的算法拓展到单调线性互补问题,使得新算法的迭代复杂性为O(n log((x0)T s0/ε)),同时,初步的数值实验证明了新算法是有效的.     

The proof theoretic strength of the Steinitz exchange theorem

We show that the logical theory QLA proves the Cayley-Hamilton theorem from the Steinitz exchange theorem together with a strengthening of the linear independence principle. Since QLA is a fairly weak theory (in the sense that its quantifier-free fragment, LA, translates into tautologies with TC⁰-Frege proofs—when restricted to the field Q of the rationals), it follows that the proof complexity of matrix algebra can be distilled to the Steinitz exchange theorem.     

Constructive Proofs of the Brouwer Type Coincidence Theorems

In 1 966,Schirmer[1 ] proved the following interesting Brouwer type coincidencetheorem for the n dimensional closed unit disc Dn.　 Theorem1　 Suppose that the continuous mapping f:Dn→ Dn maps the boundary Sn- 1essentially onto itself.Then for any continuous mapping g:Dn→Dn,the equationf(x) =g(x)has a solution in Dn.　 This result is closely related to Brouwer' s celebrated fixed point theorem. Someimportant generalizations and applications of it can be found in [2— 4 ] .　 In this not…     

Lagrange插值公式的几种构造性证明

利用中国剩余定理、行列式以及线性方程组理论给出了Lagrange插值公式的几种构造性证明,得到了Vandermonde矩阵的逆矩阵的一种算法.     

单调算子的值域和在混合边值问题中的应用

通过定义几种算子,对其性质加以研究,并利用了Reich的关于值域和的有关结果,研究了非线性椭圆型方程及非线性抛物型方程,推导出这两种方程的解的存在性条件,从而推广了Pascali的相关结果.     

Monotone method for singular BVP in the presence of upper and lower solutions

In this paper we examine existence of monotone approximations of solutions of singular boundary value problem -(p(x)y^′(x))^′=q(x)f(x,y,py^′) for 0<x?b and lim_x→0⁺p(x)y^′(x)=0,α₁y(b)+β₁p(b)y^′(b)=γ₁. Under quite general conditions on f(x,y,py^′) we show that solution of the singular two point boundary value problem is unique. Here is allowed to have integrable singularity at x=0 and we do not assume .     

Best Approximation from the Kuhn-Tucker Set of Composite Monotone Inclusions

Kuhn-Tucker points play a fundamental role in the analysis and the numerical solution of monotone inclusion problems, providing in particular both primal and dual solutions. We propose a class of strongly convergent algorithms for constructing the best approximation to a reference point from the set of Kuhn-Tucker points of a general Hilbertian composite monotone inclusion problem. Applications to systems of coupled monotone inclusions are presented. Our framework does not impose additional assumptions on the operators present in the formulation, and it does not require knowledge of the norm of the linear operators involved in the compositions or the inversion of linear operators.     

On the complexity of cutting-plane proofs using split cuts

We prove a monotone interpolation property for split cuts which, together with results from Pudlák (1997) [20], implies that cutting-plane proofs which use split cuts (or, equivalently, mixed-integer rounding cuts or Gomory mixed-integer cuts) have exponential length in the worst case.     

A new proof of the refined alternating sign matrix theorem

In the early 1980s, Mills, Robbins and Rumsey conjectured, and in 1996 Zeilberger proved a simple product formula for the number of n×n alternating sign matrices with a 1 at the top of the ith column. We give an alternative proof of this formula using our operator formula for the number of monotone triangles with prescribed bottom row. In addition, we provide the enumeration of certain 0-1-(−1) matrices generalizing alternating sign matrices.     

Sufficient conditions for the existence of global solutions of delayed differential equations

The purpose of this contribution is to give sufficient conditions for the existence of global solutions or left semi-global solutions for some classes of delayed functional differential equations. The principle of monotone sequences is used as a main tool of investigation. Inequalities for coordinates of global solutions are derived as a consequence of used method. Examples illustrate the results.     

On the complexity of monotone dualization and generating minimal hypergraph transversals

In 1994 Fredman and Khachiyan established the remarkable result that the duality of a pair of monotone Boolean functions, in disjunctive normal forms, can be tested in quasi-polynomial time, thus putting the problem, most likely, somewhere between polynomiality and coNP-completeness. We strengthen this result by showing that the duality testing problem can in fact be solved in polylogarithmic time using a quasi-polynomial number of processors (in the PRAM model). While our decomposition technique can be thought of as a generalization of that of Fredman and Khachiyan, it yields stronger bounds on the sequential complexity of the problem in the case when the sizes of f and g are significantly different, and also allows for generating all minimal transversals of a given hypergraph using only polynomial space.     

RMI原则在GA中的应用

把关系结构P映射为关系结构GA,经过GA过程确定目标映像,最后通过求反演求目标原像.