Mip-0406.dvi

Generalized Constraint Solving over
Differential Algebras
Fakult¨at f¨ur Mathematik und Informatik Abstract
We describe an algorithm for quantifier elimination over differentially closed fields and its implementation within the computer logic package RED- LOG of the computer algebra system REDUCE. We give various application examples, which on the one hand demonstrate the applicability of our soft-ware to non-trivial problems, and on the other hand give a good impressionof the possible range of applications of our work. Essentially, our elimi-nation technique dates back to Seidenberg. It has been made much moreexplicit on the basis of the common axioms for differentially closed fieldsin lectures on differential algebra by Weispfenning. In this explicit form,which we use and describe here, it had remained unpublished so far.
∗dolzmann@uni-passau.de, http://www.fmi.uni-passau.de/˜dolzmann/ †sturm@uni-passau.de, http://www.fmi.uni-passau.de/˜sturm/ Introduction
Since the 1960’s REDUCE has permanently been among the most widely acceptedcomputer algebra systems on the market. From the outset it had mainly focusedon users and applications in physics. Nowadays, with several modern competitorson the market, it is again at the first place this scientific community of physicists,which highly estimates the superior efficiency of the actual REDUCE packagesand, even more important, the highly optimized Portable Standard Lisp compiler.
At the beginning of the 1990’s the authors started to develop within REDUCE their computer logic package REDLOG [DS97a]. Meanwhile the authors belongto the permanent REDUCE development group, and REDLOG is an integral partof the REDUCE distribution. The basic idea of REDLOG is to combine methods ofcomputer algebra on the one hand with symbolic logic on the other hand. REDLOGis a quite comprehensive system including numerous convenient tools for handlingand processing first-order formulas. One central and in fact extremely generalmethod is effective quantifier elimination on the background of temporarily fixedlanguages and theories in the sense of model theory.
In the REDLOG framework, a fixed combination of a language and a theory as mentioned above is called a context. A most prominent example for this isthe language (0, 1, +, −, ·, ≤) of ordered rings in combination with the theory ofreal closed fields. This context was actually the starting point for REDLOG. Thecurrent version of REDLOG comprises implementations of three regular quantifierelimination procedures for the reals, viz. partial cylindrical algebraic decomposi-tion [CH91], virtual substitution methods [Wei88, Wei97, Dol00], and Hermitianquantifier elimination, which is based on parametric real root counting [Wei98].
During the past ten years, REDLOG has been augmented by several other con- texts: algebraically closed fields (complex numbers) [Wei92], discretely valuedfields (p-adic numbers) [Wei88, Stu00, DS99a, DS01], initial Boolean algebras (quantified propositional logic) [SS03], and Presburger Arithmetic (additive the- ory of the integers) [Wei90]. In addition, there are first steps done in incorporatingfree term algebras [SW02].
REDLOG thus covers a comparatively wide range of—mainly commutative— algebra. One rather comprehensive and most fruitful branch of computer algebrahad, however, been passed over so far: differential algebra. The present paper isclosing this gap for the following setup: Basic constraints are ordinary differentialequations and inequalities. From these we obtain systems of constraints by con-structing arbitrary Boolean combinations and in addition admitting universal andexistential quantification. The language is thus (0, 1, +, −, ·, ), where is a unarydifferential operator. The theory is that of differentially closed fields [Rob79a].
Returning to our initial remarks, it is obvious that suitable tools in the area ofdifferential algebra are of high interest in particular to the area of physics, which In Section 2 we are going to illuminate the notion of differentially closed fields, which are unfortunately less natural than algebraically closed fields or realclosed fields. In Section 3 we motivate that our methods are nevertheless highlysuitable for deriving results also about natural differential fields. In Section 4we outline the elimination algorithm. In Section 5, we describe our new RED- LOG context DCFSF, which goes considerably beyond the mere implementation of the elimination procedure. In Section 6 we give various application examples,which on the one hand demonstrate the applicability of our software to non-trivialproblems, and on the other hand give a good impression of the possible range ofapplications of our work. In Section 7 we finally summarize our results.
The Notion of Differentially Closed Fields
Differential algebra dates back to Ritt [Rit50]. Ritt had the initial idea to treat dif-ferential equations to a large extent in a purely algebraic framework and developeda corresponding algebraic framework. As a major result, he proved his differen-tial Nullstellensatz, which is a perfect analogue to Hilbert’s Nullstellensatz foralgebraically closed fields [Hil93].
The first major algorithmic contribution in differential algebra was Seiden- berg’s elimination theory [Sei56]. It provided an elimination theorem with a per-fectly algorithmic proof. We give a formulation of this result from our logicalpoint of view: Theorem 1 (Seidenberg, 1956) Let K be a differential field. Consider for
differential polynomials f1, . . . , f
m, g ∈ K {y1, . . . , yn, u1, . . . , uk ϕ ≡ ∃y1 . . . ∃ynψ, where fi(y1, . . . , yn, u1, . . . , uk) = 0 ∧ g(y1, . . . , yn, u1, . . . , uk) = 0. ϕ and some differential extension field K of K such that we have fij(u1, . . . , uk) = 0 ∧ gj(u1, . . . , uk) = 0 ϕ can be effectively constructed By means of prenex normal form computation, successive elimination of quanti-fier blocks from the inside to the outside, the equivalence between ∀y1 . . . ∀ynψand ¬∃y1 . . . ∃y ¬ ψ, and disjunctive normal form computations, this theorem can be extended to arbitrary first-order input formulas. Note that in the theorem, theextension K of K depends on the input formula ϕ, such that it does not reallyprovide a quantifier elimination procedure for any fixed structure or theory.
On the basis of Seidenberg’s work Robinson introduced in 1959 the notion of a differentially closed field [Rob79a]. He axiomatized the class of differentiallyclosed fields by combining the following sets of axioms: 2. The Leibniz axioms for the derivative.
3. For each existential formula the equivalence between this formula and the corresponding quantifier-free formula obtained according to Seidenberg.
Thus while Seidenberg provided a dynamic process in the sense that equivalenceholds in differential extension fields, Robinson switched from the outset to a suffi-ciently large field such that no such extension is necessary. From a model the-oretic point of view, these differentially closed fields are perfect analogues ofalgebraically closed fields. Unfortunately, there is no natural example for suchfields which could play the role that the complex numbers play for algebraicallyclosed fields. Robinson’s main result was the model completeness of the class ofdifferentially closed fields. It is obvious that Seidenberg’s procedure is an effec-tive quantifier elimination procedure for the class of differentially closed fields.
Consequently, beyond model completeness, differentially closed fields even havethe stronger property of substructure completeness, which is equivalent to the ex-istence of quantifier elimination. Interestingly, Robinson who had just one yearbefore discussed this stronger phenomenon [Rob79b]—without introducing thenotion of substructure completeness, however—did not address this fact at all.
In 1968 Blum reanalyzed Seidenberg’s proof wrt. the assumptions on the dif- ferential extension fields made there [Blu68, Blu77]. By indirect model theoreticmethods, viz. saturated models, she found a natural axiomatization of differen-tially closed fields, in contrast to Robinson’s pragmatic collection of all possibleresults of Seidenberg’s procedure: 3 . For each pair f , g of univariate differential polynomials with ord(f ) > ord(g) there is a c in the field such that f (c) = 0 and g(c) = 0.
Note that this is still an infinite set of axioms. In contrast to Robinson’s, however,these axioms are very natural. In fact, they nicely resemble the axiomatization of algebraically closed fields. At that time the notion of substructure complete-ness had been introduced by Sacks [Sac72], and the scientific community wasabsolutely aware of the fact that differentially closed fields admit quantifier elim-ination via Seidenberg’s procedure.
It is a straightforward idea to come full circle by reformulating Seidenberg’s elimination procedure in such a way that exactly Blum’s axioms become explicitthere. This has actually been done by Weispfenning in 1973. This work has beenincluded in his lectures on differential algebra during the 1980’s but remained un-published in the literature so far. We are going to outline in Section 4 our revisionof the Weispfenning procedure, which we have used for our implementation. Be-fore turning to such technical aspects, we should, however, motivate in Section 3the practical relevance of the method.
The Practical Relevance
of Differentially Closed Fields
We have already mentioned that there is no natural example for a differentiallyclosed field at all. That is, quantifier elimination will certainly never take placein the structures that the users have actually in their minds. It rather takes placein a differentially closed extension field, where there generally exist elements thatcannot be interpreted as functions.
Nevertheless, the quantifier elimination results will for many first-order for- mulations of natural questions provide information also on the differential fieldactually under consideration. At the first place, this applies to input formulas thatare either purely existential or purely universal.
Example 1 (Solvability Conditions for parametric systems) One exam-
ple for a purely existential question is that for the solvability of a parametric sys-
tem of differential equations
ψ ≡ f1(x1, . . . , xn, u1, . . . , um) = 0 ∧ · · · ∧ fk(x1, . . . , xn, u1, . . . , um) = 0, where the f1, . . . , f ∈ Z{ x1, . . . , xn, u1, . . . , um are differential polynomials. We are interested in conditions on the parameters u1, . . . , um for the solvability ofthe system wrt. x1, . . . , xn. A corresponding first-order formulation is given byϕ ≡ ∃x1 . . . ∃xnψ.
For such existential problems, quantifier elimination yields a quantifier-free ϕ such that for any differentially closed field ¯ ϕ is a necessary and sufficient condition in the parameters u1, . . . , um for the solvability of ψ in the differentially closed field ¯ point of view we have in particular that ˆ K |= ∀u1 . . . ∀um(ϕ −→ ˆ ϕ), which can in turn be rewritten as follows: ∀u1 . . . ∀um(ϕ −→ ˆϕ) ⇐⇒ ∀u1 . . . ∀um(∃x1 . . . ∃xn(ψ) −→ ˆϕ) ⇐⇒ ∀u1 . . . ∀u ¬∃ x1 . . . ∃xn(ψ) ∨ ˆ ⇐⇒ ∀u1 . . . ∀u ∀ x1 . . . ∀xn(¬ψ) ∨ ˆ ⇐⇒ ∀u1 . . . ∀u ∀ x1 . . . ∀xn(¬ψ ∨ ˆ ϕ is a necessary condition can be expressed as a universal sentence, and thus holds in all subfields of ¯ Applied to our Example 1, the quantifier elimination result ˆ dition to valid choices possibly identify choices of parameters for which the con-sidered system has no solutions in the field actually under consideration. Never-theless, we secondly expect the case distinctions on the parameters made in ˆ be typical for the input problem rather than for the considered differential field.
They would then provide a certain structural insight into the problem modeled bythe parametric system ψ.
The first point is a fact, which we have proved above. The second point is not mathematically precise and has to be substantiated by empirical data.
Example 2 (Conditions on the solutions of systems) As an example for
a purely universal question consider the differential equation x 2 + x = 0. By
taking the derivative we obtain
0 = (x 2 + x) = 2x x + x = x (2x + 1). It is thus necessary for solutions x that x = 0 or x = −1/2.1 We can ask for suchconditions by means of a universal formula: ψ ≡ x 2 + x = 0 −→ x = a ∨ x = b. As a quantifier-free equivalent our procedure delivers after automatic simplifica-tion ˆ ϕ ≡ a = 0 ∧ 2b + 1 = 0.
ϕ −→ ϕ corresponds to a universal sentence: ∀a∀b( ˆϕ −→ ϕ) ⇐⇒ ∀a∀b( ˆϕ −→ ∀xψ) ⇐⇒ ∀a∀b(¬ ˆϕ ∨ ∀xψ)⇐⇒ ∀a∀b∀x(¬ ˆϕ ∨ ψ). 1This very instructive problem has been suggested by E. Pankratiev at the MEXMAT faculty of Moscow State University during the second author’s stay there.
That is, the quantifier-free condition ˆ ϕ on the parameters is sufficient for ϕ in all K, in particular in the field actually under consideration.
Applying this observation to Example 2 is a bit puzzling at first: We ask for a necessary condition on a = x and b = x for being a solution of the consideredequation x 2 + x = 0. According to the discussion above we may, however, onlyconclude that the obtained result is—in any reasonable differential field—a suffi-cient condition on a = x and b = x for being a necessary condition as requiredin the formulation of the input formula. We see that, in general, it requires a cer-tain intuition about mathematical logic to deal with the results of our procedure.
Here, the situation can be resolved as follows: From ¯ ϕ) a/0, b/ − 1 . That is, K |= ∀x x 2 + x = 0 −→ x = 0 ∨ x = −1 ←→ 0 = 0 ∧ 2 · −1 + 1 = 0 . K |= ∀x x 2 + x = 0 −→ x = 0 ∨ x = −1 , which as a universal The Elimination Algorithm
We want to be able to eliminate quantifiers from an arbitrary first-order formulaover the language (0, 1, +, −, ·, ). In view of our discussion after Theorem 1, itsuffices to consider input formulas of the form f1, . . . , fm, g ∈ Z{y, u1, . . . , uk . Our quantifier elimination algorithm is recursive. After giving some basic definitions, we are first going to discuss five base cases, in which there occurs norecursion. Then we proceed to the actual recursion.
Basic Definitions
Let us consider a differential polynomial f ∈ Z{y, u1, . . . , u } to play the special role of being quantified. We introduce some notions, whichdepend on this variable y, where y is not mentioned explicitly anymore. Theorder ord(f ) of f is the largest s ∈ N such that the s-th derivative y(s) occurs inf . For our next definitions, we consider f of order s as a univariate polynomial in k [y, y(1), . . . , y(s−1) ][y(s) ]. 2This pragmatic treatment for the considered example has been suggested by A. Seidl. In general, it will be interesting to develop a general theory for transferring results for certain typesof input formulas. It is, however, beyond the scope of this paper.
The degree of this univariate polynomial is denoted by deg(f ). Its leading coef-ficient is called the initial I (f ) of f . Its reductum red(f ) is f without the lead-ing monomial. Its partial derivative ∂f /∂y(s) is called the separant S(f ) of f .
Whenever we are going to apply polynomial pseudo-division in our eliminationprocedure, this takes place in this univariate polynomial ring wrt. y(s).
Example 3 Consider f = y y 3+y y +u1y +y +u1. Then we have ord(f ) = 2.
Rewritten as a univariate polynomial, this is
y y 3 + (y + u1 + 1)y + u1. From this we see that deg(f ) = 3, I (f ) = y , red(f ) = (y + u1 + 1)y + u1, andS(f ) = 3y y 2 + (y + u1 + 1).
At some points, however, we take an alternative view of f as a distributive k [y, y(1), . . . , y(s) ]. ¿From that point of view, every polynomial has a representation of the followingform: f = coef(f, t) · t, where terms(f ) is the set of distributive terms in f , and coef(f, t) is the coefficient of a given term t ∈ terms(f ) of f.
Example 4 We resume Example 3, and obtain the multivariate representation
f = y y 3 + y y + (u1 + 1)y + u1, we have terms(f ) = {y y 3, y y , y , 1}, and
coef(f, y y 3) = coef(f, y y ) = 1, coef(f, y ) = u1 + 1, and coef(f, 1) = u1.
Base Cases
Base Case 1
If g = 0, then the elimination result is obviously false.
Base Case 2
If we have m = 0, i.e., there is no equation in our input, then the elimination result is the following disjunction of coefficients stating that g is notthe zero polynomial: Base Case 3
If m = 1 and g ∈ Z\{0}, then the elimination result is the following formula specifying that f is either not constant or the constant zero polynomial: Base Case 4
If m = 1 and g = I (f1) · ˆg and ord( ˆg) < ord(f1), i.e., if we know that I (f1) = 0, then the elimination result is Base Case 5
If m = 1 and g = I (f1) · ˆg and ord( ˆg) = ord(f1), then we proceed as follows: We compute the remainder r of the polynomial pseudo-division ofI (f1)de · ˆgd by f where d = deg(f1) and e = deg( ˆg). Our elimination result issimilar to the previous case with r instead of ˆ Recursion
deg(fi) for i ∈ {1, . . . , m}. Then we can assume wlog. that (s1, d1) ≥ · · · ≥ (sm, dm) wrt. the lexicographic order on N2.
Recursion Case 1
If deg(fm) = 0, i.e., if y does not occur in fm, then we This yields a quantifier-free equivalent ˆ ϕ. The overall elimination result is then Recursion Case 2
In view of Recursion Case 1, we can assume that y occurs in fm. In a first step we construct a case distinction on the initial of fm being zero ornot. That is, we replace our considered formula 0 ∧ red(fm) = 0 ∧ I (fm) = 0 ∧ g = 0 , 0 ∧ I (fm) · g = 0 . For ϕ1 we can by recursion obtain a quantifier-free equivalent ˆ ϕ2 we are going to distinguish cases once more. The final Recursion Subcase 2.1
If m = 1 and ord(g) ≤ ord(f1), then we proceed as described in the base cases 3–5 discussed above.
Recursion Subcase 2.2
Assume m = 1 and ord(g) > ord(f1). We start by computing the remainder r of the polynomial pseudo-division ϕ2 can be recursively computed from ∃x f1 = 0 ∧ I(f1) · r = 0 . Otherwise we perform another polynomial pseudo-division computing the re-mainder f of the division f1 : S(f1)(s1−ˆs), ˆs = ord S(f1) . ϕ2 is then obtained by recursively applying our pro- cedure to the two constituents of the following case distinction on the possiblevanishing of S(f1): ∃y f1 = 0 ∧ S(f1) · I(f1) · r = 0 ∨ ∃y S(f1) = 0 ∧ f = 0 ∧ I(f1) · r = 0 . Recursion Subcase 2.3
Assume m > 1. We compute the remainder r of the ϕ2 is then computed by recursively applying our 0 ∧ r = 0 ∧ I (fm) · g = 0 . Implementation
The procedure described in the previous section has been implemented in RED- LOG, which stands for “REDUCE logic” system [DS97a]. It provides an extension of the computer algebra system REDUCE to a computer logic system implement-ing symbolic algorithms on first-order formulas wrt. temporarily fixed first-orderlanguages and theories. Such a choice of language and theory is called a context.
So far, the following REDLOG contexts had been available: OFSF (Ordered fields, standard form representation of terms). The class of real
closed fields such as the real numbers with ordering. This context was theoriginal motivation for REDLOG. It is still the most important and mostcomprehensive one.
ACFSF (Algebraically closed fields, standard form representation of terms). The
class of algebraically closed fields such as the complex numbers over thelanguage of rings.
PASF (Presburger Arithmetic, standard form representation of terms). The theory
of the integers with addition, additive inverses, and congruences wrt. fixedmoduli.
DVFSF (Discretely valued fields, standard form representation of terms). The
most prominent example for discretely valued fields are p-adic numbers forsome prime p with abstract divisibility relations encoding order betweenvalues. All DVFSF algorithms are optionally uniform in p.
IBALP (Initial Boolean algebras, Lisp prefix representation of terms). The class
of Boolean algebras with two elements. These algebras are uniquely de-termined up to isomorphisms. IBALP comprises quantified propositionalcalculus.
The work discussed here establishes another such context DCFSF: DCFSF (Differentially closed fields, standard form representation of terms). Our
context for dealing with differentially closed fields. There is no natural ex-ample for such a field. As shown in this paper one can, however, still obtainrelevant and interpretable results also for reasonable differential fields.
The idea of REDLOG is to combine methods from computer algebra with first- order logic thus extending the computer algebra system REDUCE to a computerlogic system. In this extended system both the algebraic side and the logic sidegreatly benefit from each other in numerous ways. The current version RED- LOG 3.0 including our work described here is an integral part of the computer algebra system REDUCE 3.8. We give a short overview of the REDLOG function-ality currently available for DCFSF. Details can be found in the REDLOG usermanual [DS99b].
We are going to describe how to bring up the system, and how to input formu- las. Then we discuss the available functions by category: Functions for simplify-ing formulas, normal form computations, and utility functions. Finally we turn tothe quantifier elimination rlqe, which is the main subject of this paper.
Getting started
After invoking REDUCE, the following commands load REDLOG into memory andswitch to the context DCFSF: Always use either ; or $ to terminate commands. The latter suppresses the output.
We explain by example the format of DCFSF formulas. The formula 1 = a −→ y3 = 3c phi := ex({a,y1},y1 d 1 = (a * b) d 1 equiv all(y2,5 * y2 d 1 ** 2 + y1 <> a impl y3 = 3 * c d 3 or not(y1 d 1 = a and b = 0))); Note that all left hand sides are immediately subtracted to the corresponding righthand sides, and the summands of the differential polynomials are canonically or-dered there. For the sake of convenience, we are going to switch to mathematicalnotation for our explanation of the available functions in the subsequent sections.
The following are the available binary infix operators with decreasing precedence:d, **, *, +, -, and, or, impl, repl, equiv. There is a synonym ˆ for **,and * between numbers and variables may be omitted.
Lists are comma-separated and enclosed in braces. When functions have only one argument, parentheses may be omitted. For finally terminating a REDUCEsession, use quit: Simplification
The techniques used for simplification have been described for real closed fieldsin [DS97b]. We have adapted them to differentially closed fields for our imple-mentation: rlsimpl formula Simplification. The applied simplifications are Boolean sim-
plification rules at the first place plus some few algebraic ones. Quantifierelimination results and output of the other simplifiers discussed below are always simplified wrt. rlsimpl. It is thus not interesting to explicitly callrlsimpl on these.
Example: rlsimpl(a = 0 ∧ (b = 0 ∨ (c = 0 ∧ (e = 0 ∨ a = 0)))) a = 0 ∧ (b = 0 ∨ c = 0). rlgsn quantifier-free-formula Gr¨obner simplification. Applies a rather so-
phisticated simplification, which detects algebraic dependencies by means
of Gr ¨obner basis techniques. For this either a conjunctive or disjunctive
normal form has to be computed at the beginning. The result is in the cor-
responding normal form as well. The choice between the conjunctive and
the disjunctive variant is made automatically using some heuristics to pre-
dict the smaller choice. Use the calls rlgsc or rlgsd to force the use of
conjunctive normal form or disjunctive normal form, respectively.
Example: rlgsn(xy + 1 = 0 ∨ yz + 1 = 0 ∨ x − z = 0) rlitab formula Iterative automatic tableau simplification.
distinctions wrt. the vanishing of terms contained in formula. The idea is
that the simplification results for both branches together are smaller than
the original formula. All terms in formula are successively tried; the one
leading to the smallest output is chosen provided that this output is actually
smaller than the size of the original formula. This process is iterated on the
result until there is no further improvement. The call rlatab performs
only one tableau step without the iteration loop on the results.
Example: rlitab((a = 0 ∨ b = 0) ∧ ((a = 0 ∧ b = 0) ∨ (a = 0 ∧ c = 0))) a = 0 ∧ b = 0 ∧ c = 0. In this example there is one tableau step wrt. a = 0 vs. a = 0 performed.
Normal Form Computations
Normal form computations result in formulas that are equivalent to the input buthave a particular Boolean structure: rldnf quantifier-free-formula Disjunctive normal form. During the computa-
tion we apply simplification techniques extending the ideas of Quine andMcCluskey for propositional calculus [Qui52, Qui55, Qui59, McC56] toour algebraic situation.
Example: rldnf(x − a = 0 ←→ x − b = 0) (a − x = 0 ∧ b − x = 0) ∨ (a − x = 0 ∧ b − x = 0). rlcnf quantifier-free-formula Conjunctive normal form. During the compu-
tation we apply simplification techniques extending the ideas of Quine andMcCluskey for propositional calculus [Qui52, Qui55, Qui59, McC56] toour algebraic situation.
Example: rlcnf(x − a = 0 ←→ x − b = 0) (a − x = 0 ∨ b − x = 0) ∧ (a − x = 0 ∨ b − x = 0). rlnnf formula Negation normal form. A negation normal form of formula is
an equivalent formula that contains only ∧ and ∨ as Boolean operators. Inparticular there is no explicit logical negation ¬. Instead, all negation isexpressed by means of the relations = and =.
Example: rlnnf(∃x(x − a = 0) ←→ ∀x(¬(x − b = 0))) (∃x(−a + x = 0) ∧ ∀x(−b + x = 0)) ∨ (∀x(−a + x = 0) ∧ ∃x(−b + x = 0)). rlpnf formula Prenex normal form. A prenex normal form of formula is an
equivalent formula that consists of one prenex quantifier block followedby a quantifier-free formula. rlpnf minimizes the number of quantifierchanges in the prenex block. Prenex normal forms are used within the quan-tifier elimination procedure, where the prenex quantifiers are successivelyeliminated from the inside to the outside.
Example: rlpnf(∃x(x − a = 0) ←→ ∀x(¬x − b = 0)) ∀x1∀x2∃x0∃x3((−a+x0 = 0∧−b+x1 = 0) ∨ (−a+x2 = 0∧−b+x3 = 0)). Utilities
The utility functions allow to comfortably construct, manipulate, and access for-mulas or parts of formulas: rlmatrix prenex-formula Matrix. That is the quantifier-free part following
Example: rlmatrix(∀a∃x(ax + b = 0 ∨ c = 0)) ax + b = 0 ∨ c = 0. rlall formula [varlist] Universal closure. Binds all free variables of formula
that are not in the optional varlist with a prenex universal quantifier.
Example: rlall(∀a∃x(ax + b = 0) ∨ c f = 0, {f}) ∀b∀c∀a∃x(ax + b = 0 ∨ c f = 0). rlex formula [varlist] Existential closure. Binds all free variables of formula
that are not in the optional varlist with a prenex existential quantifier.
Example: rlex(∀a∃x(ax + b = 0) ∨ c f = 0) ∃b∃c∃f∀a∃x(ax + b = 0 ∨ c f = 0). rlstruct formula Structure. Returns a pair where the first entry is a formula,
and the second entry is a list of equations. The first entry is the formula witheach left hand side polynomial replaced by a symbolic name v1, v2, . . . Thesecond entry is the corresponding binding for these symbolic names. Oneidea is that the first entry can be used to get an impression of the logicalstructure of formulas when there are very large terms.
Example: rlstruct(x − 5 = 0 ∨∀x(xx − 13x − 5x + 65 = 0 ∧ x − 5 = 0)) {v2 = 0 ∨ ∀x(v1 = 0 ∧ v2 = 0), {v1 = xx − 13x − 5x + 65, v2 = x − 5}}. rlifstruct formula Irreducible factor structure. Returns a pair where the
first entry is a formula, and the second entry is a list of equations. Thefirst entry is the formula with each irreducible factor in the left hand sidepolynomials replaced by a symbolic name v1, v2, . . . The second entry is thecorresponding binding for these symbolic names. One idea is that the firstentry can be used to get an impression of the logical structure of formulaswhen there are very large terms.
Example: rlifstruct(x−5 = 0∨∀x(xx −13x−5x +65 = 0∧x−5 = 0)) {v2 = 0 ∨ ∀x(v1v2 = 0 ∧ v2 = 0), {v1 = x − 13, v2 = x − 5}}. rlatl formula Atomic formula list. A list of all atomic formulas (equations
and inequalities) contained in formula, ignoring multiplicities.
Example: rlatl(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) {ax = 0, a = 0, a = 0}. rlatml formula Atomic formula multiplicity list. A list of pairs containing all
atomic formulas (equations and inequalities) contained in formula togetherwith the number of their occurrences.
Example: rlatml(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) {{ax = 0, 1}, {a = 0, 2}, {a = 0, 1}}. rlterml formula Term list. A list of all terms (left hand side polynomials)
contained in formula, ignoring multiplicities.
Example: rlterml(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) rltermml formula Term multiplicity list. A list of pairs containing all terms
(left hand side polynomials) contained in formula together with the number Example: rltermml(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) {{ax, 1}, {a, 3}}. rlifacl formula Irreducible factor list. A list of all irreducible factors of all
left hand side polynomials contained in formula, ignoring multiplicities.
Example: rlifacl(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) rlifacml formula Irreducible factor multiplicity list. A list of pairs containing
all irreducible factors of all left hand side polynomials contained in formulatogether with the number of their occurrences.
Example: rlifacml(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) {{a, 4}, {x, 1}}. rlfvarl formula Free variable list. The list of all variables that occur at some
place in formula where they are not bound by any quantifier.
Example: rlfvarl(∃x(y = 0 ∨ ∀y(x − y + a = 0))) rlbvarl formula Bound variable list. The list of all variables that occur at
some place in formula where they are bound by some quantifier.
Example: rlbvarl(∃x(y = 0 ∨ ∀y(x − y + a = 0))) rlvarl formula Variable list. A pair combining the results of both rlfvarl
(1st entry) and rlbvarl (2nd entry).
Example: rlvarl(∃x(y = 0 ∨ ∀y(x − y + a = 0))) {{a, y}, {x, y}}. rlatnum formula Atomic formula number. The number of atomic formulas
(equations and inequalities) contained in formula, counting multiplicities.
This is a good measure for the size of a formula.
Example: rlatnum(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) rlqnum formula Quantifier number. The number of quantifiers (∃x and ∀x)
contained in formula, counting multiplicities.
Example: rlqnum(∃x(a = 0 ∧ ∀y((ax = 0 ∧ a = 0) ∨ a = 0))) sub equationlist formula Substitution. Semantically correctly substitutes terms
for variables. Afterwards the result is brought into the usual canonical dis-tributive form. As can be seen in the example below, substitution for severalvariables is done in parallel in contrast to sequentially. Note also the propertreatment and necessary renaming of bound variables.
Example: sub({x = 2xy, y = x}, x = 0 ∨ y = 0 ∨ ∃y(x = 0 ∨ y = 0)) 2x y + 2y x = 0 ∨ x = 0 ∨ ∃y0(2xy = 0 ∨ y0 = 0). for . . . mkand Make and. Loop for the systematic construction of conjunctions.
Example: for each x in {a,b,c d 1} mkand x=0 true ∧ a = 0 ∧ b = 0 ∧ c = 0. for . . . mkor Make or. Loop for the systematic construction of disjunctions.
Example: for i:=1:3 mkor mkid(x,i) d (i - 1) = 0 false ∨ x1 = 0 ∨ x = 0 ∨ x = 0. Quantifier Elimination
The elimination algorithm described in the previous section has been implementedin the REDLOG function rlqe. This function has two arguments; the second oneis optional: The first one is the formula to eliminate quantifiers from; the sec-ond one specifies an external theory. Such external theories, which have beenintroduced in [DS97b], are a general concept present in REDLOG. Formally, anexternal theory is a list of atomic formulas considered as a conjunction. All elim-ination results are equivalent to the input formula for parameter values satisfyingthe external theory. In other words, if ˆ ϕ is the result of eliminating ϕ wrt. the external theory ϑ in K , then we have Note that if ϑ is empty, which is the default value, then In the case of rlqe in DCFSF, such theories ϑ are exploited as follows: When- ever during the elimination procedure the derivation operator is applied to somey(n) a check is performed whether there is an equation y(n+1) = t contained in ϑ,where t is any differential polynomial. In the positive case, t is used instead ofy(n+1). This allows in particular to specify via a = 0 that a is a constant, andvia t = 1 that t is essentially the independent variable. Our examples in thenext section are going to demonstrate that this can greatly support the eliminationprocedure.
rlqe formula [theory] Quantifier Elimination. The optional argument theory
is a list of equations and inequalities. Returns quantifier-free equivalent (wrt. theory, if present) of formula.
Example: rlqe(∃x(x = a ∧ x = b), {a = 0}) Application Examples
All our computations have been carried out on a 2 GHz Intel Pentium 4 using128 MB of RAM.
Example 5 (Example 2 revisited) We start by revisiting Example 2. For the
input formula
ϕ ≡ ∀x x 2 + x = 0 −→ x = a ∨ x = b , we obtain the quantifier-free equivalent ˆ ϕ ≡ a = 0 ∧ 2b + 1 = 0 discussed there in Example 6 (A Benchmark Sequence) In the previous Example 5, we have
seen that it is necessary for the solvability of x 2 + x = 0 that x = 0 or x = −1/2.
In either case, it follows for the solutions that x(s) = 0 for s > 2. This motivates
the following sequence of benchmark examples
x x 2 + x = 0 ∧ x(s) = 0 for increasing s ∈ N. The following table collects the obtained quantifier-freeequivalents ˆ ϕs and the computation times of our procedure applied to ϕs for some time (ms) < 10 < 10 < 10 < 10 For s = 37 our implementation exceeds the available memory of 128 MB.
Example 7 (Inhomogeneous System with Polynomial Coefficients)
This example has been adapted from Example 7.2 in [AW04]. The following
system is discussed there:
It is furthermore specified that r is a constant and t is the independent variable,i.e. r = 0 and t = 1. Note that the coefficient matrix A is thus polynomial.
We are interested in deriving conditions on the parameters r and t for the solvability of the system wrt. y. We introduce a new indeterminate a for modelingthe trigonometric functions: a := sin(t2), and it follows that a = 2t cos(t2).
Substitution yields For constructing our input formulas, we formulate the system as a quantifier-freeformula: We formulate the conditions on r and t as an external theory ϑ = {r = 0, t = 1},which we use for all our computations. For ∃y1∃y2(ψ ∧ y1 = 0 ∧ y2 = 0) we obtain “true” wrt. ϑ in less than 10 ms. A more interesting result is obtainedfor ∃y1∃y2(ψ ∧ y1 = 0 ∧ y2 = 0 ∧ y = 2ty This yields after 50 ms the following quantifier-free equivalent wrt. ϑ: t = 0 ∨ (a t − a + 4at3 = 0 ∧ a = 0 ∧ a = 0 ∧ r = 0). Note that t = 0 is “false” wrt. ϑ; here the simplifier requires some improvement. Itis well-known that the most general solution for the equations in ψ is of the form y1 = C1 sin(t2) + C2 cos(t2) + r sin(t2), y2 = C1 cos(t2) − C2 sin(t2). The implicit condition y = 2ty 1 has thus indeed the consequence r = 0. More- over, the fundamental equation a t − a + 4at3 = 0 is a homogeneous differentialequation for a = sin(t2). Accordingly, resubstituting sin(t2) for our artificial pa-rameter a yields t = 0 ∨ 2t cos(t2) = 0 ∧ sin(t2) = 0 ∧ r = 0 . For comparison of efficiency we finally give result and timing for the same elimination without specifying the external theory ϑ. We then we obtain t = 0 ∨ (a rt − a t r − r at + r t a + 4art3 = 0 ∧ a r − r a = 0 ∧ a = 0 ∧ r = 0), Example 8 (Equilibrium Points of an Electric Circuit) This example has
been taken from [IT03]. The following system ϕ describes a certain nonlinear
electric circuit:
f1(v6) = 9u2g 1 1v6 − 6u1g1v2 2 2v4 − 6u2g2v2 f3(v3) = 9u2g 3 3v3 − 6u3g3v2 4 4v5 − 6u4g4v2 Capital letters indicate parameters: C1, . . . , C4 are constant capacities, L0 and L1 are constant inductances, and I0, I01, I02 are constant current sources. Thepolynomials ˜ f4 are cubic Lagrange polynomials interpolating the non- linear voltage-current characteristics f1, . . . , f4 of corresponding resistors. Fori ∈ {1, . . . , 4}, u i denotes the first extremum of fi, and gi In the original work [IT03], the left hand sides of the equations, which contain the derivation operator are set to zero in order to determine the equilibrium pointsof the circuit. This is, however, a purely algebraic problem then.
In order to get an impression of the current limits of our implementation, we instead try to eliminate as many currents and voltages from the original system inorder to derive necessary relations between the parametric quantities. We are ableto eliminate the currents i1 and i2 and the voltage v3 wrt. the theory ϑ = {C = 0, . . . , C = 0, L = 0, L = 0, I = 0, I = 0, I = 0}. For ∃i1∃i2∃v3ϕ and ϑ, we obtain within 80 ms 2g4u4v5 − 6u4 2g4v2 4L2 + 9v5 2g4u24 2g4u4v5 + 3v5 2g4v25 2 + v5 4 − v6 1 − I02 − 9g1u21 6 + 6g1u1v26 where χ is a huge irreducible differential polynomial with 1441 monomials in itsdistributive representation. The elimination of more variables exceeds our mem-ory of 128 MB. Without specifying ϑ the elimination above takes 160 ms. Theresult then also consists of three equations. The first two of these equations areonly slightly more complicated than the displayed ones, while the polynomialcorresponding to χ grows to 2543 monomials.
Conclusions
We have described a quantifier elimination procedure for differentially closedfields. For this purpose, we have carefully motivated and introduced the notionof a differentially closed field. We furthermore have motivated that although thesestructures are not at all natural, results obtained there are in general of high rel-evance for natural differential fields. Our method is an optimized version of avariant of Seidenberg’s famous elimination method. It is implemented in the logicpackage REDLOG of the computer algebra system REDUCE. This implementation goes far beyond only providing quantifier elimination. Instead it provides a richexperimentation and implementation environment for logic algorithms in differ-ential fields and many other algebraic structures. We have finally demonstratedthe applicability of our implementation to non-trivial problems taken from thecontemporary scientific literature on computer algebra.
Acknowledgment
This work has been supported by numerous fruitful discussions with E. Pankratievat Moscow State University and with A. Seidl and V. Weispfenning. In addition,we wish to point out once more that our version of Seidenberg’s elimination inSection 4 is based on notes of lectures on differential algebra by V. Weispfenning.
References
Hirokazu Anai and Volker Weispfenning. Reach set computations us-ing real quantifier elimination. Technical Report MIP-0012, FMI, Uni-versit¨at Passau, D-94030 Passau, Germany, October 2004.
Lenore Blum. Generalized Algebraic Structures: A Model TheoreticalApproach. Ph.D. thesis, MIT, Cambridge, MA, 1968.
Lenore Blum. Differentially closed fields: A model theoretic tour. InH. Bass, P. J. Cassidy, and J. Kovacic, editors, Contributions to Alge-bra. A Collection of Papers Dedicated to Ellis Kolchin, pages 37–61.
Academic Press, New York, 1977.
George E. Collins and Hoon Hong. Partial cylindrical algebraic decom-position for quantifier elimination. Journal of Symbolic Computation,12(3):299–328, September 1991.
Andreas Dolzmann. Algorithmic Strategies for Applicable Real Quan-tifier Elimination. Doctoral dissertation, Department of Mathematicsand Computer Science. University of Passau, Germany, D-94030 Pas-sau, Germany, March 2000.
Andreas Dolzmann and Thomas Sturm. Redlog: Computer algebrameets computer logic. ACM SIGSAM Bulletin, 31(2):2–9, June 1997.
[DS97b] Andreas Dolzmann and Thomas Sturm. Simplification of quantifier- free formulae over ordered fields. Journal of Symbolic Computation,24(2):209–231, August 1997.
Andreas Dolzmann and Thomas Sturm. P-adic constraint solving. InSam Dooley, editor, Proceedings of the 1999 International Symposiumon Symbolic and Algebraic Computation (ISSAC 99), Vancouver, BC,pages 151–158. ACM Press, New York, NY, July 1999.
[DS99b] Andreas Dolzmann and Thomas Sturm. Redlog user manual. Techni- cal Report MIP-9905, FMI, Universit¨at Passau, D-94030 Passau, Ger-many, April 1999. Edition 2.0 for Version 2.0.
Andreas Dolzmann and Thomas Sturm. Parametric systems of linearcongruences. In V. G. Ganzha, E. W. Mayr, and E. V. Vorozhtsov,editors, Computer Algebra in Scientific Computing. Proceedings of theCASC 2000, pages 149–166. Springer, Berlin, 2001. To appear.
Uber die vollen Invarianzsysteme. Mathematische An- Valentin Irtegov and Tatyana Titorenko. On modeling the qualitativeinvestigation of nonlinear systems with the aid of computer algebra.
In Victor G. Ganzha, Ernst W. Mayr, and E. V. Vorozhtsov, editors,Computer Algebra in Scientific Computing. Proceedings of the CASC2003, pages 199–212. TUM M¨unchen, 2003.
[McC56] E. J. McCluskey. Minimization of Boolean functions. Bell Systems Technical Journal, 35:1417–1444, April 1956.
Willard Van Orman Quine. The problem of simplifying truth functions.
American Mathematical Monthly, 59:521–531, November 1952.
Willard Van Orman Quine. A way to simplify truth functions. Ameri-can Mathematical Monthly, 62:627–631, November 1955.
Willard Van Orman Quine. On cores and prime implicants of truthfunctions. American Mathematical Monthly, 66:755–760, November1959.
Joseph F. Ritt. Differential Algebra, volume 33 of AMS ColloquiumPublications. American Mathematical Society, New York, NY, 1950.
[Rob79a] Abraham Robinson. On the concept of a differentially closed field. In H. J. Kreisler, S. K¨orner, W. A. Luxemburg, and A. D. Young, editors,Abraham Robinson. Selected Papers, volume 1, pages 440–455. YaleUniversity Press, New Haven and London, 1979. Originally in Bull.
Res. Council Israel 8F (1959), 113–128. M.R. 23 #2323.
[Rob79b] Abraham Robinson. Relative model-completeness and the elimination of quantifiers. In H. J. Kreisler, S. K ¨orner, W. A. Luxemburg, andA. D. Young, editors, Abraham Robinson. Selected Papers, volume 1,pages 146–159. Yale University Press, New Haven and London, 1979.
Originally in Dialectica 12 (1958) 394–407. M.R. 21 #1265.
Gerald E. Sacks. Saturated Model Theory. Mathematics Lecture NoteSeries. W. A. Benjamin, Inc., Reading, MA, 1972.
An elimination theory for differential alge- bra. University of California Publications in Mathematics. New Series,3:31–66, 1956.
Andreas Seidl and Thomas Sturm. A generic projection operator forpartial cylindrical algebraic decomposition. In Rafael Sendra, editor,Proceedings of the 2003 International Symposium on Symbolic and Al-gebraic Computation (ISSAC 03), Philadelphia, Pennsylvania, pages240–247. ACM Press, New York, NY, 2003.
Thomas Sturm. Linear problems in valued fields. Journal of SymbolicComputation, 30(2):207–219, August 2000.
Thomas Sturm and Volker Weispfenning. Quantifier elimination interm algebras. The case of finite languages.
Ernst W. Mayr, and E. V. Vorozhtsov, editors, Computer Algebra inScientific Computing. Proceedings of the CASC 2002, pages 285–300.
TUM M¨unchen, 2002.
Volker Weispfenning. The complexity of linear problems in fields.
Journal of Symbolic Computation, 5(1&2):3–27, February–April1988.
Volker Weispfenning. The complexity of almost linear diophantineproblems. Journal of Symbolic Computation, 10(5):395–403, Novem-ber 1990.
Volker Weispfenning. Comprehensive Gr ¨obner bases. Journal of Sym-bolic Computation, 14:1–29, July 1992.
Quantifier elimination for real algebra—the quadratic case and beyond. Applicable Algebra in Engineering Com-munication and Computing, 8(2):85–101, February 1997.
Volker Weispfenning. A new approach to quantifier elimination for realalgebra. In B.F. Caviness and J.R. Johnson, editors, Quantifier Elimina-tion and Cylindrical Algebraic Decomposition, Texts and Monographsin Symbolic Computation, pages 376–392. Springer, Wien, New York,1998.

Source: http://andreas.dolzmann.de/publications/MIP-0406.pdf