Output details

Gröbner Basis Construction Algorithms Based on Theorem Proving Saturation Loops

<12> Originality: The chief novelty is the combination of an abstract strategy-independent framework for describing Groebner Basis construction algorithms and the presentation of instantiations of this framework that are implemented and empirically evaluated.

Significance: The implementation was incorporated into Microsoft's Z3 SMT solver and improved its capabilities for non-linear arithmetic reasoning. The Z3 solver was the best performing of the 13 competitors in the 2011 SMT competition.

Rigour: The paper includes a precise mathematical definition of the abstract framework, pseudocode for the instantiations, theorems proving the correctness of the instantiations, and experimental results.