Search

Collins introduced the cylindrical algebraic decomposition method for eliminating quantifiers in real arithmetic formulas. In our work we use this method for satisfiability checking in satisfiability modulo theories solver technologies, and tune it by trying to avoid some computation steps that are needed for quantifier elimination but not for satisfiability checking. We further propose novel data structures and adapt the method to work incrementally and to support backtracking. We verify the effectiveness experimentally by comparing different versions of the cylindrical algebraic decomposition used within a state-of-the-art satisfiability modulo theories solver.

International audience; We consider feasibility of linear integer problems in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer problems is decidable, many state-of-the-art implementations neglect termination in favor of efficiency. We present thecalculus CutSat++ that is sound, terminating, complete, and leaves enough space for model assumptions and simplification rules in order to be efficient in practice. CutSat++ combines model-driven reasoning and quantifier elimination to the feasibility of linear integer problems.

In the context of trajectory planning for autonomous vehicles, a widely used vehicle model relies on linear integrator dynamics. We consider planning with this model type, with a focus on the requirement to account for curved road topologies. As our analysis reveals, this generally gives rise to non-convex, coupled constraints on the vehicle’s states and inputs, which impedes computationally efficient planning. We propose a method to resolve this issue by modification of the non-convex constraints. This modification is based on inner approximations of sub-level sets of nonlinear functions, which are obtained by quantifier elimination. The efficacy of the method is demonstrated in two example scenarios.

We study the model theoretic structure $(\Z,+,P_r)$ where $r>1$ is an irrational number and the elements of $P_r$ are of the form $\floor{nr}$ for some $n\in\Z\setminus\{0\}$. We axiomatize of this structure and prove a quantifier elimination result. As a consequence, we get that definable subsets are not sparse unless they are finite. We also prove that there are no reducts of this structure expanding $(\Z,+)$.

This study covers an analytical approach to calculate positive invariant sets of dynamical systems. Using Lyapunov techniques and quantifier elimination methods, an automatic procedure for determining bounds in the state space as an enclosure of attractors is proposed. The available software tools permit an algorithmizable process, which normally requires a good insight into the systems dynamics and experience. As a result we get an estimation of the attractor, whose conservatism only results from the initial choice of the Lyapunov candidate function. The proposed approach is illustrated on the well-known Lorenz system.

In this work we study the intrinsic complexity of elimination algorithms in effective algebraic geometry and we focus our attention to elimination algorithms produced within the object–oriented paradigm. To this end, we describe a new computation model called quiz game (introduced in [1]) which models the notions of information hiding (due to Parnas, see [8]) and non–functional requirements (e.g. robustness) among other important concepts in software engineering. This characteristic distinguish our model from classical computation models such as the Turing machine or algebraic models. We illustrate our computation model with a non–trivial complexity lower bound for the identity function of polynomials. We show that any object–oriented (and robust) implementation of the identity function of polynomials is necessarily inefficient compared with a trivial implementation of this function. This result shows an existing synergy between Software Engineering and Algebraic Complexity Theory. Keywords: Abstract data type, abstraction function, data structure, information hiding, lower complexity bound, non–functional requirement, quantifier elimination, quiz game, robustness, scientific computing.

In this paper we study fundamental model-theoretic questions for free associative algebras, namely, first-order classification, decidability of the first-order theory, and definability of the set of free bases. We show that two free associative algebras of finite rank over fields, at least one of which is infinite, are elementarily equivalent if and only if either their ranks are finite and equal or both are infinite and the fields are equivalent in the weak second order logic. In particular, two free associative algebras of finite rank over the same field are elementarily equivalent if and only if they are isomorphic. We prove that if an arbitrary ring B with at least one Noetherian proper centralizer is first-order equivalent to a free associative algebra of finite rank over an infinite field then B is also a free associative algebra of finite rank over a field. This solves the elementary classification problem for free associative algebras in a wide class of rings (in fact, we note that a finitely generated algebra for which this result would not solve the classification problem would be a true monster). We also present a formula of the pure ring language which defines the set of free bases in a free associative algebra A K ( X ) with finite basis X over an infinite field K . To prove this result we establish rather deep connections between first order theory of A K ( X ) and the weak second order theory of the field K . In fact, we prove that A K ( X ) and the weak second order theory of K (the superstructure H F ( K ) ) are bi-interpretable in each other. Finally, we show that the arithmetical hierarchy over A K ( X ) is proper, in particular there is no any reasonable “quantifier elimination” in free associative algebras.

This note presents a counterexample that illustrates why the lack of absolute continuity destroys the correctness of a main result of Liu (2008) and provides a modified model for the minimax RIM quantifier problem and the correct formulation of Liu's result.

The classical energy method for the approximate determination of critical buckling loads of bars is revisited. This method is based on the stability condition of the bar and on the appropriate selection of an approximation to the deflection of the bar. Moreover, it is frequently related to the Rayleigh quotient or to the Timoshenko quotient for the determination of the critical buckling load. Here we will use again the energy method for the determination of critical buckling loads of bars but now on the basis of a new computational approach. This new approach consists of using the modern computational method of quantifier elimination efficiently implemented in the computer algebra system Mathematica instead of partial differentiations when we use the stability condition of the bar or essentially equivalently when we minimize the Rayleigh quotient or the Timoshenko quotient. This approach, which avoids partial differentiations, is also more rigorous than the classical approach based on partial derivatives because it does not require the use of the conditions for a minimum based on second partial derivatives, which are generally ignored in practice. Moreover, it is very simple to use inside the powerful computational environment offered by Mathematica. The present approach is illustrated in several buckling problems of bars including parametric buckling problems. Buckling problems of bars with two internal unilateral constraints, where the classical energy method is difficult to apply, are also studied. Even in this rather difficult application the critical buckling load is directly determined with a sufficient accuracy.

The method of caustics is a powerful experimental method in elasticity and particularly in fracture mechanics for crack problems. The related method of pseudocaustics is also of interest. Here we apply the computational method of quantifier elimination implemented in the computer algebra system Mathematica in order to determine (i) the non-parametric equation and two properties of the caustic at a crack tip and especially (ii) the illuminated and the dark regions related to caustics and pseudocaustics in plane elasticity and plate problems. The present computations concern: (i) The derivation of the non-parametric equation of the classical caustic about a crack tip through the elimination of the parameter involved (here the polar angle) as well as two geometrical properties of this caustic. (ii) The derivation of the inequalities defining the illuminated region on the screen in the problem of an elastic half-plane loaded normally by a concentrated load with the boundary of this illuminated region related to some extent to the caustic formed. (iii) Similarly for the problem of a clamped circular plate under a uniform loading with respect to the caustic and the pseudocaustic formed. (iv) Analogously for the problem of an equilateral triangular plate loaded by uniformly distributed moments along its whole boundary, which defines the related pseudocaustic. (v) The determination of quantities of interest in mechanics from the obtained caustics or pseudocaustics. The kind of computations in the applications (ii) to (iv), i.e. the derivation of inequalities defining the illuminated region on the screen, seems to be completely new independently of the use here of the method of quantifier elimination. Additional applications are also possible, but some of them require the expansion of the present somewhat limited power of the quantifier elimination algorithms in Mathematica . This is expected to take place in the future.

A kind of personalized quantifier, the so-called SEVSI-induced quantifier as an acronym for Subjective Expected Value of Sample Information, is developed in this paper by introducing Bernstein polynomials of higher degree. This allows us to provide a novel solution to improve the final representation of the quantifier that generally performed poorly in our previous work, thus enhancing the quality of global approximation of functions and improving the operability of this kind of quantifier for practical use. We show some properties of the developed quantifier. We also prove the consistency of the OWA aggregation under the guidance of this type of quantifier. Finally, we experimentally show that the developed quantifier outperforms the one with the piecewise linear interpolation in many aspects of geometrical characteristics and operability. Thus it could be considered as an effective analytical tool to help handle the complex cases involving people's personalities or behavior intentions that have to be considered in decision making under uncertainty.

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 e, find a real interval such that it contains x and its width is less than or equal to e.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 quadratically1 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.

Le groupe des decimales avec l'addition modulo 1 et l'ordre naturel, qui n'est pas un groupe ordonne au sens habituel, est utilise pour ameliorer l'efficacite des automates temporels ([1]). Dans cette note, on donne une axiomatisation de cette structure, et on montre qu'elle admet l'elimination des quantificateurs. / ABSTRACT. The logic of fractional parts or real numbers. The group of decimals with addition modulo 1 and the natural order, which is not an ordered group in the usual sense, is used to enhance the efficiency of timed automata ([1]). In this note, we axiomatize this structure and show it admits quantifier elimination.

The Weak Nilpotent Minimum logic WNM was introduced by Esteva and Godo in 6 and shown to be the logic of the class of weak nilpotent minimum triangular norms. In this article, we prove that WNM admits the Deductive Interpolation Property by showing through a model-theoretic argument that the corresponding variety of algebras has the Amalgamation Property.

International audience; We consider existential problems over the reals. Extended quanti-fier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination for the quadratic case via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers , which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.

The classical problem of a beam on a tensionless Winkler elastic foundation is reconsidered for the derivation of the conditions of complete contact between the beam and the foundation. This is achieved through the application of modern quantifier elimination software included in the computer algebra system Mathematica together with Taylor–Maclaurin series approximations to the deflection of the beam. Four particular beam problems have been considered in detail and the related QFFs (quantifier-free formulae) have been obtained for several values of the order in the series approximations. Additional approximation possibilities have also been investigated with an emphasis put on the use of the Galerkin method based on weighted residuals. The present results seem to constitute one more interesting application of modern quantifier elimination algorithms and the related software (here in Mathematica ) to applied and engineering mechanics.

We consider the use of Quanti fier Elimination (QE) technology for automated reasoning in economics. There is a great body of work considering QE applications in science and engineering but we demonstrate here that it also has use in the social sciences. We explain how many suggested theorems in economics could either be proven, or even have their hypotheses shown to be inconsistent automatically via QE. However, economists who this technology could bene t are usually unfamiliar with QE, and the use of mathematical software generally. This motivated the development of a Mathematica Package TheoryGuru, whose purpose is to lower the costs of applying QE to economics. We describe the package's functionality and give examples of its use.

This paper addresses the issue of potential invariant generation in the formal analysis of transition systems with k-induction, in the linear real/integer arithmetic fragment. First, quantifier elimination is used to find parameters for generic templates such that the said templates become inductive. Second, a backward analysis, also using quantifier elimination, outputs preimages of the negation of the proof objective, viewed as unauthorized states, or gray states. Two heuristics are proposed to take advantage of this source of information and generate potential invariants: a thorough exploration of the possible partitionings of the gray state space, and an inexact exploration regrouping and over-approximating disjoint areas of the gray state space. Both aim at discovering hidden relations between state variables. K-induction is used to isolate actual invariants and to check if they make the proof objective inductive. These heuristics can be used on the first preimage of the backward exploration, and each time a new one is output, refining the information on the gray states. We show, on examples of interest in the application field of critical embedded systems, that our approach is able to prove properties for which other academic or commercial tools fail. The different methods are introduced as components of a collaborative formal verification framework based on k-induction and are motivated through two examples, one of which was provided by Rockwell Collins. In this paper, the authors presented two automatic and property directed potential invariant generation heuristics.The first one uses quantifier elimination to find values for template parameters such that said template becomes inductive.The second one operates on preimages of the negation of the proof objective obtained by a backward exploration, itself powered by quantifier elimination.The preimages are fed to two potential invariant extraction heuristics.

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.

We give foundational results for the model theory of A K fin , the ring of finite adeles over a number field, construed as a restricted product of local fields. In contrast to Weispfenning we work in the language of ring theory, and various sortings interpretable therein. In particular we give a systematic treatment of the product valuation and the valuation monoid. Deeper results are given for the adelic version of Krasner's hyperfields, relating them to the Basarab–Kuhlmann formalism.

We present an algebraic characterization of both o-minimal and weakly o-minimal MV-chains by showing that a linearly ordered MV-algebra is ( 1 ) o-minimal if and only if it is finite or divisible, and ( 2 ) weakly o-minimal if and only if its first-order theory admits quantifier elimination in the language 〈 ⊕ , ∗ , 0 〉 if and only if R a d ( A ) is a divisible monoid and A / R a d ( A ) is either finite or divisible.

Termination is an essential part of program correctness. For a class of regular programs, both automatically proving termination and constructing witnesses of nontermination are significant in theoretical computer science. Many traditional theorem-proving methods for analyzing termination are based on Presburger arithmetic or linear programming, so they are valid only for restricted linear problems. On the contrary, some newly-emerged algebraic methods are suitable for polynomial problems, and are promising in deciding termination of polynomial programs. In this paper, we investigate a large class of imperative programs, called solvable loops, whose guards are general polynomials and assignments are special polynomial mappings. We then propose some sufficient criteria for proving termination and nontermination of such loops in parallel. These criteria can further be translated to the quantifier elimination problem over the reals, and hence are computable. Finally, feasible sample points in the process for inferring nontermination are eventually nonterminating inputs, which can be used to generate witnesses of nontermination. Our decision procedure uses symbolic computation and is mechanically implementable in spite of considerably high complexity. Thereby a series of strong and exact results are established in analyzing termination of loops.

Liu and Lou [Fuzzy Sets and Systems 159 (2007) 1673-1688] investigated the equivalence of solutions to the maximum entropy and minimax ratio RIM quantifier problems. The paper improves Liu and Lou's theorems from a mathematical perspective. Because their theorems are not suitable for absolutely continuous generating functions, the paper provides a correct proof of the minimax ratio RIM quantifier problem for the case in which generating functions are absolutely continuous and a generalized solution to the maximum entropy RIM quantifier problem for the case in which generating functions are Lebesgue integrable. Based on the results, the paper provides a correct relationship between the maximum entropy and minimax ratio RIM quantifier problems.

The problem of eliminating second-order quantification over predicate symbols is in general undecidable. Since an application of second-order quantifier elimination is correspondence theory in modal logic, understanding when second-order quantifier elimination methods succeed is an important problem that sheds light on the kinds of axioms that are equivalent to first-order correspondence properties and can be used to obtain complete axiomatizations for modal logics. This paper introduces a substitution-rewrite approach based on Ackermannʼs Lemma to second-order quantifier elimination in modal logic. Compared to related approaches, the approach includes a number of enhancements: The quantified symbols that need to be eliminated can be flexibly specified. The inference rules are restricted by orderings compatible with the elimination order, which provides more control and reduces non-determinism in derivations thereby increasing the efficiency and success rate. The approach is equipped with a powerful notion of redundancy, allowing for the flexible definition of practical simplification and optimization techniques. We present correctness, termination and canonicity results, and consider two applications: (i) computing first-order frame correspondence properties for modal axioms and rules, and (ii) rewriting second-order modal problems to equivalent simpler forms. The approach allows us to define and characterize two new classes of formulae, which are elementary and canonical, and subsume the class of Sahlqvist formulae and the class of monadic inductive formulae.

We present a generalization of the Cylindrical Algebraic Decomposition (CAD) algorithm to systems of equations and inequalities in functions of the form p(x,f"1(x),...,f"m(x),y"1,...,y"n), where [email protected]?Q[x,t"1,...,t"m,y"1,...,y"n] and f"1(x),...,f"m(x) are real univariate functions such that there exists a real root isolation algorithm for functions from the algebra Q[x,f"1(x),...,f"m(x)]. In particular, the algorithm applies when f"1(x),...,f"m(x) are real exp-log functions or tame elementary functions.

Recently, Liu and Lou [On the equivalence of some approaches to the OWA operator and RIM quantifier determination, Fuzzy Sets and Systems 159 (2007) 1673-1688] investigated the equivalence of solutions to the minimum-variance and minimax disparity RIM quantifier problems. However, their proofs are very sensitive to the assumption, and some are mathematically incomplete. In this regard, this paper provides a counterexample of the minimax disparity RIM quantifier problem for the case in which generating functions are continuous. The paper also provides a correct proof of the minimax disparity RIM quantifier problem for the case in which generating functions are absolutely continuous and a generalized result for the minimum-variance RIM quantifier problem for the case in which generating functions are Lebesgue integrable. Based on the results, the paper provides a correct relationship between the minimum-variance and minimax disparity RIM quantifier problems.

The dominance relationship between two members of the family of Sugeno-Weber t-norms is proven by using a quantifier elimination algorithm. Further it is shown that dominance is a transitive, and therefore also an order relation, on this family of t-norms.

Tiwari proved that termination of linear programs (loops with linear loop conditions and updates) over the reals is decidable through Jordan forms and eigenvectors computation. Braverman proved that it is also decidable over the integers. In this paper, we consider the termination of loops with polynomial loop conditions and linear updates over the reals and integers. First, we prove that the termination of such loops over the integers is undecidable. Second, with an assumption, we provide an complete algorithm to decide the termination of a class of such programs over the reals. Our method is similar to that of Tiwari in spirit but uses different techniques. Finally, we conjecture that the termination of linear programs with polynomial loop conditions over the reals is undecidable in general by %constructing a loop and reducing the problem to another decision problem related to number theory and ergodic theory, which we guess undecidable., 17pages, 0 figures

Whether the determinant of the Dixon matrix equals zero or not is used for determining if a system of n + 1 polynomial equations in n variables has a common root, and is a very efficient quantifier elimination approach too. But for a complicated polynomial system, it is not easy to construct the Dixon matrix. In this paper, a recursive algorithm to construct the Dixon matrix is proposed by which some problems that cannot be tackled by other methods can be solved on the same computer platform. A dynamic programming algorithm based on the recursive formula is developed and compared for speed and efficiency to the recursive algorithm.

This paper presents an algebraic approach to polynomial spectral factorization, an important mathematical tool in signal processing and control. The approach exploits an intriguing relationship between the theory of Gröbner bases and polynomial spectral factorization which can be observed through the sum of roots, and allows us to perform polynomial spectral factorization in the presence of real parameters. It is discussed that parametric polynomial spectral factorization enables us to express quantities such as the optimal cost in terms of parameters and the sum of roots. Furthermore an optimization method over parameters is suggested that makes use of the results from parametric polynomial spectral factorization and also employs two quantifier elimination techniques. This proposed approach is demonstrated in a numerical example of a particular control problem.

PCS (Proving-Computing-Solving) introduced by B. Buchberger in 2001 and S-Decomposition, introduced by T. Jebelean in 2001, are strategies for handling proof problems by combining logic inference steps (e.g., modus ponens, Skolemization, instantiation) with rewriting steps (application of definitions) and solving procedures based on algebraic techniques (e.g., Groebner Bases, Cylindrical Algebraic Decomposition). If one formalizes the main notions of elementary analysis like continuity, convergence, etc., usually a sequence of alternating quantifier blocks appears in the quantifier prefix of the corresponding formula. This makes the proof problems involving these notions difficult. The S-Decomposition strategy is especially suitable for property-preserving problems like continuity of sum, because it is designed for handling problems where the goal and the main assumptions have a similar structure. During proof deduction, existentially quantified goals and universal assumptions are handled by introducing metavariables, if no suitable ground instance is known in advance. For finalizing proof attempts, the metavariables must be instantiated in such a way that they satisfy the cumulated algebraic constraints collected during the proof attempt. The instantiation problem is considered to be difficult in a purely logical calculus. Appropriate instances can be often found using quantifier elimination (QE) over real closed fields. In order to obtain witness terms we utilize the QE method based on cylindrical algebraic decomposition (CAD) invented by G. Collins in 1973. However, the QE method alone is not sufficient. One needs to pre-process the (closed, quantified) conjectured formula and post-process the resulting CAD-structure after the call of the QE algorithm.

The ordered weighted averaging (OWA) operator is a widely used aggregation method, and its determination is usually a prerequisite step in many related applications. The regular increasing monotone (RIM) quantifier can be seen as the continuous case of the OWA operator with the quantifier aggregation method. Some approaches with optimization criteria for the determination of OWA operator and RIM quantifier were proposed. Although these problems look different at the first sight, a deeper investigation can reveal the equivalence of solutions between them. Inspired by the solution equivalence of minimum variance problems and minimax disparity problem for OWA operator, we propose the minimax disparity RIM quantifier problem and two minimax ratio problems for OWA operator and RIM quantifier, respectively. We investigate the equivalence of solutions for the maximum entropy and minimax ratio problems, and solutions for the minimum variance and minimax disparity problems of OWA operator and RIM quantifier, respectively, by a theoretical point of view.

We prove quantifier elimination in Witt vectors over an algebraically closed fields (or in power series), considered as a valued module over the Ore ring of Frobenius polynomials. We get that these structures do not have the independence property. To cite this article: L. Belair, F. Point, C. R. Acad. Sci. Paris, Ser. I 346 (2008). Resume On donne un algorithme d'elimination des quantificateurs dans les vecteurs de Witt sur un corps algebriquement clos (ou encore dans les series formelles), vus comme module value sur l'anneau de Ore des polynomes de Frobenius. On obtient alors que ces structures n'ont pas la propriete d'independance. Pour citer cet article : L. Belair, F. Point, C. R. Acad. Sci. Paris, Ser. I 346 (2008).

In this paper, quantified Horn formulas (QHORN) are investigated. We prove that the behavior of the existential quantifiers depends only on the cases where at most one of the universally quantified variables is zero. Accordingly, we give a detailed characterization of QHORN satisfiability models which describe the set of satisfying truth assignments to the existential variables. We also consider quantified Horn formulas with free variables (QHORN^*) and show that they have monotone equivalence models. The main application of these findings is that any quantified Horn formula @F of length |@F| with free variables, |@?| universal quantifiers and an arbitrary number of existential quantifiers can be transformed into an equivalent quantified Horn formula of length O(|@?|.|@F|) which contains only existential quantifiers. We also obtain a new algorithm for solving the satisfiability problem for quantified Horn formulas with or without free variables in time O(|@?|.|@F|) by transforming the input formula into a satisfiability-equivalent propositional formula. Moreover, we show that QHORN satisfiability models can be found with the same complexity.

The Dixon resultant method solves a system of polynomial equations by computing its resultant. It constructs a square matrix whose determinant (det) is a multiple of the resultant (res). The naive way to proceed is to compute det, factor it, and identify res. But often det is too large to compute or factor, even though res is relatively small. In this paper we describe three heuristic methods that often overcome these problems. The first, although sometimes useful by itself, is often a subprocedure of the second two. The second may be used on any polynomial system to discover factors of det without producing the complete determinant. The third applies when res appears as a factor of det in a certain exponential pattern. This occurs in some symmetrical systems of equations. We show examples from computational chemistry, signal processing, dynamical systems, quantifier elimination, and pure mathematics.

Most well-known algorithms for equational solving are based on quantifier elimination. This technique iteratively eliminates the innermost block of existential/universal quantifiers from prenex formulas whose matrices are in some normal form (mostly DNF). Traditionally used notions of normal form satisfy that every constraint (in normal form) different from false is trivially satisfiable. Hence, they are called solved forms. However, the manipulation of such constraints require hard transformations, especially due to the use of the distributive and the explosion rules, which increase the number of constraints at intermediate stages of the solving process. On the contrary, quasi-solved forms allow for simpler transformations by means of a more compact representation of solutions, but their satisfiability test is not so trivial. Nevertheless, the total cost of checking satisfiability and manipulating constrains using quasi-solved forms is cheaper than using simpler solved forms. Therefore, they are suitable for improving the efficiency of constraint solving procedures. In this paper, we present a notion of quasi-solved form that provides a good trade-off between the cost of checking satisfiability and the effort required to manipulate constraints. In particular, our new quasi-solved form has been carefully designed for efficiently handling conjunction and negation, which are the main Boolean operations necessary to keep matrices of formulas in normal form.

The development of a multicellular organism is a dynamic process. Starting with one or a few cells, the organism develops into different types of cells with distinct functions. We have constructed a simple model by considering the cell number increase and the cell-type order conservation, and have assessed conditions for cell-type diversity. This model is based on a stochastic Lindenmayer system with cell-to-cell interactions for three types of cells. In the present model, we have successfully derived complex but rigorous algebraic relations between the proliferation and transition rates for cell-type diversity by using a symbolic method: quantifier elimination (QE). Surprisingly, three modes for the proliferation and transition rates have emerged for large ratios of the initial cells to the developed cells. The three modes have revealed that the equality between the development rates for the highest cell-type diversity is reduced during the development process of multicellular organisms. Furthermore, we have found that the highest cell-type diversity originates from order conservation.

We have been developing a toolbox on Maple, called SyNRAC, for solving real algebraic constraints derived from various engineering problems. Its main tools are real quantifier elimination and the simplification of quantifier-free formulas. We illustrate algorithms implemented in SyNRAC, give some examples of how its commands are used, and present its application to design problems in systems and control theory.

We continue the study of a theory which is a valued analogue of the theory of regular rings studied by Carson, Lipshitz and Saracino, characterize it as the model companion of the theory of (extended) Prufer rings, and prove its decidability. We then link it to the theory of p.p. rings developed by Weispfenning and show that it admits quantifier elimination in a related language.

A function f is continuous iff the PRE-image f^{-1}[V] of any open set V is open again. Dual to this topological property, f is called OPEN iff the IMAGE f[U] of any open set U is open again. Several classical Open Mapping Theorems in Analysis provide a variety of sufficient conditions for openness. By the Main Theorem of Recursive Analysis, computable real functions are necessarily continuous. In fact they admit a well-known characterization in terms of the mapping V+->f^{-1}[V] being EFFECTIVE: Given a list of open rational balls exhausting V, a Turing Machine can generate a corresponding list for f^{-1}[V]. Analogously, EFFECTIVE OPENNESS requires the mapping U+->f[U] on open real subsets to be effective. By effectivizing classical Open Mapping Theorems as well as from application of Tarski's Quantifier Elimination, the present work reveals several rich classes of functions to be effectively open., added section on semi-algebraic functions; to appear in Proc. http://cca-net.de/cca2005

The calculation of threshold conditions for models of infectious diseases is of central importance for developing vaccination policies. These models are often coupled systems of ordinary differential equations, in which case the computation of threshold conditions can be reduced to the question of stability of the disease-free equilibrium. This paper shows how computing threshold conditions for such models can be done fully algorithmically using quantifier elimination for real closed fields and related simplification methods for quantifier-free formulas. Using efficient quantifier elimination techniques for special cases that have been developed by Weispfenning and others, we can also compute whether there are ranges of parameters for which sub-threshold endemic equilibria exist.

In this paper a new algorithm for computing the intersection of two rational ruled surfaces, given in parametric/parametric or implicit/parametric form, is presented. This problem can be considered as a quantifier elimination problem over the reals with an additional geometric flavor which is one of the central themes in V. Weispfenning research. After the implicitization of one of the surfaces, the intersection problem is reduced to finding the zero set of a bivariate equation which represents the parameter values of the intersection curve, as a subset of the other surface. The algorithm, which involves both symbolic and numerical computations, determines the topology of the intersection curve as an intermediate step and eliminates extraneous solutions that might arise in the implicitization process.

Term algebras can model recursive data structures which are widely used in programming languages. To verify programs we must be able to reason about these structures. However, as programming languages often involve multiple data domains, in program verification decision procedures for a single theory are usually not applicable. An important class of mixed constraints consists of combinations of data structures with integer constraints on the size of data structures. Such constraints can express memory safety properties such as absence of memory overflow and out-of-bound array access, which are crucial for program correctness. In this paper we extend the theory of term algebras with the length function which maps a term to its size, resulting in a combined theory of term algebras and Presburger arithmetic. This arithmetic extension provides a natural but tight coupling between the two theories, and hence the general purpose combination methods like Nelson-Oppen combination are not applicable. We present decision procedures for quantifier-free theories in structures with an infinite constant domain and with a finite constant domain. We also present a quantifier elimination procedure for the extended first-order theory that can remove a block of existential quantifiers in one step.

We present a version of the Cylindrical Algebraic Decomposition (CAD) algorithm which uses interval sample points in the lifting phase, whenever the results can be validated. This gives substantial time savings by avoiding computations with exact algebraic numbers. We use bounds based on Rouche’s theorem combined with information collected during the projection phase and during construction of the current cell to validate the singularity structure of roots. We compare empirically our implementation of this variant of CAD with implementations of CAD using exact algebraic sample points (our and QEPCAD) and with our implementation of CAD using interval sample points with validation based solely on interval data.

We generalize the work of M. Singer (1978) on the theory of closed ordered differential fields to the case of m-ODF, the theory of ordered fields equipped with m commuting derivations. We give an algebraic axiomatization of the model completion (denoted by m-CODF) of this theory and we can immediately deduce that m-CODF has quantifier elimination in the natural language of ordered Δ-rings. To cite this article: C. Riviere, C. R. Acad. Sci. Paris, Ser. I 343 (2006).

The paper shows elimination of imaginaries for real closed valued fields to suitable sorts. We also show that this result is in some sense optimal. The paper includes a quantifier elimination theorem for real closed valued fields in a language with sorts for the field, value group and residue field.

This paper presents a decision procedure for problems relating polynomial and transcendental functions. The procedure applies to functions that are continuously differentiable with a finite number of points of inflection in a closed convex set. It decides questions of the form 'is f~0?', where [email protected]?{=,>

We propose a decision procedure for algebraically closed fields based on a quantifier elimination method. The procedure is intended to build proofs for systems of polynomial equations and inequations. We describe how this procedure can be carried out in a proof assistant using a Computer Algebra system in a purely skeptical way. We present an implementation in the particular framework of Coq and Maple giving some details regarding the interface between the two tools. This allows us to show that a Computer Algebra system can be used not only to bring additional computational power to a proof assistant but also to enhance the automation of such tools.

In this paper, we present an out of order quantifier elimination algorithm for a class of Quantified Linear Programs (QLPs) called Standard Quantified Linear Programs (SQLPs). QLPs in general and SQLPs in particular are extremely useful constraint logic programming structures that find wide applicability in the modeling of real-time schedulability specifications; see Subramani [Subramani, K., 2005a. A comprehensive framework for specifying clairvoyance, constraints and periodicity in real-time scheduling. The Computer Journal 48 (3), 259–272]. Consequently any algorithmic advance in their solution has a strong practical impact. Prior to this work, the only known approaches to the solution of QLPs involved sequential variable elimination; see Subramani [Subramani, K., 2003b. An analysis of quantified linear programs. In: Calude, C.S. et al. (Eds.), Proceedings of the 4th International Conference on Discrete Mathematics and Theoretical Computer Science. DMTCS. In: Lecture Notes in Computer Science, vol. 2731. Springer-Verlag, pp. 265–277]. In the sequential approach, the innermost quantified variable is eliminated first, followed by the variable which then becomes the innermost quantified variable and so on, until we are left with a single variable from which the satisfiability of the original formula is easily deduced. This approach is applicable in both discrete and continuous domains; however, it is to be noted that the logic demanding the sequential approach requires that the variables are discrete-valued. To the best of our knowledge, the necessity for sequential elimination over continuous-valued variables has not been investigated in the literature. The techniques used in the development of our elimination algorithm may find applications in domains such as classical logic and finite model theory. The final aspect of our research concerns the structure-preserving nature of the algorithm that we introduce here; in general, it is not known whether discrete domains admit such elimination procedures.

Let M be a polynomially bounded, o-minimal structure with archimedean prime model, for example if M is a real closed field. Let C be a convex and unbounded subset of M. We determine the first order theory of the structure M expanded by the set C. We do this also over any given set of parameters from M, which yields a description of all subsets of M^n, definable in the expanded structure., Comment: 16 pages. The paper is a sequel to http://www-nw.uni-regensburg.de/~.trm22116.mathematik.uni-regensburg.de/paper s/cutsa.ps