| Conjecture synthesis for inductive theories M Johansson, L Dixon, A Bundy Journal of Automated Reasoning 47 (3), 251-289, 2011 | 85 | 2011 |
| Automating inductive proofs using theory exploration K Claessen, M Johansson, D Rosén, N Smallbone Automated Deduction–CADE-24, 392-406, 2013 | 83 | 2013 |
| Proof-pattern recognition and lemma discovery in ACL2 J Heras, E Komendantskaya, M Johansson, E Maclean International Conference on Logic for Programming Artificial Intelligence …, 2013 | 42 | 2013 |
| Hipster: Integrating Theory Exploration in a Proof Assistant M Johansson, D Rosén, N Smallbone, K Claessen Conference on Intelligent Computer Mathematics (CICM), 2014 | 40 | 2014 |
| TIP: Tons of Inductive Problems K Claessen, M Johansson, D Rosén, N Smallbone Conference on Intelligent Computer Mathematics, 2015 | 31 | 2015 |
| Case-Analysis for Rippling and Inductive Proof M Johansson, L Dixon, A Bundy Interactive Theorem Proving, 291-306, 2010 | 27 | 2010 |
| HipSpec: Automating Inductive Proofs of Program Properties. K Claessen, M Johansson, D Rosén, N Smallbone ATx/WInG@ IJCAR, 16-25, 2012 | 23 | 2012 |
| On interpolation in automated theorem proving MP Bonacina, M Johansson Journal of Automated Reasoning 54 (1), 69-97, 2015 | 21 | 2015 |
| Quick specifications for the busy programmer. N Smallbone, M Johansson, K Claessen, M Algehed J. Funct. Program. 27, e18, 2017 | 17 | 2017 |
| Interpolation systems for ground proofs in automated deduction: a survey MP Bonacina, M Johansson Journal of Automated Reasoning 54 (4), 353-390, 2015 | 16 | 2015 |
| On interpolation in decision procedures M Bonacina, M Johansson Automated Reasoning with Analytic Tableaux and Related Methods, 1-16, 2011 | 16 | 2011 |
| Dynamic rippling, middle-out reasoning and lemma discovery M Johansson, L Dixon, A Bundy Verification, Induction, Termination Analysis - Festschrift for Christoph …, 2010 | 12* | 2010 |
| Automated discovery of inductive lemmas M Johansson PhD. thesis, University of Edinburgh, 2009 | 11 | 2009 |
| IsaPlanner 2: A proof planner in Isabelle L Dixon, M Johansson DReaM Technical Report (System description), 2007 | 9 | 2007 |
| Automated theory exploration for interactive theorem proving M Johansson International Conference on Interactive Theorem Proving, 1-11, 2017 | 8 | 2017 |
| Conditional Lemma Discovery and Recursion Induction in Hipster I Lobo Valbuena, M Johansson 15th International Workshop on Automated Verification of Critical Systems …, 2015 | 7* | 2015 |
| Towards interpolation in an SMT solver with integrated superposition MP Bonacina, M Johansson Notes of the 9th International Workshop on Satisfiability Modulo Theories …, 2011 | 5 | 2011 |
| Towards machine learning on data from professional cyclists A Hilmkil, O Ivarsson, M Johansson, D Kuylenstierna, T van Erp arXiv preprint arXiv:1808.00198, 2018 | 4 | 2018 |
| Best-first rippling M Johansson, A Bundy, L Dixon Reasoning, Action and Interaction in AI theories and Systems, 83-100, 2006 | 4 | 2006 |
| Lemma discovery for induction M Johansson International Conference on Intelligent Computer Mathematics, 125-139, 2019 | 3 | 2019 |
Alan BundyProfessor of Automated Reasoning, University of EdinburghAdresse e-mail validée de ed.ac.uk
