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.     

The split closure of a strictly convex body

The Chvátal-Gomory closure and the split closure of a rational polyhedron are rational polyhedra. It has been recently shown that the Chvátal-Gomory closure of a strictly convex body is also a rational polytope. In this note, we show that the split closure of a strictly convex body is defined by a finite number of split disjunctions, but is not necessarily polyhedral. We also give a closed form expression in the original variable space of a split cut for full-dimensional ellipsoids.     

On split common fixed point problems

Based on the convergence theorem recently proved by the second author, we modify the iterative scheme studied by Moudafi for quasi-nonexpansive operators to obtain strong convergence to a solution of the split common fixed point problem. It is noted that Moudafi's original scheme can conclude only weak convergence. As a consequence, we obtain strong convergence theorems for split variational inequality problems for Lipschitz continuous and monotone operators, split common null point problems for maximal monotone operators, and Moudafi's split feasibility problem.     

Glivenko sequent classes in the light of structural proof theory

In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened to height-preserving statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained.     

A constructive proof of the Cartan-Dieudonné-Scherk Theorem in the real or complex case

The Cartan-Dieudonné-Scherk Theorem states that for fields of characteristic other than 2, every orthogonality can be written as the product of a certain minimal number of reflections across hyperplanes. The earliest proofs are not constructive, and constructive proofs either do not achieve minimal results or have been restricted to special cases. This paper presents a constructive proof in the real or complex field of the decomposition of a generalized orthogonal matrix into the product of the minimal number of generalized Householder matrices.     

A construction of pseudo metacirculants

Metacirculants were introduced by Alspach and Parsons in 1982 and have been a rich source of various topics since then. It is known that every metacirculant is a split weak metacirculant (A graph is called (split) weak metacirculant if it has a vertex-transitive (split) metacyclic subgroup of automorphisms). We say that a split metacirculant is a pseudo metacirculant if it is not metacirculant. In this paper, an infinite family of pseudo metacirculants is constructed, and this provides a negative answer to Question A in Zhou and Zhou (2018).     

The Borsuk-Ulam-property, Tucker-property and constructive proofs in combinatorics

This article is concerned with a general scheme on how to obtain constructive proofs for combinatorial theorems that have topological proofs so far. To this end the combinatorial concept of Tucker-property of a finite group G is introduced and its relation to the topological Borsuk-Ulam-property is discussed. Applications of the Tucker-property in combinatorics are demonstrated.     

On the NP-hardness of deciding emptiness of the split closure of a rational polytope in the 0,1 hypercube

Split cuts are prominent general-purpose cutting planes in integer programming. The split closure of a rational polyhedron is what is obtained after intersecting the half-spaces defined by all the split cuts for the polyhedron. In this paper, we prove that deciding whether the split closure of a rational polytope is empty is NP-hard, even when the polytope is contained in the unit hypercube. As a direct corollary, we prove that optimization and separation over the split closure of a rational polytope in the unit hypercube are NP-hard, extending an earlier result of Caprara and Letchford.     

Meaning explanations at higher dimension

Martin-Löf’s intuitionistic type theory is a widely-used framework for constructive mathematics and computer programming. In its most popular form, type theory consists of a collection of inference rules inductively defining formal proofs. These rules are justified by Martin-Löf’s meaning explanations, which extend the Brouwer–Heyting–Kolmogorov interpretation of connectives to a rich collection of types, and therefore provide a constructive realizability interpretation of formal proofs.Around 2005, researchers noticed that the rules of type theory also admit homotopy-theoretic models, and subsequently extended type theory with constructs inspired by these models: higher inductive types and Voevodsky’s univalence axiom. Although the resulting homotopy type theory has proved useful for homotopy-theoretic reasoning, it lacks a constructive interpretation. In this overview, we discuss a cubical generalization of the meaning explanations of type theory that constitutes an inherently constructive account of higher-dimensional structure in types.     

A note on the MIR closure and basic relaxations of polyhedra

Anderson et al. (2005) [1] show that for a polyhedral mixed integer set defined by a constraint system Ax≥b, along with integrality restrictions on some of the variables, any split cut is in fact a split cut for a basic relaxation, i.e., one defined by a subset of linearly independent constraints. This result implies that any split cut can be obtained as an intersection cut. Equivalence between split cuts obtained from simple disjunctions of the form x_j≤0 or x_j≥1 and intersection cuts was shown earlier for 0/1-mixed integer sets by Balas and Perregaard (2002) [4]. We give a short proof of the result of Anderson, Cornuéjols and Li using the equivalence between mixed integer rounding (MIR) cuts and split cuts.     

A strong constructive version of engel's theorem

We examine two problems in the computational theory of Lie algebras. First, we prove a constructive version of Engel's theorem: if L is a finite-dimensional Lie algebra that is not nilpotent, we show how to construct an element x in L such that the linear transformation ad x is not nilpotent. No special assumptions about the underlying field are needed. Second, as an important application of the first result, we give an algorithm for the construction of a Cartan subalgebra of a finite-dimensional Lie algebra. This solves the problem of finding a totally constructive proof of the existence of a Cartan subalgebra, posed by Beck, Kolman, and Stewart in the paper "Computing the Structure of a Lie Algebra". Our proofs are ordinary mathematical proofs that do not employ the general law of excluded middle. The advantage of this approach to mathematics is that our proofs, which are not burdened or obscured by the details of a particular programming language, can nevertheless be routinely turned into computer programs     

On constructivity and the Rosser property: a closer look at some Gödelean proofs

The proofs of Kleene, Chaitin and Boolos for Gödel's First Incompleteness Theorem are studied from the perspectives of constructivity and the Rosser property. A proof of the incompleteness theorem has the Rosser property when the independence of the true but unprovable sentence can be shown by assuming only the (simple) consistency of the theory. It is known that Gödel's own proof for his incompleteness theorem does not have the Rosser property, and we show that neither do Kleene's or Boolos' proofs. However, we show that a variant of Chaitin's proof can have the Rosser property. The proofs of Gödel, Rosser and Kleene are constructive in the sense that they explicitly construct, by algorithmic ways, the independent sentence(s) from the theory. We show that the proofs of Chaitin and Boolos are not constructive, and they prove only the mere existence of the independent sentences.     

On the formal points of the formal topology of the binary tree

 Formal topology is today an established topic in the development of constructive mathematics and constructive proofs for many classical results of general topology have been obtained by using this approach. Here we analyze one of the main concepts in formal topology, namely, the notion of formal point. We will contrast two classically equivalent definitions of formal points and we will see that from a constructive point of view they are completely different. Indeed, according to the first definition the formal points of the formal topology of the real numbers can be indexed by a set whereas this is not possible according to the second one. Received: 23 May 2000 / Published online: 12 July 2002     

Prototype Proofs in Type Theory

The proofs of universally quantified statements, in mathematics, are given as “schemata” or as “prototypes” which may be applied to each specific instance of the quantified variable. Type Theory allows to turn into a rigorous notion this informal intuition described by many, including Herbrand. In this constructive approach where propositions are types, proofs are viewed as terms of λ‐calculus and act as “proof‐schemata”, as for universally quantified types. We examine here the critical case of Impredicative Type Theory, i. e. Girard's system F, where type‐quantification ranges over all types. Coherence and decidability properties are proved for prototype proofs in this impredicative context.     

On extreme points of bounded sets of generalized finite sequence spaces

The Linear Independence Extreme Point Theorem and Opposite Sign Theorem of semiinfinite programming provide algebraic characterizations of unbounded infinite dimensional convex polyhedral sets in terms of their extreme points. The Charnes, Kortanek, and Raike purification algorithm, which transforms any non-extreme point to an extreme point having objective function value at least as great, is based upon the constructive proofs of these two theorems. In this paper these extreme point characterizations are extended to additionally constrained, bounded convex polyhedral constraint sets of semi-infinite programming. It is shown that each of these bounded sets is spanned by a possibly infinite number of extreme points, and as before the proofs are constructive, thereby expanding the range of applicability of the purification algorithm to these cases.     

Effect of Modeling Uncertainty on Some Routing Problems

In this paper, we consider the routing problem described in Mohanty and Cassandras (Ref. 1). As in Ref. 1, we show that the optimal Bernoulli split to minimize mean time in the system is asymptotically independent of the variance of the service time. We give simple proofs of the results in that paper. We exploit the fact that the optimal split to minimize the mean queueing time is variance independent and the special structure of the Karush–Kuhn–Tucker optimality conditions to derive the optimal solution. Apart from being very straightforward, the proofs also give insight into the reason for the existence of the variance-independent asymptotically optimal routing policy.     

Specker sequences revisited

Specker sequences are constructive, increasing, bounded sequences of rationals that do not converge to any constructive real. A sequence is said to be a strong Specker sequence if it is Specker and eventually bounded away from every constructive real. Within Bishop's constructive mathematics we investigate non‐decreasing, bounded sequences of rationals that eventually avoid sets that are unions of (countable) sequences of intervals with rational endpoints. This yields surprisingly straightforward proofs of certain basic results fromconstructive mathematics. Within Russian constructivism, we show how to use this general method to generate Specker sequences. Furthermore, we show that any nonvoid subset of the constructive reals that has no isolated points contains a strictly increasing sequence that is eventually bounded away from every constructive real. If every neighborhood of every point in the subset contains a rational number different from that point, the subset contains a strong Specker sequence. (© 2005 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

A constructive proof of Ky Fan's generalization of Tucker's lemma

We present a proof of Ky Fan's combinatorial lemma on labellings of triangulated spheres that differs from earlier proofs in that it is constructive. We slightly generalize the hypotheses of Fan's lemma to allow for triangulations of Sⁿ that contain a flag of hemispheres. As a consequence, we can obtain a constructive proof of Tucker's lemma that holds for a more general class of triangulations than the usual version.     

Comparison of Picard groups in dimension 1

We compare two Picard groups in dimension 1. Our proofs are constructive and the results generalize a theorem of J. Sands [11]. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)     

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…