<< TEACHING - VERONA/BONACINA 2014 - Decision Procedures for Nonlinear Arithmetic - Grant Passmore

# Literature

• Background on Ideals and Varieties - Sec 2.1.1 of my PhD thesis (pdf)
• Background on ACF - Sec 2.1.2 of my PhD thesis (pdf)
• Background on Groebner Bases - Sec 2.3 of my PhD thesis (pdf)

# Code

• Algebra: Multivariate commutative algebra over Q[x_1, ..., x_n] - (view)
• Groebner: Construction of Groebner Bases via Buchberger's Algorithm - (view)
• Sturm: Sturm Chains and Real Root Isolation - (view)
• Resultant: Bivariate Resultants via a Modular Euclidean Method - (view)
• RealAlg: Arithmetic in the Field of Real Algebraic Numbers - (view)

Install compiler:

Run, Experiment and Play!

• An example with Groebner bases:

``````\$ poly

Poly/ML 5.5.1 Release
> use "top.sml"; (* Load libraries and open namespaces *)
> val f_1 = [((Rat.rat_of_int 2), [(1, 1)]), (Rat.one, [(0, 1)]), (Rat.one, [])] : poly;
val f_1 =
[(Rat (true, 2, 1), [(1, 1)]), (Rat (true, 1, 1), [(0, 1)]),
(Rat (true, 1, 1), [])]: poly
> p_toString f_1;
val it = "2 x1 + x0 + 1": string
> val f = [(Rat.one, [(1, 2), (0, 1)]), ((Rat.rat_of_int 4), [(1, 1), (0, 1)]),
((Rat.rat_of_int ~3), [(0, 2)])] : poly;
val f =
[(Rat (true, 1, 1), [(1, 2), (0, 1)]),
(Rat (true, 4, 1), [(1, 1), (0, 1)]), (Rat (false, 3, 1), [(0, 2)])]:
poly
> p_toString f;
val it = "x1^2 x0 + 4 x1 x0 + -3 x0^2": string
> p_toString (case p_div f [f_1] of (_, r) => r);
val it = "1/4 x0^3 + -9/2 x0^2 + -7/4 x0": string
> val p = [(Rat.one, [(1,1),(0,1)]), (Rat.one, [])] : poly;
val p = [(Rat (true, 1, 1), [(1, 1), (0, 1)]), (Rat (true, 1, 1), [])]: poly
> p_toString p;
val it = "x1 x0 + 1": string
> val q = [(Rat.one, [(2,1),(0,1)]), (Rat.one, [])] : poly;
val q = [(Rat (true, 1, 1), [(2, 1), (0, 1)]), (Rat (true, 1, 1), [])]: poly
> p_toString q;
val it = "x2 x0 + 1": string
> buchberger [p,q];
val it =
[[(Rat (true, 1, 1), [(2, 1)]), (Rat (false, 1, 1), [(1, 1)])],
[(Rat (true, 1, 1), [(1, 1), (0, 1)]), (Rat (true, 1, 1), [])],
[(Rat (true, 1, 1), [(2, 1), (0, 1)]), (Rat (true, 1, 1), [])]]:
poly list
> map p_toString (buchberger [p,q]);
val it = ["x2 + -1 x1", "x1 x0 + 1", "x2 x0 + 1"]: string list
``````
• An example with real algebraic numbers:

``````\$ poly

Poly/ML 5.5.1 Release
> use "top.sml"; (* Load libraries and open namespaces *)
> val p = [(Rat.one, [(0, 2)]), (Rat.rat_of_int ~2, [])] : poly;
val p = [(Rat (true, 1, 1), [(0, 2)]), (Rat (false, 2, 1), [])]: poly
> p_toString p;
val it = "x0^2 + -2": string
> val alpha = mk_real_alg p Rat.zero (Rat.rat_of_int 5);
val alpha =
([(Rat (true, 1, 1), [(0, 2)]), (Rat (false, 2, 1), [])],
Rat (true, 1, 4), Rat (true, 5, 1)): real_alg
> toString(alpha);
val it = "RealRoot(x0^2 + -2, [1/4, 5])": string
> val beta = mk_real_alg p Rat.zero Rat.zero;
Exception-
Non_unique
"Poly (x0^2 + -2) does not have exactly one root in the interval [0, 0]."
raised
> val beta = mk_real_alg p (Rat.rat_of_int ~2) Rat.zero;
val beta =
([(Rat (true, 1, 1), [(0, 2)]), (Rat (false, 2, 1), [])],
Rat (false, 2, 1), Rat (false, 1, 4)): real_alg
> toString(beta);
val it = "RealRoot(x0^2 + -2, [-2, -1/4])": string
> val gamma = add(alpha, beta);
val gamma =
([(Rat (true, 1, 1), [(0, 1)])], Rat (true, 0, 1), Rat (true, 0, 1)):
real_alg
> toString(gamma);
val it = "RealRoot(x0, [0, 0])": string``````

• Please email me if you have any questions!