References

  1. M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry & B. Werner (2011): A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In: 1st International Conference on Certified Programs and Proofs (CPP'11), Lecture Notes in Computer Science 7086, pp. 135–150, doi:10.1007/978-3-642-25379-9_12.
  2. A. Asperti, F. Guidi, C. Sacerdoti Coen, E. Tassi & S. Zacchiroli (2006): A Content Based Mathematical Search Engine: Whelp. In: Post-Proceedings of the TYPES'04 International Conference, Lecture Notes in Computer Science 3839, pp. 17–32, doi:10.1007/11617990_2.
  3. A. Asperti, W. Ricciotti, C. Sacerdoti Coen & E. Tassi (2011): The Matita interactive Theorem prover. In: 23rd International Conference on Automated Deduction (CADE'11), Lecture Notes in Computer Science 6803, pp. 64–69, doi:10.1007/978-3-642-22438-6_7.
  4. D. Aspinall (2000): Proof General: A Generic Tool for Proof Development. In: 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), Lecture Notes in Computer Science 1785, pp. 38–43, doi:10.1007/3-540-46419-0_3.
  5. C. Barrett & C. Tinelli (2007): CVC3. In: 19th International Conference on Computer Aided Verification (CAV'07), Lecture Notes in Computer Science 4590, pp. 298–302, doi:10.1007/978-3-540-73368-3_34.
  6. D. Basin, A. Bundy, D. Hutter & A. Ireland (2005): Rippling: Meta-level Guidance for Mathematical Reasoning. Cambridge University Press.
  7. A. Bauer, E. M. Clarke & X. Zhao (1998): Analytica - an experiment in combining theorem proving and symbolic computation. Journal of Automated Reasoning 21(3), pp. 295–325, doi:10.1023/A:1006079212546.
  8. C. Bishop (2006): Pattern Recognition and Machine Learning. Springer.
  9. J. C. Blanchette, S. Böhme & L. C. Paulson (2011): Extending Sledgehammer with SMT Solvers. In: 23rd International Conference on Automated Deduction (CADE-23), Lecture Notes in Computer Science 6803, pp. 116–130, doi:10.1007/978-3-642-22438-6_11.
  10. J. C. Blanchette, S. Böhme, A. Popescu & N. Smallbone (2013): Encoding monomorphic and polymorphic types. In: 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), Lecture Notes in Computer Science 7795, pp. 493–507, doi:10.1007/978-3-642-36742-7_34.
  11. A. Bove, P. Dybjer & U. Norell (2009): A Brief Overview of Agda — A Functional Language with Dependent Types. In: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), Lecture Notes in Computer Science 5674, pp. 73–78, doi:10.1007/978-3-642-03153-3.
  12. A. Bundy, D. Hutter, C. B. Jones & J S. Moore (2012): AI meets Formal Software Development (Dagstuhl Seminar 12271). Dagstuhl Reports 2(7), pp. 1–29, doi:10.4230/DagRep.2.7.1.
  13. K. Claessen, M. Johansson, D. Rosén & N. Smallbone (2013): Automating Inductive Proofs using Theory Exploration. In: 24th International Conference on Automated Deduction (CADE–24), To be published in Lecture Notes in Computer Sciene, doi:10.1007/978-3-642-38574-2_27.
  14. Coq development team (2012): The Coq Proof Assistant Reference Manual, version 8.4. Technical Report.
  15. Thierry Coquand & Gérard P. Huet (1988): The Calculus of Constructions. Inf. Comput. 76(2/3), pp. 95–120, doi:10.1016/0890-5401(88)90005-3.
  16. J. Denzinger, M. Fuchs, C. Goller & S. Schulz (1999): Learning from Previous Proof Experience: A Survey. Technical Report. Technische Universitat Munchen.
  17. J. Denzinger & S. Schulz (2000): Automatic Acquisition of Search Control Knowledge from Multiple Proof Attempts. Information and Computation 162(1-2), pp. 59–79, doi:10.1006/inco.1999.2857.
  18. L. Dixon & J. D. Fleuriot (2003): IsaPlanner: A Prototype Proof Planner in Isabelle. In: 19th International Conference on Automated Deduction (CADE'2003), Lecture Notes in Computer Science 2741, pp. 279–283, doi:10.1007/978-3-540-45085-6_22.
  19. H. Duncan (2002): The use of Data-Mining for the Automatic Formation of Tactics. University of Edinburgh.
  20. B. Dutertre & L. de Moura (2006): The Yices SMT solver. Available at http://yices.csl.sri.com/tool-paper.pdf.
  21. G. Gonthier (2008): Formal proof - The Four-Color Theorem. Notices of the American Mathematical Society 55(11), pp. 1382–1393.
  22. G. Gonthier & A. Mahboubi (2010): An introduction to small scale reflection. Journal of Formalized Reasoning 3(2), pp. 95–152, doi:10.6092/issn.1972-5787/1979.
  23. A. Grabowski, A. Kornilowicz & A. Naumowicz (2010): Mizar in a nutshell. Journal of Formalized Reasoning 3(2), pp. 153–245, doi:10.6092/issn.1972-5787/1980.
  24. G. Grov, E. Komendantskaya & A. Bundy (2012): A Statistical Relational Learning Challenge - extracting proof strategies from exemplar proofs. In: ICML'12 worshop on Statistical Relational Learning.
  25. T. Hales (2005): The Flyspeck Project fact sheet. Project description available at http://code.google.com/p/flyspeck/.
  26. M. Hall (2009): The WEKA Data Mining Software: An Update. SIGKDD Explorations 11(1), pp. 10–18, doi:10.1145/1656274.1656278.
  27. J. Harrison & L. Théry (1998): A skeptic approach to combining HOL and Maple. Journal of Automated Reasoning 21, pp. 279–294, doi:10.1023/A:1006023127567.
  28. J. Heras & E. Komendantskaya (2012): ML4PG: machine learning interface for Proof General. Program files and user manual. http://www.computing.dundee.ac.uk/staff/katya/ML4PG/.
  29. J. Heras & E. Komendantskaya (2013): ML4PG in Computer Algebra Verification. In: Conferences on Intelligent Computer Mathematics (CICM'13), Lecture Notes in Computer Science 7961, pp. 354–358.
  30. W. A. Hunt & E. Reeber (2006): A SAT-based procedure for verifying finite state machines in ACL2. In: 6th International workshop on the ACL2 theorem prover and its applications, pp. 127–135, doi:10.1145/1217975.1218001.
  31. M. Jamnik, M. Kerber & C. Benzmller (2002): Automatic learning of proof methods in proof planning. Technical Report.
  32. M. Johansson, L. Dixon & A. Bundy (2011): Conjecture Synthesis for Inductive Theories. Journal of Automated Reasoning 47(3), pp. 251–289, doi:10.1007/s10817-010-9193-y.
  33. I. Joliffe (1986): Principal Components Analysis. Springer-Verlag, doi:10.1007/978-1-4757-1904-8.
  34. M. Kaufmann & J S. Moore (2012): Accumulated persistence in ACL2. http://www.cs.utexas.edu/users/moore/acl2/current/ACCUMULATED-PERSISTENCE.html.
  35. M. Kaufmann, P. Manolios & J S. Moore (2000): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers.
  36. M. Kaufmann, P. Manolios, J S. Moore & D. Vroon (2006): Integrating CCG analysis into ACL2. In: Eighth International Workshop on Termination, part of FLOC'06, doi:10.1.1.79.4636.
  37. E. Komendantskaya & K. Lichota (2012): Neural Networks for Proof-Pattern Recognition. In: International Conference on Artificial Neural Networks (ICANN'12), Lecture Notes in Computer Science 7553, pp. 427–435, doi:10.1007/978-3-642-33266-1_53.
  38. V. Komendantsky, A. Konovalov & S. Linton (2012): Interfacing Coq + SSReflect with GAP. In: 9th International Workshop On User Interfaces for Theorem Provers (UITP'10), Electronic Notes in Theoretical Computer Science 285, pp. 17–28, doi:10.1016/j.entcs.2012.06.003.
  39. D. Kuehlwein & J. Urban (2012): Learning from Multiple Proofs: first experiments. In: 3rd Workshop on Practical Aspects of Automated Reasoning (PAAR'12), pp. 82–94.
  40. D. Kühlwein, J. C. Blanchette, C. Kaliszyk & J. Urban (2013): MaSh: Machine Learning for Sledgehammer. In: 4th Conference on Interactive Theorem Proving (ITP'13), To be published in Lecture Notes in Computer Sciene.
  41. D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban & T. Heskes (2012): Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics. In: 6th International Joint Conference on Automated Reasoning (IJCAR'12), Lecture Notes in Computer Science 7364, pp. 378–392, doi:10.1007/978-3-642-31365-3_30.
  42. MATLAB (2012): version 7.14.0 (R2012a). The MathWorks Inc., Natick, Massachusetts.
  43. J. Meng & L. C. Paulson (2009): Lightweight relevance filtering for machine-generated resolution problems. Journal of Applied Logic 7(1), pp. 41–57, doi:10.1016/j.jal.2007.07.004.
  44. J. Meng & L. C. Paulson (2009): Translating higher-order clauses to first-order clauses. Journal of Automated Reasoning 40(1), pp. 35–60, doi:10.1007/s10817-007-9085-y.
  45. A. Mercer, A. Bundy, H. Duncan & D. Aspinall (2006): PG Tips: A Recommender System for an Interactive Theorem Prover. In: Mathematical User-Interfaces Workshop (MathUI'2006).
  46. L. M. de Moura & N. Bjorner (2008): Z3: An efficient SMT solver. In: 14th Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), Lecture Notes in Computer Science 4963, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  47. T. Nipkow, L. C. Paulson & M. Wenzel (2002): Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science 2283. Springer, doi:10.1007/3-540-45949-9.
  48. L. C. Paulson & J. C. Blanchette (2010): Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. In: 8th International Workshop on the Implementation of Logics (IWIL'10), doi:10.1.1.186.3278.
  49. A. Riazano & A. Voronkov (2002): The design and implementation of Vampire. Artificial Intelligence Communications 15(2–3), pp. 91–110. Available at http://iospress.metapress.com/content/ajar8kjbdtdf7kc2/.
  50. D. Rosén (2012): Proving Equational Haskell Properties using Automated Theorem Provers. University of Gothenburg, Sweden.
  51. S. Schulz (2004): System description: E 0.81. In: 2nd International Joint Conference on Automated Reasoning (IJCAR'04), Lecture Notes in Computer Science 3097, pp. 223–228, doi:10.1007/978-3-540-25984-8_15.
  52. Mathematical components team (2012): Formalization of the Odd Order theorem. Technical Report. http://www.msr-inria.inria.fr/Projects/math-components.
  53. E. Tsivtsivadze, J. Urban, H. Geuvers & T. Heskes (2011): Semantic Graph Kernels for Automated Reasoning. In: SIAM Conference on Data Mining (SDM'11). SIAM / Omnipress, pp. 795–803. Available at http://siam.omnibooksonline.com/2011datamining/data/papers/231.pdf#page=1.
  54. J. Urban (2006): MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Journal of Applied Logic 4(4), pp. 414–427, doi:10.1016/j.jal.2005.10.004.
  55. J. Urban (2006): MPTP 0.2: Design, Implementation, and Initial Experiments. Journal of Automated Reasoning 37(1-2), pp. 21–43, doi:10.1007/s10817-006-9032-3.
  56. J. Urban, G. Sutcliffe, P. Pudlák & J. Vyskocil (2008): MaLARea SG1- Machine Learner for Automated Reasoning with Semantic Guidance. In: 4th International Joint Conference on Automated Reasoning (IJCAR'08), Lecture Notes in Computer Science 5195, pp. 441–456, doi:10.1007/978-3-540-71070-7_37.
  57. C. Weidenbach (2001): Combining superposition, sorts and splitting, pp. 1965–2013, Handbook of Automated Reasoning. Elsevier.
  58. R. Xu & D. Wunsch (2005): Survey of Clustering Algorithms. IEEE Transactions on Neural Networks 16(3), pp. 645–678, doi:10.1109/TNN.2005.845141.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org