<< 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)

Download code:

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 *)
    ( ... lots of printing about library loading removed ... )
    > 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 *)
    ( ... lots of printing about library loading removed ... )
    > 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!