When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.

In this paper we categorize the types and prevalence of psychological factors that were present in ICTD interventions described in the ICTD2012 proceedings. With an eye towards recommendations for better understanding and addressing these dynamics, we then interpret and discuss these findings. We conclude that psychological dynamics on an individual level of analysis are either more prominent or tend to be identified more often by ICTD practitioners/researchers than dynamics on dyad/team and organizational levels. In addition, instances where psychological dynamics impede the success of ICTD interventions feature more prominently than dynamics which facilitate the success of those interventions. We argue for a greater appreciation and enhancement of positive psychological dynamics on higher levels of analysis through a more robust application of theory relating to organizational behavior.

This article makes the key observation that when using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is not always the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This motivates our definition of a Truth Table Invariant CAD (TTICAD). We generalise the theory of equational constraints to design an algorithm which will efficiently construct a TTICAD for a wide class of problems, producing stronger results than when using equational constraints alone. The algorithm is implemented fully in Maple and we present promising results from experimentation.

Let V ⊂ Rr denote the real algebraic variety defined by the conjunction f = 0 ∧ g = 0, where f and g are real polynomials in the variables x1, ..., xr and let S be a submanifold of Rr-2. This paper proposes the notion of the analytic delineability of V on S with respect to the last 2 variables. It is suggested that such a notion could be useful in solving more efficiently certain quantifier elimination problems which contain the conjunction f = 0 ⊂ g = 0 as subformula, using a variation of the CAD-based method. Two bi-equational lifting theorems are proved which provide the basis for such a method.

This paper presents a decision procedure for a certain class of sentences of first order logic involving integral polynomials and the exponential function in which the variables range over the real numbers. The inputs to the decision procedure are prenex sentences in which only the outermost quantified variable can occur in the exponential function. The decision procedure has been implemented in the computer logic system REDLOG. Closely related work is reported in [2, 7, 16, 20, 24].

This paper introduces an improved method for constructing cylindrical algebraic decompositions (CADs) for formulas with two polynomial equations as implied constraints. The fundamental idea is that neither of the varieties of the two polynomials is actually represented by the CAD the method produces, only the variety defined by their common zeros is represented. This allows for a substantially smaller projection factor set, and for a CAD with many fewer cells.In the current theory of CADs, the fundamental object is to decompose n-space into regions in which a polynomial equation is either identically true or identically false. With many polynomials, one seeks a decomposition into regions in which each polynomial equation is identically true or false independently. The results presented here are intended to be the first step in establishing a theory of CADs in which systems of equations are fundamental objects, so that given a system we seek a decomposition into regions in which the system is identically true or false --- which means each equation is no longer considered independently. Quantifier elimination problems of this form (systems of equations with side conditions) are quite common, and this approach has the potential to bring large problems of this type into the scope of what can be solved in practice. The special case of formulas containing two polynomial equations as constraints is an important one, but this work is also intended to be extended in the future to the more general case.

The improved projection operation for cylindrical algebraic decomposition (CAD) described in [10] requires for its validity the crucial concept of order-invariance. A real polynomial f(x1, ..., xr) is said to be order-invariant in a subset c of Rr if the order (of vanishing) of f at the point p is constant as p varies throughout c. The application of the improved projection which is perhaps simplest conceptually is in the construction of a CAD for a set of polynomials which is well-oriented in a certain sense. Given a well-oriented set A of r-variate integral polynomials algorithm CADW [10] uses the improved projection to construct a CAD of Rr which is order-invariant for each polynomial in A. A drawback of CADW is that it halts in failure, reporting that A is not well-oriented, when presented with a non-well-oriented set A as input. Such failure of CADW is potentially serious, because it forces the user to fall back on less efficient projection operators (such as the Collins-Hong projection) for CAD. The present paper describes an efficient method for avoiding the failure of CADW in certain special non-well-oriented cases. The method is based upon a sufficient criterion for the order of a polynomial h(x1, ..., xr) of the special form h = a(x1, ..., xr-1)xrk + b(x1, ldots, xr-1) (which we shall call a binomial in xr) to be 1 throughout the entire cylinder over a nullifying point p in Rr-1 for h (that is, a point p for which h(p, xr) = 0 identically). Following a review of CADW, the sufficient criterion referred to is motivated and proved. The algorithmic application of the criterion is carefully described and validated, and an example discussed.

Collins [4] observed that quantifier elimination problems often have equational constraints, and he asserted that such constraints can be used to reduce the projection sets required for cylindrical algebraic decomposition (cad) based quantifier elimination. This paper follows on from [11], and validates the use of a semi-restricted equational projection scheme throughout the projection phase of cad. The fully restricted projection scheme as originally proposed in [4] is proved valid for four variable problems under certain conditions.

We consider the problem of determining the consistency over the real number of a system of integral polynomial strict inequalities. This problem has applications in geometric modelling. The cylindrical algebraic decomposition (cad) algorithm [2] can be used to solve this problem, though not very efficiently. In this paper we present a less powerful version of the cad algorithm which can be used to solve the consistency problem for conjunctions of strict inequalities, and which runs considerably faster than the original method applied to this problem. In the case that a given conjunction of strict inequalities is consistent, the modified cad algorithm constructs solution points with rational coordinates.

Given a set of r-variate integral polynomials, a cylindrical algebraic decomposition (cad) of euclidean r-space $E^r $ partitions $E^r $ into connected subsets compatible with the zeros of the polynomials. Each subset is a cell Collins gave a cad construction algorithm in 1975, as part of a quantifier elimination procedure for real closed fields. The cad algorithm has found diverse applications (optimization, curve display); new applications have been proposed (term rewriting systems, motion planning). In the present two-part paper, we give an algorithm which determines the pairs of adjacent cells as it constructs a cad of $E^2 $. Such information is often useful in applications. In Part I we describe the essential features of the r-space cad algorithm, to provide a framework for the adjacency algorithm in Part II.

Given a set of r-variate integral polynomials, a cylindrical algebraic decomposition (cad) of euclidean r-space $E^r $ partitions $E^r $ into connected subsets compatible with the zeros of the polynomials. Each subset is a cell. Informally, two cells of a cad are adjacent if they touch each other; formally, they are adjacent if their union is connected. In applications of cad’s one often wishes to know the adjacent pairs of cells. Previous algorithms for cad construction (such as that given in Part I of this paper) have not actually determined them. We give here in Part II an algorithm which determines the pairs of adjacent cells as it constructs a cad of $E^2 $.