Advertisement

Using Machine Learning to Improve Cylindrical Algebraic Decomposition

  • Zongyan Huang
  • Matthew EnglandEmail author
  • David J. Wilson
  • James Bridge
  • James H. Davenport
  • Lawrence C. Paulson
Open Access
Article
  • 57 Downloads

Abstract

Cylindrical Algebraic Decomposition (CAD) is a key tool in computational algebraic geometry, best known as a procedure to enable Quantifier Elimination over real-closed fields. However, it has a worst case complexity doubly exponential in the size of the input, which is often encountered in practice. It has been observed that for many problems a change in algorithm settings or problem formulation can cause huge differences in runtime costs, changing problem instances from intractable to easy. A number of heuristics have been developed to help with such choices, but the complicated nature of the geometric relationships involved means these are imperfect and can sometimes make poor choices. We investigate the use of machine learning (specifically support vector machines) to make such choices instead. Machine learning is the process of fitting a computer model to a complex function based on properties learned from measured data. In this paper we apply it in two case studies: the first to select between heuristics for choosing a CAD variable ordering; the second to identify when a CAD problem instance would benefit from Gröbner Basis preconditioning. These appear to be the first such applications of machine learning to Symbolic Computation. We demonstrate in both cases that the machine learned choice outperforms human developed heuristics.

Keywords

Symbolic Computation Computer Algebra Machine Learning Support Vector Machine Cylindrical Algebraic Decomposition Gröbner Basis Parameter Selection 

Mathematics Subject Classification

68W30 (Symbolic Computation and Algebraic Computation) 68T05 (Learning and Adaptive Systems) 

Notes

Acknowledgements

This work was supported by EPSRC Grant EP/J003247/1; the European Union’s Horizon 2020 research and innovation programme under Grant Agreement No 712689 (SC\(^2\)); and the China Scholarship Council (CSC). The authors acknowledge both the anonymous referees of the present paper, and those of [66, 67], whose comments also helped improve this article.

References

  1. 1.
    Ábrahám, E., Abbott, J., Becker, B., Bigatti, A.M., Brain, M., Buchberger, B., Cimatti, A., Davenport, J.H., England, M., Fontaine, P., Forrest, S., Griggio, A., Kroening, D., Seiler, W.M., Sturm, T.: \({{\sf SC}}^2\): satisfiability checking meets symbolic computation. In: Kohlhase, M., Johansson, M., Miller, B., de Moura, L., Tompa, F. (eds.) Intelligent Computer Mathematics: Proceedings CICM 2016, volume 9791 of Lecture Notes in Computer Science, pp. 28–43. Springer (2016)Google Scholar
  2. 2.
    Alpaydin, E.: Introduction to Machine Learning. MIT Press, Cambridge (2004)zbMATHGoogle Scholar
  3. 3.
    Arai, N.H., Matsuzaki, T., Iwane, H., Anai, H.: Mathematics by machine. In: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC ’14, pp. 1–8. ACM (2014)Google Scholar
  4. 4.
    Arnon, D., Collins, G.E., McCallum, S.: Cylindrical algebraic decomposition I: the basic algorithm. SIAM J. Comput. 13, 865–877 (1984)MathSciNetzbMATHGoogle Scholar
  5. 5.
    Baldi, P., Brunak, S., Chauvin, Y., Andersen, C.A.F., Nielsen, H.: Assessing the accuracy of prediction algorithms for classification: an overview. Bioinformatics 16(5), 412–424 (2000)Google Scholar
  6. 6.
    Basu, S., Pollack, R., Roy, M.E.: Algorithms in Real Algebraic Geometry. Volume 10 of Algorithms and Computations in Mathematics. Springer, Berlin (2006)zbMATHGoogle Scholar
  7. 7.
    Böge, W., Gebauer, R., Kredel, H.: Gröbner bases using SAC2. In: Caviness, B.F. (ed.) EUROCAL ’85, Volume 204 of Lecture Notes in Computer Science, pp. 272–274. Springer, Berlin (1985)Google Scholar
  8. 8.
    Boser, B.E., Guyon, I.M., Vapnik, V.N.: A training algorithm for optimal margin classifiers. In: Proceedings of the Fifth Annual Workshop on Computational Learning Theory, COLT ’92, pp. 144–152. ACM (1992)Google Scholar
  9. 9.
    Boyan, J., Freitag, D., Joachims, T.: A machine learning architecture for optimizing web search engines. In: AAAI Workshop on Internet Based Information Systems, pp. 1–8 (1996)Google Scholar
  10. 10.
    Bradford, R., Chen, C., Davenport, J.H., England, M., Moreno Maza, M., Wilson, D.: Truth table invariant cylindrical algebraic decomposition by regular chains. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing, Volume 8660 of Lecture Notes in Computer Science, pp. 44–58. Springer, Berlin (2014)Google Scholar
  11. 11.
    Bradford, R., Davenport, J.H., England, M., Errami, H., Gerdt, V., Grigoriev, D., Hoyt, C., Košta, M., Radulescu, O., Sturm, T., Weber, A.: A case study on the parametric occurrence of multiple steady states. In: Proceedings of the 2017 ACM International Symposium on Symbolic and Algebraic Computation, ISSAC ’17, pp. 45–52. ACM (2017)Google Scholar
  12. 12.
    Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Cylindrical algebraic decompositions for boolean combinations. In: Proceedings of the 38th International Symposium on Symbolic and Algebraic Computation, ISSAC ’13, pp. 125–132. ACM (2013)Google Scholar
  13. 13.
    Bradford, R., Davenport, J.H., England, M., McCallum, S., Wilson, D.: Truth table invariant cylindrical algebraic decomposition. J. Symb. Comput. 76, 1–35 (2016)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Bradford, R., Davenport, J.H., England, M., Wilson, D.: Optimising problem formulations for cylindrical algebraic decomposition. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics, Volume 7961 of Lecture Notes in Computer Science, pp. 19–34. Springer, Berlin (2013)Google Scholar
  15. 15.
    Bridge, J.P.: Machine learning and automated theorem proving. Technical Report UCAM-CL-TR-792, University of Cambridge, Computer Laboratory (2010)Google Scholar
  16. 16.
    Bridge, J.P., Holden, S.B., Paulson, L.C.: Machine learning for first-order theorem proving. J. Autom. Reason. 1–32 (2014)Google Scholar
  17. 17.
    Brown, C.W.: Improved projection for cylindrical algebraic decomposition. J. Symb. Comput. 32(5), 447–465 (2001)MathSciNetzbMATHGoogle Scholar
  18. 18.
    Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97–108 (2003)zbMATHGoogle Scholar
  19. 19.
    Brown, C.W.: Companion to the tutorial: cylindrical algebraic decomposition. Presented at ISSAC ’04 (2004). http://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf
  20. 20.
    Brown, C.W.: Open non-uniform cylindrical algebraic decompositions. In: Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15, pp. 85–92. ACM (2015)Google Scholar
  21. 21.
    Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC ’07, pp. 54–60. ACM (2007)Google Scholar
  22. 22.
    Brown, C.W., El Kahoui, M., Novotni, D., Weber, A.: Algorithmic methods for investigating equilibria in epidemic modelling. J. Symb. Comput. 41, 1157–1173 (2006)zbMATHGoogle Scholar
  23. 23.
    Brown, C.W., Kosta, M.: Constructing a single cell in cylindrical algebraic decomposition. J. Symb. Comput. 70, 14–48 (2015)MathSciNetzbMATHGoogle Scholar
  24. 24.
    Buchberger, B.: Bruno Buchberger’s Ph.D. thesis (1965): an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J. Symb. Comput. 41(3–4), 475–511 (2006)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Buchberger, B., Hong, H.: Speeding up quantifier elimination by Gröbner bases. Technical report, 91-06. RISC, Johannes Kepler University (1991)Google Scholar
  26. 26.
    Byun, H., Lee, S.: A survey on pattern recognition applications of support vector machines. Int. J. Pattern Recognit. Artif. Intell. 17(03), 459–486 (2003)Google Scholar
  27. 27.
    Carette, J.: Understanding expression simplification. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC ’04, pp. 72–79. ACM (2004)Google Scholar
  28. 28.
    Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Berlin (1998)Google Scholar
  29. 29.
    Charalampakis, A.E., Chatzigiannelis, I.: Analytical solutions for the minimum weight design of trusses by cylindrical algebraic decomposition. Arch. Appl. Mech. 88(1), 39–49 (2018)Google Scholar
  30. 30.
    Chen, C., Moreno Maza, M.: An incremental algorithm for computing cylindrical algebraic decompositions. In: Feng, R., Lee, W., Sato, Y. (eds.) Computer Mathematics, pp. 199–221. Springer, Berlin (2014)Google Scholar
  31. 31.
    Chen, C., Moreno Maza, M.: Real quantifier elimination in the RegularChains library. In: Hong, H., Yap, C. (eds.) Mathematical Software—ICMS 2014, Volume 8592 of Lecture Notes in Computer Science, pp. 283–290. Springer, Heidelberg (2014)Google Scholar
  32. 32.
    Chen, C., Moreno Maza, M.: Quantifier elimination by cylindrical algebraic decomposition based on regular chains. Journal of Symbolic Computation 75, 74–93 (2016)MathSciNetzbMATHGoogle Scholar
  33. 33.
    Chen, C., Moreno Maza, M., Xia, B., Yang, L.: Computing cylindrical algebraic decomposition via triangular decomposition. In: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC ’09, pp. 95–102. ACM (2009)Google Scholar
  34. 34.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, pp. 134–183. Springer (reprinted in the collection [28]) (1975)Google Scholar
  35. 35.
    Collins, G.E.: The SAC-2 computer algebra system. In: Caviness, B.F. (ed.) EUROCAL ’85, Volume 204 of Lecture Notes in Computer Science, pp. 34–35. Springer, Berlin (1985)Google Scholar
  36. 36.
    Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12, 299–328 (1991)MathSciNetzbMATHGoogle Scholar
  37. 37.
    Cortes, C., Vapnik, V.: Support-vector networks. Mach. Learn. 20(3), 273–297 (1995)zbMATHGoogle Scholar
  38. 38.
    Davenport, J.H., Bradford, R., England, M., Wilson, D.: Program verification in the presence of complex numbers, functions with branch cuts etc. In: 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’12, pp. 83–88. IEEE (2012)Google Scholar
  39. 39.
    Davenport, J.H., England, M.: Need polynomial systems be doubly exponential? In: Greuel, G.M., Koch, T., Paule, P., Sommese, A. (eds.) Mathematical Software—Proceedings of ICMS 2016, Volume 9725 of Lecture Notes in Computer Science, pp. 157–164. Springer, Berlin (2016)Google Scholar
  40. 40.
    Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1–2), 29–35 (1988)MathSciNetzbMATHGoogle Scholar
  41. 41.
    Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation, ISSAC ’04, pp. 111–118. ACM (2004)Google Scholar
  42. 42.
    England, M.: Machine Learning for Mathematical Software. In: Davenport, J.H., Kauers, M., Labahn, G., Urban, J. (eds.) Mathematical Software—ICMS 2018, Volume 10931 of Lecture Notes in Computer Science, pp. 165–174. Springer, Heidelberg (2018)Google Scholar
  43. 43.
    England, M., Bradford, R., Chen, C., Davenport, J.H., Moreno Maza, M., Wilson, D.: Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, Volume 8543 of Lecture Notes in Artificial Intelligence, pp. 45–60. Springer, Berlin (2014)Google Scholar
  44. 44.
    England, M., Bradford, R., Davenport, J.H.: Improving the use of equational constraints in cylindrical algebraic decomposition. In: Proceedings of the 2015 International Symposium on Symbolic and Algebraic Computation, ISSAC ’15, pp. 165–172. ACM (2015)Google Scholar
  45. 45.
    England, M., Bradford, R., Davenport, J.H., Wilson, D.: Understanding branch cuts of expressions. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics, Volume 7961 of Lecture Notes in Computer Science, pp. 136–151. Springer, Berlin (2013)Google Scholar
  46. 46.
    England, M., Bradford, R., Davenport, J.H., Wilson, D.: Choosing a variable ordering for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Hong, H., Yap, C. (eds.) Mathematical Software—ICMS 2014, Volume 8592 of Lecture Notes in Computer Science, pp. 450–457. Springer, Heidelberg (2014)Google Scholar
  47. 47.
    England, M., Davenport, J.H.: The complexity of cylindrical algebraic decomposition with respect to polynomial degree. In: Gerdt, V.P., Koepf, W., Werner, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing: 18th International Workshop, CASC 2016, Volume 9890 of Lecture Notes in Computer Science, pp. 172–192. Springer (2016)Google Scholar
  48. 48.
    England, M., Errami, H., Grigoriev, D., Radulescu, O., Sturm, T., Weber, A.: Symbolic versus numerical computation and visualization of parameter regions for multistationarity of biological networks. In: Gerdt, V.P., Koepf, W., Seiler, W.M., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing (CASC), Volume 10490 of Lecture Notes in Computer Science, pp. 93–108. Springer, Berlin (2017)Google Scholar
  49. 49.
    England, M., Wilson, D., Bradford, R., Davenport, J.H.: Using the regular chains library to build cylindrical algebraic decompositions by projecting and lifting. In: Hong, H., Yap, C. (eds.) Mathematical Software—ICMS 2014, Volume 8592 of Lecture Notes in Computer Science, pp. 458–465. Springer, Berlin (2014)Google Scholar
  50. 50.
    Erascu, M., Hong, H.: Real quantifier elimination for the synthesis of optimal numerical algorithms (case study: square root computation). J. Symb. Comput. 75, 110–126 (2016)MathSciNetzbMATHGoogle Scholar
  51. 51.
    Errami, H., Eiswirth, M., Grigoriev, D., Seiler, W.M., Sturm, T., Weber, A.: Detection of Hopf bifurcations in chemical reaction networks using convex coordinates. J. Comput. Phys. 291, 279–302 (2015)MathSciNetzbMATHGoogle Scholar
  52. 52.
    Faugère, J.C.: A new efficient algorithm for computing Gröbner bases without reduction to zero (F5). In: Proceedings of the 2002 International Symposium on Symbolic and Algebraic Computation, ISSAC ’02, pp. 75–83. ACM (2002)Google Scholar
  53. 53.
    Fayyad, U.M., Irani, K.B.: Multi-interval discretization of continuous-valued attributes for classification learning. In: Proceedings of the International Joint Conference on Uncertainty in AI, pp. 1022–1027. http://trs-new.jpl.nasa.gov/dspace/handle/2014/35171 (1993)
  54. 54.
    Forsyth, R., Rada, R.: Machine Learning: Applications in Expert Systems and Information Retrieval. Halsted Press, New York (1986)Google Scholar
  55. 55.
    Graebe, H.G., Nareike, A., Johanning, S.: The SymbolicData project: towards a computer algebra social network. In: England, M., Davenport, J.H., Kohlhase, A., Kohlhase, M., Libbrecht, P., Neuper, W., Quaresma, P., Sexton, A.P., Sojka, P., Urban, J., Watt, S.M. (eds.) Joint Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress Track at CICM, Number 1186 in CEUR Workshop Proceedings (2014)Google Scholar
  56. 56.
    Guyon, I., Elisseeff, A.: An introduction to variable and feature selection. J. Mach. Learn. Res. 3, 1157–1182 (2003)zbMATHGoogle Scholar
  57. 57.
    Hall, M., Frank, E., Holmes, G., Pfahringer, B., Reutemann, P., Witten, I.H.: The WEKA data mining software: an update. SIGKDD Explor. Newsl. 11(1), 10–18 (2009)Google Scholar
  58. 58.
    Hall, M.A.: Correlation-based feature selection for discrete and numeric class machine learning. In: Proceedings of the Seventeenth International Conference on Machine Learning, ICML ’00, pp. 359–366. Morgan Kaufmann Publishers Inc. (2000)Google Scholar
  59. 59.
    Hall, M.A., Holmes, G.: Benchmarking attribute selection techniques for discrete class data mining. IEEE Trans. Knowl. Data Eng. 15(6), 1437–1447 (2003)Google Scholar
  60. 60.
    Han, J., Dai, L., Xia, B.: Constructing fewer open cells by gcd computation in CAD projection. In: Proceedings of the 39th International Symposium on Symbolic and Algebraic Computation, ISSAC ’14, pp. 240–247. ACM (2014)Google Scholar
  61. 61.
    Heinle, A., Levandovskyy, V.: The SDEval benchmarking toolkit. ACM Commun. Comput. Algebra 49(1), 1–9 (2015)MathSciNetzbMATHGoogle Scholar
  62. 62.
    Hong, H.: An improvement of the projection operator in cylindrical algebraic decomposition. In: Proceedings of the International Symposium on Symbolic and Algebraic Computation, ISSAC ’90, pp. 261–264. ACM (1990)Google Scholar
  63. 63.
    Hong, H.: Comparison of several decision algorithms for the existential theory of the reals. Technical report, RISC, Linz (1991)Google Scholar
  64. 64.
    Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Netw. 2(5), 359–366 (1989)zbMATHGoogle Scholar
  65. 65.
    Hsu, C., Chang, C., Lin, C.: A practical guide to support vector classification. Technical report, Department of Computer Science, National Taiwan University (2003)Google Scholar
  66. 66.
    Huang, Z., England, M., Davenport, J.H., Paulson, L.: Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases. In: 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC ’16), pp. 45–52. IEEE (2016)Google Scholar
  67. 67.
    Huang, Z., England, M., Wilson, D., Davenport, J.H., Paulson, L., Bridge, J.: Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics, Volume 8543 of Lecture Notes in Artificial Intelligence, pp. 92–107. Springer, Berlin (2014)Google Scholar
  68. 68.
    Huang, Z., Paulson, L.: An application of machine learning to RCF decision procedures. In: 20th Automated Reasoning Workshop, University of Dundee, UK, ARW ’13 (2013)Google Scholar
  69. 69.
    Iwane, H., Yanami, H., Anai, H., Yokoyama, K.: An effective implementation of a symbolic-numeric cylindrical algebraic decomposition for quantifier elimination. In: Proceedings of the 2009 Conference on Symbolic Numeric Computation, SNC ’09, pp. 55–64 (2009)Google Scholar
  70. 70.
    Joachims, T.: Making large-scale support vector machine learning practical. In: Schölkopf, B., Burges, C.J.C., Smola, A.J. (eds.) Advances in Kernel Methods, pp. 169–184. MIT Press, Cambridge (1999)Google Scholar
  71. 71.
    Joachims, T.: A support vector method for multivariate performance measures. In: Proceedings of the 22nd International Conference on Machine Learning, ICML ’05, pp. 377–384. ACM (2005)Google Scholar
  72. 72.
    Jovanovic, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Automated Reasoning: 6th International Joint Conference (IJCAR), Volume 7364 of Lecture Notes in Computer Science, pp. 339–354. Springer (2012)Google Scholar
  73. 73.
    Kobayashi, M., Iwane, H., Matsuzaki, T., Anai, H.: Efficient subformula orders for real quantifier elimination of non-prenex formulas. In: Kotsireas, S.I., Rump, M.S., Yap, K.C. (eds.) Mathematical Aspects of Computer and Information Sciences (MACIS ’15), Volume 9582 of Lecture Notes in Computer Science, pp. 236–251. Springer, Berlin (2016)Google Scholar
  74. 74.
    Matthews, B.W.: Comparison of the predicted and observed secondary structure of T4 phage lysozyme. Biochim. Biophys. Acta (BBA) Protein Struct. 405(2), 442–451 (1975)Google Scholar
  75. 75.
    Mayr, E.W., Meyer, A.R.: The complexity of the word problems for commutative semigroups and polynomial ideals. Adv. Math. 46(3), 305–329 (1982)MathSciNetzbMATHGoogle Scholar
  76. 76.
    McCallum, S.: An improved projection operation for cylindrical algebraic decomposition. In: Caviness, B., Johnson, J. (eds.) Quantifier Elimination and Cylindrical Algebraic Decomposition, Texts and Monographs in Symbolic Computation, pp. 242–268. Springer, Berlin (1998)Google Scholar
  77. 77.
    McCallum, S.: On projection in CAD-based quantifier elimination with equational constraint. In: Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, ISSAC ’99, pp. 145–149. ACM (1999)Google Scholar
  78. 78.
    McCallum, S., Hong, H.: On using Lazard’s projection in CAD construction. J. Symb. Comput. 72, 65–81 (2016)MathSciNetzbMATHGoogle Scholar
  79. 79.
    McCulloch, W.S., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. Bull. Math. Biophys. 5(4), 115–133 (1943)MathSciNetzbMATHGoogle Scholar
  80. 80.
    Mulligan, C.B.: Automated economic reasoning with quantifier elimination. Working Paper 22922, National Bureau of Economic Research (2016)Google Scholar
  81. 81.
    Patel, B.R., Kaushik, K.R.: A survey on decision tree algorithm for classification. Int. J. Eng. Dev. Res. 2, 1–5 (2014)Google Scholar
  82. 82.
    Paulson, L.C.: Metitarski: past and future. In: Beringer, L., Felty, A. (eds.) Interactive Theorem Proving, Volume 7406 of Lecture Notes in Computer Science, pp. 1–10. Springer, Berlin (2012)Google Scholar
  83. 83.
    Platzer, A., Quesel, J.D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Automated Reasoning, Volume 5195 of Lecture Notes in Computer Science, pp. 171–178. Springer, Berlin (2008)Google Scholar
  84. 84.
    Platzer, A., Quesel, J.D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) Automated Deduction (CADE-22), Volume 5663 of Lecture Notes in Computer Science, pp. 485–501. Springer, Berlin (2009)Google Scholar
  85. 85.
    Press, W.H., Teukolsky, S.A., Vetterling, W.T., Flannery, B.P.: Numerical Recipes in C (2nd Ed.): The Art of Scientific Computing. Cambridge University Press, Cambridge (1992)zbMATHGoogle Scholar
  86. 86.
    Quinlan, J.R.: Induction of decision trees. Mach. Learn. 1(1), 81–106 (1986)Google Scholar
  87. 87.
    Rosenblatt, F.: The perceptron: a probabilistic model for information storage and organization in the brain. Psychol. Rev. 65(6), 386 (1958)Google Scholar
  88. 88.
    Schölkopf, B., Tsuda, K., Vert, J.-P.: Kernel methods in computational biology. MIT Press, Cambridge (2004)Google Scholar
  89. 89.
    Sebastiani, F.: Machine learning in automated text categorization. ACM Comput. Surv. 34(1), 1–47 (2002)Google Scholar
  90. 90.
    Shannon, Claude E.: A mathematical theory of communication. Mob. Comput. Commun. Rev. 5(1), 3–55 (2001)MathSciNetGoogle Scholar
  91. 91.
    Shawe-Taylor, J., Cristianini, N.: Kernel Methods for Pattern Analysis. Cambridge University Press, Cambridge (2004)zbMATHGoogle Scholar
  92. 92.
    Stone, P., Veloso, M.: Multiagent systems: a survey from a machine learning perspective. Auton. Robot. 8(3), 345–383 (2000)Google Scholar
  93. 93.
    Strzeboński, A.: Cylindrical algebraic decomposition using validated numerics. J. Symb. Comput. 41(9), 1021–1038 (2006)MathSciNetzbMATHGoogle Scholar
  94. 94.
    Strzeboński, A.: Cylindrical algebraic decomposition using local projections. J. Symb. Comput. 76, 36–64 (2016)MathSciNetzbMATHGoogle Scholar
  95. 95.
    Tarski, A.: A Decision Method for Elementary Algebra and Geometry. RAND Corporation, Santa Monica, CA (reprinted in the collection [28]) (1948)Google Scholar
  96. 96.
    Vapnik, V.N., Chervonenkis, A.Y.: A note on one class of perceptrons. Autom. Remote Control 25(1), 821–837 (1964)zbMATHGoogle Scholar
  97. 97.
    Wilson, D., Bradford, R., Davenport, J.H., England, M.: Cylindrical algebraic sub-decompositions. Math. Comput. Sci. 8, 263–288 (2014)MathSciNetzbMATHGoogle Scholar
  98. 98.
    Wilson, D., Davenport, J.H., England, M., Bradford, R.: A “piano movers” problem reformulated. In: 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’13, pp. 53–60. IEEE (2013)Google Scholar
  99. 99.
    Wilson, D., England, M., Davenport, J.H., Bradford, R.: Using the distribution of cells by dimension in a cylindrical algebraic decomposition. In: 16th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC ’14, pp. 53–60. IEEE (2014)Google Scholar
  100. 100.
    Wilson, D.J., Bradford, R.J., Davenport, J.H.: A repository for CAD examples. ACM Commun. Comput. Algebra 46(3), 67–69 (2012)zbMATHGoogle Scholar
  101. 101.
    Wilson, D.J., Bradford, R.J., Davenport, J.H.: Speeding up cylindrical algebraic decomposition by Gröbner bases. In: Jeuring, J., Campbell, J.A., Carette, J., Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) Intelligent Computer Mathematics, Volume 7362 of Lecture Notes in Computer Science, pp. 280–294. Springer, Berlin (2012)Google Scholar

Copyright information

© The Author(s) 2019

Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Authors and Affiliations

  • Zongyan Huang
    • 1
  • Matthew England
    • 2
    Email author
  • David J. Wilson
    • 3
  • James Bridge
    • 1
  • James H. Davenport
    • 3
  • Lawrence C. Paulson
    • 1
  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeUK
  2. 2.Faculty of Engineering, Environment and ComputingCoventry UniversityCoventryUK
  3. 3.Department of Computer ScienceUniversity of BathBathUK

Personalised recommendations