Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii Program committee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Author index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vii Keyword index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix Hard Combinatorial Problems: A Challenge for Satis ability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Ilias Kotsireas 2 Research papers Towards Incremental Cylindrical Algebraic Decomposition in Maple . . . . . . . . . . . . . . . . . . . . . . Alexander Cowen-Rivers and Matthew England Evaluation of Equational Constraints for CAD in SMT Solving . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Rebecca Haehn, Gereon Kremer and Erika Abraham Refutation of Products of Linear Polynomials . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Jan Horacek and Martin Kreuzer Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics 48 Casey Mulligan, Russell Bradford, James H. Davenport, Matthew England and Zak Tonks A Practical Polynomial Calculus for Arithmetic Circuit Veri cation . . . . . . . . . . . . . . . . . . . . . . 61 Daniela Ritirc, Armin Biere and Manuel Kauers Unknot Recognition Through Quanti er Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Meesum Syed Mohammad and Prathamesh T. V. H.
3