References

  1. Clark Barrett, Pascal Fontaine & Cesare Tinelli (2017): The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org.
  2. R. S. Boyer & J S. Moore (1979): A Computational Logic. Academic Press.
  3. Rudy Braquehais & Colin Runciman (2017): Speculate: discovering conditional equations and inequalities about black-box functions by reasoning from test results. In: Proceedings of the 10th ACM SIGPLAN International Symposium on Haskell, pp. 40–51, doi:10.1145/3156695.3122961.
  4. Koen Claessen & John Hughes (2000): QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of ICFP, pp. 268–279, doi:10.1145/351240.351266.
  5. Koen Claessen & John Hughes (2002): Testing Monadic Code with QuickCheck. SIGPLAN Notices 37(12), pp. 4759, doi:10.1145/636517.636527.
  6. Koen Claessen, Moa Johansson, Dan Rosén & Nicholas Smallbone (2013): Automating Inductive Proofs using Theory Exploration. In: Proceedings of the Conference on Automated Deduction (CADE), LNCS 7898. Springer, pp. 392–406, doi:10.1007/978-3-642-38574-2_27.
  7. Koen Claessen, Moa Johansson, Dan Rosén & Nicholas Smallbone (2015): TIP: Tons of Inductive Problems. In: Conference on Intelligent Computer Mathematics, LNCS 9150. Springer, pp. 333–337, doi:10.1007/978-3-319-20615-8_23.
  8. Simon Colton (2002): The HR Program for Theorem Generation. In: Andrei Voronkov: Automated Deduction—CADE-18. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 285–289, doi:10.1007/3-540-45620-1_24.
  9. Lucas Dixon & Moa Johansson (2007): IsaPlanner 2: A Proof Planner for Isabelle. DReaM Technical Report (System description).
  10. Sólrún Halla Einarsdóttir, Moa Johansson & Johannes Åman Pohjola (2018): Into the Infinite - Theory Exploration for Coinduction. In: Proceedings of AISC 2018, pp. 70–86, doi:10.1007/978-3-319-99957-9_5.
  11. Sólrún Halla Einarsdóttir, Nicholas Smallbone & Moa Johansson (2021): Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing. Post-proceedings of IFL'20.
  12. Siemion Fajtlowicz (1988): On conjectures of Graffiti. Annals of Discrete Mathematics 38, pp. 113–118, doi:10.1016/S0167-5060(08)70776-3.
  13. M. Hajdu, P. Hozzova, L. Kovacs, J. Schoisswohl & A. Voronkov (2020): Induction with Generalization in Superposition Reasoning. In: Intelligent Computer Mathematics. CICM 2020, LNCS 12236. Springer, doi:10.1007/978-3-030-53518-6_8.
  14. Jonathan Heras, Ekaterina Komendantskaya, Moa Johansson & Ewen Maclean (2013): Proof-Pattern Recognition and Lemma Discovery in ACL2. In: Proceedings of LPAR, doi:10.1007/978-3-642-45221-5_27.
  15. Paul Hudak (200): The Haskell School of Expression: Learning Functional Programming through Multimedia. Cambridge University Press, doi:10.1017/CBO9780511818073.
  16. Andrew Ireland & Alan Bundy (1996): Productive Use of Failure in Inductive Proof. Journal of Automated Reasoning 16, pp. 79–111, doi:10.1007/BF00244460.
  17. Moa Johansson (2017): Automated theory exploration for interactive theorem proving: An introduction to the Hipster system. In: Proceedings of ITP, LNCS 10499. Springer, pp. 1–11, doi:10.1007/978-3-319-66107-0_1.
  18. Moa Johansson, Lucas Dixon & Alan Bundy (2011): Conjecture Synthesis for Inductive Theories. Journal of Automated Reasoning 47(3), pp. 251–289, doi:10.1007/s10817-010-9193-y.
  19. Moa Johansson, Dan Rosén, Nicholas Smallbone & Koen Claessen (2014): Hipster: Integrating Theory Exploration in a Proof Assistant. In: Proceedings of CICM. Springer, pp. 108–122, doi:10.1007/978-3-319-08434-3_9.
  20. Douglas B. Lenat (1976): AM, an artificial intelligence approach to discovery in mathematics as heuristic search. Stanford University.
  21. R. L. McCasland, A. Bundy & P. F. Smith (2017): MATHsAiD: Automated mathematical theory exploration. Applied Intelligence, doi:10.1007/s10489-017-0954-8.
  22. Omar Montano-Rivas, Roy McCasland, Lucas Dixon & Alan Bundy (2012): Scheme-based theorem discovery and concept invention. Expert systems with applications 39(2), pp. 1637–1646, doi:10.1016/j.eswa.2011.06.055. Available at https://hdl.handle.net/1842/6269.
  23. Markus N. Rabe, Dennis Lee, Kshitij Bansal & Christian Szegedy (2021): Mathematical Reasoning via Self-supervised Skip-tree Training. Accepted for ICLR 2021, to appear..
  24. Juan Ricart (2019): Hopster: Automated discovery of mathematical properties in HOL. Chalmers University of Technology. Available at https://hdl.handle.net/20.500.12380/300420.
  25. Dan Rosén & Nicholas Smallbone (2015): TIP: Tools for Inductive Provers. In: Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS 9450. Springer, pp. 219–232, doi:10.1007/978-3-662-48899-7_16.
  26. Nicholas Smallbone, Moa Johansson, Koen Claessen & Maximilian Algehed (2017): Quick specifications for the busy programmer. Journal of Functional Programming 27, doi:10.1017/S0956796817000090.
  27. Willam Sonnex, Sophia Drossopoulou & Susan Eisenbach (2012): Zeno: An automated prover for properties of recursive datatypes. In: Proceedings of TACAS. Springer, pp. 407–421, doi:10.1007/978-3-642-28756-5_28.
  28. Josef Urban & Jan Jakubův (2020): First Neural Conjecturing Datasets and Experiments. In: Proceedings of CICM, doi:10.1007/978-3-030-53518-6_24.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org