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