SC-square 2018 Table of Contents Table of Contents Preface . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii Program committee . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . v Author index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . vii Keyword index . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . ix 1 Invited talk Hard Combinatorial Problems: A Challenge for Satisfiability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 Ilias Kotsireas 2 Research papers Towards Incremental Cylindrical Algebraic Decomposition in Maple . . . . . . . . . . . . . . . . . . . . . . 3 Alexander Cowen-Rivers and Matthew England Evaluation of Equational Constraints for CAD in SMT Solving . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 Rebecca Haehn, Gereon Kremer and Erika Ábrahám 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 Verification . . . . . . . . . . . . . . . . . . . . . . 61 Daniela Ritirc, Armin Biere and Manuel Kauers Unknot Recognition Through Quantifier Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 Meesum Syed Mohammad and Prathamesh T. V. H. 3 Extended abstracts New in CoCoA-5.2.4 and CoCoALib-0.99600 for SC-Square . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 John Abbott, Anna Maria Bigatti and Elisa Palezzato Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving . . . . . 95 Andreas Eggers, Matthias Stasch, Tino Teige, Tom Bienmüller and Udo Brockmeyer Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT . . . . . . . . . . . . . . 110 Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Van Khanh To and Xuan Tung Vu SMT-like Queries in Maple . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 Stephen A. Forrest Techniques for Natural-style Proofs in Elementary Analysis. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 122 Tudor Jebelean i SC-square 2018 Table of Contents ii