SC-Square 2018
Satisfiability Checking and Symbolic Computation

Table of Contents

• Table of contents (pdf)
• Preface
• Program committee
• Author index
• Keyword index

1 - Invited Talk

• Hard Combinatorial Problems: A Challenge for Satisfiability (invited paper) 1
  Ilias Kotsireas

2 - Research Papers

• Towards Incremental Cylindrical Algebraic Decomposition in Maple 3
  Alexander Cowen-Rivers , Matthew England
• Evaluation of Equational Constraints for CAD in SMT Solving 19
  Rebecca Haehn , Gereon Kremer Erika Ábrahám
• Refutation of Products of Linear Polynomials 33
  Jan Horacek , Martin Kreuzer
• Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics 48
  Casey Mulligan , Russell Bradford , James H. Davenport , Matthew England , Zak Tonks
• A Practical Polynomial Calculus for Arithmetic Circuit Verification 61
  Daniela Ritirc , Armin Biere , Manuel Kauers
• Unknot Recognition Through Quantifier Elimination 77
  Meesum Syed Mohammad , 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 , Elisa Palezzato
• Constraint Systems from Traffic Scenarios for the Validation of Autonomous Driving 95
  Andreas Eggers , Matthias Stasch , Tino Teige , Tom Bienmüller , Udo Brockmeyer
• Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT 110
  Pascal Fontaine , Mizuhito Ogawa , Thomas Sturm , Van Khanh To , Xuan Tung Vu
• SMT-like Queries in Maple 118
  Stephen A. Forrest
• Techniques for Natural-style Proofs in Elementary Analysis 122
  Tudor Jebelean