Search

Quantifier elimination is a foundational issue in the field of algebraic and logic computation. In first-order logic, every formula is well composed of atomic formulas by negation, conjunction, disjunction, and introducing quantifiers. It is often made quite complicated by the occurrences of quantifiers and nonlinear functions in atomic formulas. In this paper, we study a class of quantified exponential polynomial formulas extending polynomial ones, which allows the exponential to appear in the first variable. We then design a quantifier elimination procedure for these formulas. It adopts the scheme of cylindrical decomposition that consists of four phases—projection, isolation, lifting, and solution formula construction. For the non-algebraic representation, the triangular systems are introduced to define transcendental coordinates of sample points. Based on that, our cylindrical decomposition produces projections for input variables only. Hence the procedure is direct and effective. [ABSTRACT FROM AUTHOR]

Given a variety X over a perfect field, we study the partition defined on X by the multiplicity (into equimultiple points), and the effect of blowing up at smooth equimultiple centers. Over fields of characteristic zero we prove resolution of singularities by using the multiplicity as an invariant, instead of the Hilbert Samuel function. [ABSTRACT FROM AUTHOR]

Abstract: Video surveillance on highway is a hot topic and a great challenge in Intelligent Transportation Systems. In such applications requiring objects extraction, cast shadows induce shape distortions and object fusions interfering performance of high level algorithms. Shadow elimination allows to improve the performances of video object extraction, classification and tracking. In other hand, it is very important to recognize the type of a detected object in order to track reliably and estimate traffic parameters correctly. This paper presents two approaches to enhance automatic traffic surveillance systems. The first deals with the elimination of shadows and the second concerns the classification of vehicles, based on robust vision and image processing. For moving shadow elimination, a contrast model is proposed to describe and remove dynamic shadows based on the idea that a shadow transformation is a change in contrast. For vehicles classification, Hu moments are calculated in a manner to reduce the perspective effects and used to describe vehicles in knowledge base. Experimental results on the various challenging video sequences show that the proposed approach outperforms classification methods of related works (with a classification accuracy of 96.96%), and that the shadow elimination approach performs better than compared works (with detection rate of 95–99% and discrimination rate of 85.7–89%). [Copyright &y& Elsevier]

This paper shows that for any given polynomial ideal the collection of Gröbner cones corresponding to -specific elimination orders forms a star-shaped region which contrary to first intuition in general is not convex. Moreover we show that the corresponding region may contain Gröbner cones intersecting in the boundary of the Gröbner fan in the origin only. This implies that Gröbner walks aiming for the elimination of variables from a polynomial ideal can be terminated earlier than previously known. We provide a slightly improved stopping criterion for a known Gröbner walk algorithm for the elimination of variables. [ABSTRACT FROM AUTHOR]

Abstract: Newton, in notes that he would rather not have seen published, described a process for solving simultaneous equations that later authors applied specifically to linear equations. This method — which Euler did not recommend, which Legendre called “ordinary,” and which Gauss called “common” — is now named after Gauss: “Gaussian” elimination. Gauss’s name became associated with elimination through the adoption, by professional computers, of a specialized notation that Gauss devised for his own least-squares calculations. The notation allowed elimination to be viewed as a sequence of arithmetic operations that were repeatedly optimized for hand computing and eventually were described by matrices. [Copyright &y& Elsevier]

Abstract: In this paper we present some results showing the good behavior of the τ-invariant of a Rees algebra with integral closure and elimination (of variables). [ABSTRACT FROM AUTHOR]

Abstract: We study adjunct-elimination results for Context Logic applied to trees, following previous results by Lozes for Separation Logic and Ambient Logic. In fact, it is not possible to prove such elimination results for the original single-holed formulation of Context Logic. Instead, we prove our results for multi-holed Context Logic. [Copyright &y& Elsevier]

Abstract: We develop in this paper methods for studying the implicitization problem for a rational map defining a hypersurface in , based on computing the determinant of a graded strand of a Koszul complex. We show that the classical study of Macaulay resultants and Koszul complexes coincides, in this case, with the approach of approximation complexes and we study and give a geometric interpretation for the acyclicity conditions. Under suitable hypotheses, these techniques enable us to obtain the implicit equation, up to a power, and up to some extra factor. We give algebraic and geometric conditions for determining when the computed equation defines the scheme theoretic image of ϕ, and, what are the extra varieties that appear. We also give some applications to the problem of computing sparse discriminants. [Copyright &y& Elsevier]

Abstract: An improved algorithm, together with its implementation, is presented for the automatic computation of the complete root classification of a real parametric polynomial. The algorithm offers improved efficiency and a new test for non-realizable conditions. The improvement lies in the direct use of ‘sign lists’, obtained from the discriminant sequence, rather than ‘revised sign lists’. It is shown that the discriminant sequences, upon which the sign lists are based, are closely related both to Sturm–Habicht sequences and to subresultant sequences. Thus calculations based on any of these quantities are essentially equivalent. One particular application of complete root classifications is the determination of the conditions for the positive definiteness of a polynomial, and here the new algorithm is applied to a class of sparse polynomials. It is seen that the number of conditions for positive definiteness remains surprisingly small in these cases. [Copyright &y& Elsevier]

Abstract: We extend the recently proposed state-space restriction (SSR) technique for quantum spin dynamics simulations [Kuprov et al., J. Magn. Reson. 189 (2007) 241–250] to include on-the-fly detection and elimination of unpopulated dimensions from the system density matrix. Further improvements in spin dynamics simulation speed, frequently by several orders of magnitude, are demonstrated. The proposed zero track elimination (ZTE) procedure is computationally inexpensive, reversible, numerically stable and easy to add to any existing simulation code. We demonstrate that it belongs to the same family of Krylov subspace techniques as the well-known Lanczos basis pruning procedure. The combined SSR+ZTE algorithm is recommended for simulations of NMR, EPR and Spin Chemistry experiments on systems containing between 10 and 104 coupled spins. [Copyright &y& Elsevier]

Abstract: In functional brain mapping, pattern recognition methods allow detecting multivoxel patterns of brain activation which are informative with respect to a subject''s perceptual or cognitive state. The sensitivity of these methods, however, is greatly reduced when the proportion of voxels that convey the discriminative information is small compared to the total number of measured voxels. To reduce this dimensionality problem, previous studies employed univariate voxel selection or region-of-interest-based strategies as a preceding step to the application of machine learning algorithms. Here we employ a strategy for classifying functional imaging data based on a multivariate feature selection algorithm, Recursive Feature Elimination (RFE) that uses the training algorithm (support vector machine) recursively to eliminate irrelevant voxels and estimate informative spatial patterns. Generalization performances on test data increases while features/voxels are pruned based on their discrimination ability. In this article we evaluate RFE in terms of sensitivity of discriminative maps (Receiver Operative Characteristic analysis) and generalization performances and compare it to previously used univariate voxel selection strategies based on activation and discrimination measures. Using simulated fMRI data, we show that the recursive approach is suitable for mapping discriminative patterns and that the combination of an initial univariate activation-based (F-test) reduction of voxels and multivariate recursive feature elimination produces the best results, especially when differences between conditions have a low contrast-to-noise ratio. Furthermore, we apply our method to high resolution (2 × 2 × 2mm3) data from an auditory fMRI experiment in which subjects were stimulated with sounds from four different categories. With these real data, our recursive algorithm proves able to detect and accurately classify multivoxel spatial patterns, highlighting the role of the superior temporal gyrus in encoding the information of sound categories. In line with the simulation results, our method outperforms univariate statistical analysis and statistical learning without feature selection. [Copyright &y& Elsevier]

Abstract: Elimination is a classical subject. The problem is algorithmically solvable by using resultants or by one calculation of Groebner basis with respect to an elimination term order. However, there is no existing method that is both efficient and reliable enough for applicable size problems, say implicitization of bi-cubic Bezier surfaces with degree six in five variables. This basic and useful operation in computer aided geometric design and geometric modeling defies a solution even when approximation using floating-point or modular coefficients is used for Groebner basis computation. An elimination term order can be used to eliminate for any ideal in . However, for most practical problems we are given a fixed ideal, which means that an elimination term order may be too much for our calculation. In this paper, the author proposes a new approach for elimination. Instead of using a classical elimination term order for all problems or ideals as usual, the author proposes to use algebraic structures of the given system of equations for finding more suitable term orders for elimination of the given problem only. Experimental results showed that these ideal-specific term orders are much more efficient for elimination. In particular, when ideal specific term orders for elimination are used with Groebner walk conversion, one can completely avoid all perturbations. This is a significant result because researchers have been struggling with how to perturb basis conversions for a long time. [Copyright &y& Elsevier]

The purpose of this paper is to demonstrate how Lafont''s interaction combinators, a system of three symbols and six interaction rules, can be used to encode linear logic. Specifically, we give a translation of the multiplicative, exponential, and additive fragments of linear logic together with a strategy for cut-elimination which can be faithfully simulated. Finally, we show briefly how this encoding can be used for evaluating λ-terms. In addition to offering a very simple, perhaps the simplest, system of rewriting for linear logic and the λ-calculus, the interaction net implementation that we present has been shown by experimental testing to offer a good level of sharing in terms of the number of cut-elimination steps (resp. β-reduction steps). In particular it performs better than all extant finite systems of interaction nets. [Copyright &y& Elsevier]

New formulae are given for Chow forms, discriminants and resultants arising from (not necessarily normal) toric varieties of codimension 2. The Newton polygon of the discriminant is determined exactly. [Copyright &y& Elsevier]

Elimination of potential hypotheses is a fundamental component of many learning processes. In order to understand the nature of elimination, herein we study the following model of learning recursive functions from examples. On any target function, the learning machine has to eliminate all, save one, possible hypotheses such that the missing one correctly describes the target function. It turns out that this type of learning by the process of elimination (elm-learning, for short) can be stronger, weaker or of the same power as usual Gold style learning.While for usual learning any r.e. class of recursive functions can be learned in all of its numberings, this is no longer true for elm-learning. For elm-learnability of an r.e. class in a given of its numberings, we derive sufficient conditions of this numbering (decidability of index equivalence and paddability) as well as a condition being both necessary and sufficient. Then we deal with the problem of which r.e. classes are elm-learnable in all of their numberings and which are not.Elm-learning of arbitrary classes of recursive function is shown to be of the same power as usual learning. For elm-learnability of an arbitrary class in an arbitrary numbering, paddability of this numbering remains to be useful, whereas decidability of index equivalence can be “maximally weak” or “extremely useful”. We also give a characterization for elm-learnability of an arbitrary class of recursive functions.Finally, we consider some generalizations of elm-learning. One of them is of the same power as usual learning by teams. A further generalization even allows to learn the class of all recursive functions. [Copyright &y& Elsevier]

Focuses on the response elimination procedure. Information on experiments which were conducted; Information on methodologies used; Results and discussions of the experiments and methodologies; Indepth look at the elimination procedure.

We report on our on-going efforts to apply real quantifier elimination to the synthesis of optimal numerical algorithms. In particular, we describe a case study on the square root problem: given a real number x and an error bound ε , find a real interval such that it contains x and its width is less than or equal to ε . A typical numerical algorithm starts with an initial interval and repeatedly updates it by applying a “refinement map” on it until it becomes narrow enough. Thus the synthesis amounts to finding a refinement map that ensures the correctness and optimality of the resulting algorithm. This problem can be formulated as a real quantifier elimination. Hence, in principle, the synthesis can be carried out automatically. However, the computational requirement is huge, making the automatic synthesis practically impossible with the current general real quantifier elimination software. We overcame the difficulty by (1) carefully reducing a complicated quantified formula into several simpler ones and (2) automatically eliminating the quantifiers from the resulting ones using the state-of-the-art quantifier elimination software. As the result, we were able to synthesize semi-automatically an optimal quadratically 1 convergent map, which is better than the well known hand-crafted Secant-Newton map. Interestingly, the optimal synthesized map is not contracting as one would naturally expect. [ABSTRACT FROM AUTHOR]

Abstract: In this report a method for common subexpression elimination in matrices is explored. The method is applied to several types of matrices occurring in numerical simulations. In all cases, the cost of a matrix–vector multiplication is reduced by a significant amount. The amount of storage required for the eliminated matrices is also less than that required for the original matrices. When the proposed method is applied to the Fourier transform matrix, the output is equivalent to the fast Fourier transform. For some matrices used in the fast multipole method for dislocation dynamics, the cost of a matrix–vector multiplication is reduced from to , where p is the expansion order. Using an expansion order of 5, one can expect a factor of four speedup of the fast multipole part of a dislocation dynamics code. [Copyright &y& Elsevier]

Abstract: Let be a field of characteristic zero, any positive integer and let be the derivation of the polynomial ring in variables over . A Conjecture of Nowicki (Conjecture 6.9.10 in [Nowicki, A. 1994. Polynomial derivations and their rings of constants, Wydawnictwo Uniwersytetu Mikolaja Kopernika, Torun]) states the following in which case we say that is standard. In this paper, we use the elimination theory of Groebner bases to prove that Nowicki’s conjecture holds in the more general case of the derivation , . In [Kojima, H. Miyanishi, M. 1997. On Robert’s counterexample to the fourteenth problem of Hilbert, J. Pure Appl. Algebra 122, 277–292], Kojima and Miyanishi argued that is standard in the case where () for some . Although the result is true, we show in this paper that their proof is not complete. [Copyright &y& Elsevier]

We develop a finite volume method based on Crank-Nicolson time discretization for the two-dimensional nonsymmetric Riemann-Liouville space-fractional diffusion equation. Stability and convergence are then carefully discussed. We prove that the finite volume scheme is unconditionally stable and convergent with second-order accuracy in time and min ⁡ { 1 + α , 1 + β } order in space with respect to a weighted discrete norm. Here 0 < α , β < 1 are the space-fractional order indexes in x and y directions, respectively. Furthermore, we rewrite the finite volume scheme into a matrix form and develop a matrix-free preconditioned fast Krylov subspace iterative method, which only requires storage of O (N) and computational cost of O (N log ⁡ N) per iteration without losing any accuracy compared to the direct Gaussian elimination method. Here N is the total number of spatial unknowns. Consequently, the fast finite volume method is particularly suitable for large-scale modeling and simulation. Numerical experiments verify the theoretical results and show strong potential of the fast method. • A Crank-Nicolson finite volume method is proposed for two-dimensional Riemann-Liouville space-fractional diffusion equation. • A novel norm-based stability analysis is proposed for non-symmetric anomalously diffusive transport. • A priori error estimate with respect to a weighted discrete norm is strictly proved. • A matrix-free preconditioned fast solution method with almost linear computational complexity is developed. • Numerical experiments are given to verify the theoretical findings. [ABSTRACT FROM AUTHOR]

We reconsider whether a grand multi-winner contest elicits more equilibrium effort than a collection of sub-contests. Fu and Lu (2009) employ a sequential winner-selection mechanism and find support for running a grand contest. We show that this result is completely reversed if a simultaneous winner-selection mechanism or a sequential loser-elimination mechanism is implemented. We then discuss the optimal allocation of players and prizes among sub-contests. [ABSTRACT FROM AUTHOR]

A quantifier elimination algorithm by cylindrical algebraic decomposition based on regular chains is presented. The main idea is to refine a complex cylindrical tree until the signs of polynomials appearing in the tree are sufficient to distinguish the true and false cells. We report an implementation of our algorithm in the RegularChains library in Maple and illustrate its effectiveness by examples. [ABSTRACT FROM AUTHOR]

Abstract: The literature describes two high performance concurrent stack algorithms based on combining funnels and elimination trees. Unfortunately, the funnels are linearizable but blocking, and the elimination trees are non-blocking but not linearizable. Neither is used in practice since they perform well only at exceptionally high loads. The literature also describes a simple lock-free linearizable stack algorithm that works at low loads but does not scale as the load increases. The question of designing a stack algorithm that is non-blocking, linearizable, and scales well throughout the concurrency range, has thus remained open. This paper presents such a concurrent stack algorithm. It is based on the following simple observation: that a single elimination array used as a backoff scheme for a simple lock-free stack is lock-free, linearizable, and scalable. As our empirical results show, the resulting elimination-backoff stack performs as well as the simple stack at low loads, and increasingly outperforms all other methods (lock-based and non-blocking) as concurrency increases. We believe its simplicity and scalability make it a viable practical alternative to existing constructions for implementing concurrent stacks. [Copyright &y& Elsevier]

Abstract: The reaction network and mechanism of the hydrodenitrogenation (HDN) of 2-methylpyridine and 2-methylpiperidine were studied at 280–340 °C and 1–3 MPa in the absence and presence of H2S over sulfided NiMo/γ-Al2O3. By the addition of 2-ethylpiperidine to the HDN of 2-methylpyridine and of 2-ethylpyridine to the HDN of 2-methylpiperidine, the mutual inhibiting effects of 2-methylpyridine and 2-methylpiperidine could be determined. 2-Ethylpyridine hardly affected the HDN of 2-methylpiperidine, but 2-ethylpiperidine strongly retarded the hydrogenation of 2-methylpyridine and promoted its denitrogenation at low partial pressure and inhibited it at high partial pressure. Substantial amounts of 2,3,4,5-tetrahydro-6-methylpyridine were detected in the HDN reactions; thus, its HDN was studied. This imine intermediate reacted very rapidly to 2-methylpiperidine by hydrogenation. 2-Methylpiperidine reacted to 1-hexylamine and even more strongly to 2-hexylamine. The final hydrocarbon products were 1-hexene, 2-hexene, and hexane. Based on these results and on previous HDN studies of dialkylamines, we propose that 2-methylpyridine first reacts by hydrogenation to 2-methylpiperidine and that both react to the imines 2,3,4,5-tetrahydro-2-methylpyridine and 2,3,4,5-tetrahydro-6-methylpyridine. Breaking of the first Cd ring opening of the imines occurs as a result of the addition of H2S, elimination, and hydrogenation, forming amino-hexanethiols. The amino-hexanethiols react by hydrogenolysis to hexylamines, and the second C broken by hexylimine formation, H2S addition, and NH3 elimination. [Copyright &y& Elsevier]

A method for eliminating residual vibrations in multimode systems is presented using a command shaping technique. The proposed command shaping technique captures two main advantages. Namely, the independence of the time length of the shaped command from the resonant frequencies of the system, and the ability to generate the command profile without a full system model. Experiments on systems with partial models represented by their resonant frequencies show that shaped command profiles generated using actual measured resonant frequencies of a system outperform those based on mathematical models. This feature of the proposed command shaping technique makes it very attractive for complicated multimode systems where mathematical models are difficult to build. Profiles of the proposed shaped command are simple and do not require intensive calculations. Performance of the proposed shaped command is validated using numerical simulations and experiments. Numerical simulations prove that the shaped commands are capable of completely eliminating residual vibrations of multimode systems. Experiments show that residual vibration elimination depends on the level of accuracy of the measured resonant frequencies of the system. [ABSTRACT FROM AUTHOR]

Given the equations of the first and the second order manifolds in R n , we construct the distance equation , i.e. a univariate algebraic equation one of the zeros of which (generically minimal positive) coincides with the square of the distance between these manifolds. To achieve this goal we employ Elimination Theory methods. In the frame of this approach we also deduce the necessary and sufficient algebraic conditions under which the manifolds intersect and propose an algorithm for finding the coordinates of their nearest points. The case of parameter dependent manifolds is also considered. [ABSTRACT FROM AUTHOR]

Abstract: One may represent polynomials not only by their coefficients but also by arithmetic circuits which evaluate them. This idea allowed in the past fifteen years considerable complexity progress in effective polynomial equation solving. We present a circuit based computation model which captures all known symbolic elimination algorithms in effective Algebraic Geometry and exhibit a class of simple elimination problems which require exponential size circuits to be solved in this model. This implies that the known, circuit based elimination algorithms are already optimal. [Copyright &y& Elsevier]

Abstract: In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the system reduces to a corresponding normal proof. This paper develops a system of modal logic that is capable of expressing the notion of normal proof within the system itself, thereby making normal proofs an inherent property of the logic. Using a modality △ to express the existence of a normal proof, the system provides a means for both recognizing and manipulating its own normal proofs. We develop the system as a sequent calculus with the implication connective ⊃ and the modality △, and prove the cut elimination theorem. From the sequent calculus, we derive two equivalent natural deduction systems. [Copyright &y& Elsevier]

Abstract: The concept of pregroup was introduced by Lambek for natural language analysis, with a close link to non-commutative linear logic. We reformulate the pregroup calculus so as to extend it by composition with other logics and calculi. The cut elimination property and the decidability property of the sequent calculus proposed in the article are shown. Properties of composed calculi are also discussed. [Copyright &y& Elsevier]

Abstract: We give the first known bound for orders of differentiations in differential Nullstellensatz for both partial and ordinary algebraic differential equations. This problem was previously addressed in [A. Seidenberg, An elimination theory for differential algebra, Univ. of California Publ. in Math. III (2) (1956) 31–66] but no complete solution was given. Our result is a complement to the corresponding result in algebraic geometry, which gives a bound on degrees of polynomial coefficients in effective Nullstellensatz [G. Hermann, Die Frage der endlich vielen Schritte in der Theorie der Polynomideale, Math. Ann. 95 (1) (1926) 736–788; E.W. Mayr, A.W. Meyer, The complexity of the word problems for commutative semigroups and polynomial ideals, Adv. Math. 46 (3) (1982) 305–329; W.D. Brownawell, Bounds for the degrees in the Nullstellensatz, Ann. of Math. 126 (3) (1987) 577–591; J. Kollár, Sharp effective Nullstellensatz, J. Amer. Math. Soc. 1 (4) (1988) 963–975; L. Caniglia, A. Galligo, J. Heintz, Some new effectivity bounds in computational geometry, in: Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, Rome, 1988, in: Lecture Notes in Comput. Sci., vol. 357, Springer, Berlin, 1989, pp. 131–151; N. Fitchas, A. Galligo, Nullstellensatz effectif et conjecture de Serre (théorème de Quillen–Suslin) pour le calcul formel, Math. Nachr. 149 (1990) 231–253; T. Krick, L.M. Pardo, M. Sombra, Sharp estimates for the arithmetic Nullstellensatz, Duke Math. J. 109 (3) (2001) 521–598; Z. Jelonek, On the effective Nullstellensatz, Invent. Math. 162 (1) (2005) 1–17; T. Dubé, A combinatorial proof of the effective Nullstellensatz, J. Symbolic Comput. 15 (3) (1993) 277–296]. This paper is dedicated to the memory of Eugeny Pankratiev, who was the advisor of the first three authors at Moscow State University. [Copyright &y& Elsevier]

Abstract: We revisit in this paper the concept of decoding binary cyclic codes with Gröbner bases. These ideas were first introduced by Cooper, then Chen, Reed, Helleseth and Truong, and eventually by Orsini and Sala. We discuss here another way of putting the decoding problem into equations: the Newton identities. Although these identities have been extensively used for decoding, the work was done manually, to provide formulas for the coefficients of the locator polynomial. This was achieved by Reed, Chen, Truong and others in a long series of papers, for decoding quadratic residue codes, on a case-by-case basis. It is tempting to automate these computations, using elimination theory and Gröbner bases. Thus, we study in this paper the properties of the system defined by the Newton identities, for decoding binary cyclic codes. This is done in two steps, first we prove some facts about the variety associated with this system, then we prove that the ideal itself contains relevant equations for decoding, which lead to formulas. Then we consider the so-called online Gröbner basis decoding, where the work of computing a Gröbner basis is done for each received word. It is much more efficient for practical purposes than preprocessing and substituting into the formulas. Finally, we conclude with some computational results, for codes of interesting length (about one hundred). [Copyright &y& Elsevier]

Abstract: The aim of this article is to link Schubert varieties in the flag manifold with hyperplane arrangements. For a permutation, we construct a certain graphical hyperplane arrangement. We show that the generating function for regions of this arrangement coincides with the Poincaré polynomial of the corresponding Schubert variety if and only if the Schubert variety is smooth. We give an explicit combinatorial formula for the Poincaré polynomial. Our main technical tools are chordal graphs and perfect elimination orderings. [Copyright &y& Elsevier]