| C++ GUI Programming with Qt 4 J Blanchette, M Summerfield Pearson Education, 2008 | 1319* | 2008 |
| Nitpick: A counterexample generator for higher-order logic based on a relational model finder JC Blanchette, T Nipkow International conference on interactive theorem proving, 131-146, 2010 | 345 | 2010 |
| Extending Sledgehammer with SMT solvers JC Blanchette, S Böhme, LC Paulson Journal of automated reasoning 51 (1), 109-128, 2013 | 309 | 2013 |
| Hammering towards QED JC Blanchette, C Kaliszyk, LC Paulson, J Urban Journal of Formalized Reasoning 9 (1), 101-148, 2016 | 219 | 2016 |
| Automatic proof and disproof in Isabelle/HOL JC Blanchette, L Bulwahn, T Nipkow Frontiers of Combining Systems: 8th International Symposium, FroCoS 2011 …, 2011 | 136 | 2011 |
| Truly modular (co)datatypes for Isabelle/HOL JC Blanchette, J Hölzl, A Lochbihler, L Panny, A Popescu, D Traytel Interactive Theorem Proving, 93-110, 2014 | 124 | 2014 |
| MaSh: Machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban International Conference on Interactive Theorem Proving, 35-50, 2013 | 108 | 2013 |
| Encoding monomorphic and polymorphic types JC Blanchette, S Böhme, A Popescu, N Smallbone Logical Methods in Computer Science 12, 2017 | 95* | 2017 |
| TFF1: The TPTP typed first-order form with rank-1 polymorphism JC Blanchette, A Paskevich Automated Deduction–CADE-24: 24th International Conference on Automated …, 2013 | 84 | 2013 |
| A verified SAT solver framework with learn, forget, restart, and incrementality JC Blanchette, M Fleury, P Lammich, C Weidenbach Journal of automated reasoning 61, 333-365, 2018 | 81 | 2018 |
| Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving D Traytel, A Popescu, JC Blanchette Proceedings of the 2012 27th Annual IEEE/ACM Symposium on Logic in Computer …, 2012 | 80 | 2012 |
| A learning-based fact selector for Isabelle/HOL JC Blanchette, D Greenaway, C Kaliszyk, D Kühlwein, J Urban Journal of Automated Reasoning 57, 219-244, 2016 | 79 | 2016 |
| Mining the Archive of Formal Proofs JC Blanchette, M Haslbeck, D Matichuk, T Nipkow Intelligent Computer Mathematics, 3-17, 2015 | 63 | 2015 |
| Superposition for lambda-free higher-order logic A Bentkamp, J Blanchette, S Cruanes, U Waldmann Logical Methods in Computer Science 17, 2021 | 55 | 2021 |
| A decision procedure for (co)datatypes in SMT solvers A Reynolds, JC Blanchette Automated Deduction-CADE-25, 197-213, 2015 | 55 | 2015 |
| Superposition with lambdas A Bentkamp, J Blanchette, S Tourret, P Vukmirović, U Waldmann Journal of Automated Reasoning 65 (7), 893-940, 2021 | 54 | 2021 |
| Extending a brainiac prover to lambda-free higher-order logic P Vukmirović, JC Blanchette, S Cruanes, S Schulz International Conference on Tools and Algorithms for the Construction and …, 2019 | 52 | 2019 |
| More SPASS with Isabelle: Superposition with hard sorts and configurable simplification JC Blanchette, A Popescu, D Wand, C Weidenbach Interactive Theorem Proving, 345-360, 2012 | 50 | 2012 |
| Scalable fine-grained proofs for formula processing H Barbosa, JC Blanchette, P Fontaine CADE, 2017 | 44 | 2017 |
| A comprehensive framework for saturation theorem proving U Waldmann, S Tourret, S Robillard, J Blanchette IJCAR, 2020 | 43 | 2020 |
Andrei PopescuUniversity of Sheffield在 sheffield.ac.uk 的电子邮件经过验证
