| Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. J Alama, D Kühlwein, E Tsivtsivadze, J Urban, T Heskes Journal of Automated Reasoning 52 (2), 191-213, 2014 | 180 | 2014 |
| MaSh: machine learning for Sledgehammer D Kühlwein, JC Blanchette, C Kaliszyk, J Urban Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013 | 110 | 2013 |
| Overview and evaluation of premise selection techniques for large theory mathematics D Kühlwein, T van Laarhoven, E Tsivtsivadze, J Urban, T Heskes Automated Reasoning: 6th International Joint Conference, IJCAR 2012 …, 2012 | 88 | 2012 |
| The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts M Cramer, B Fisseni, P Koepke, D Kühlwein, B Schröder, J Veldman Controlled Natural Language, 170-186, 2010 | 83 | 2010 |
| 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 | 80 | 2016 |
| MaLeS: A framework for automatic tuning of automated theorem provers D Kühlwein, J Urban Journal of Automated Reasoning 55, 91-116, 2015 | 34 | 2015 |
| E-MaLeS 1.1 D Kühlwein, S Schulz, J Urban International Conference on Automated Deduction, 407-413, 2013 | 29 | 2013 |
| The Naproche System D Kühlwein, M Cramer, P Koepke, B Schröder Intelligent Computer Mathematics, Springer LNCS, ISBN, 978-3, 2009 | 27* | 2009 |
| Automated and human proofs in general mathematics: An initial comparison J Alama, D Kühlwein, J Urban International Conference on Logic for Programming Artificial Intelligence …, 2012 | 21 | 2012 |
| Learning from multiple proofs: First experiments D Kühlwein, J Urban PAAR, 82-94, 2012 | 18 | 2012 |
| Premise selection in the Naproche system M Cramer, P Koepke, D Kühlwein, B Schröder Automated Reasoning: 5th International Joint Conference, IJCAR 2010 …, 2010 | 16 | 2010 |
| A Survey of Axiom Selection as a Machine Learning Problem D Kühlwein, JC Blanchette Infinity, Computability and Metamathematics - Festschrift celebrating the …, 2014 | 7* | 2014 |
| Presupposition Projection and Accommodation in Mathematical Texts. M Cramer, D Kühlwein, B Schröder KONVENS, 29-36, 2010 | 7 | 2010 |
| Ein Kalkül für Proof Representation Structures (A calculus for Proof Representation Structures) D Kühlwein | 7* | 2008 |
| Machine Learning for Automated Reasoning D Kühlwein Radboud University Nijmegen, 2014 | 6 | 2014 |
| Experiments with strategy learning for E prover D Kühlwein, S Schulz, J Urban 2nd Joint International Workshop on Strategies in Rewriting, Proving and …, 2012 | 3 | 2012 |
| Multi-output ranking for automated reasoning D Kühlwein, J Urban, E Tsivtsivadze, H Geuvers, T Heskes International Conference on Knowledge Discovery and Information Retrieval 2 …, 2011 | 3 | 2011 |
| Learning2Reason D Kühlwein, J Urban, E Tsivtsivadze, H Geuvers, T Heskes Intelligent Computer Mathematics: 18th Symposium, Calculemus 2011, and 10th …, 2011 | 1 | 2011 |
| A short introduction to Naproche v0. 1 D Kuehlwein | 1 | 2008 |
| from Landau in Naproche M Carl, M Cramer, D Kühlwein | | 2009 |
Josef UrbanDistinguished Researcher at Czech Technical University in PragueVerified email at cvut.cz