Urban

CV

Scientific CV of Josef Urban, Ph.D.
CIIRC, Czech Technical University in Prague,
Zikova 4, 166 36 Praha 6 – Dejvice, Czech Republic

Josef.Urban@gmail.com, www.cs.ru.nl/~urban/
Phone: +420224354130

Education: Charles University in Prague, Czech Republic
10/98 - 12/04
10/92 - 9/98
10/92 - 6/95

Ph.D. in Computer Science
M.S. in Mathematics
B.S. in Economics

Position:
9/15 - ongoing
9/09 - 8/15
3/09 - 6/09
4/06 - 10/07
7/05 - 3/09
2/04 - 8/04, 2/02 - 8/02

Faculty of Mathematics and Physics
Faculty of Mathematics and Physics
Faculty of Social Sciences

Researcher (ERC grant holder), CIIRC, Czech Technical University
Postdoc researcher, Intelligent Systems, Radboud University Nijmegen
Visiting researcher, College of Engineering, American University in Armenia
Visiting Marie Curie researcher, University of Miami, Dept. of Comp. Sci.
Assistant professor, Dept. of Theoretical Comp. Science, Charles University
Young Visiting Researcher, Dept. of Comp. Science, University of Bialystok

Research Interests:
Automated Reasoning, Artificial Intelligence, Formal Mathematics and Verification, Machine Learning,
Semantic KBs, Automated Reasoning in Large Theories, Combining Deductive and Inductive Reasoning
Selected Funding:
9/15 - ongoing AI for Large-Scale Computer-Assisted Reasoning, ERC Consolidator, PI, EUR
1499500
9/12 - 8/15
Knowledge-based Automated Reasoning, NWO, PI and postdoc, EUR 205000
9/10 - 8/15
Learning to Reason: a Machine Learning Approach for Computer-Assisted Reasoning, NWO PhD funding, Co-investigator, EUR 205000
9/09 - 8/12
MathWiki a Web-based Collaborative Authoring Environment for Formal Proofs,
NWO, Postdoc researcher, EUR 362406
4/06 - 6/08
Automated Reasoning in Large Formal Mathematical Knowledge Bases, Marie-Curie
Fellowship, (MOIF-CT-2005-21875), Principal investigator, EUR 176076.5
4/05 - 12/06
Tools and Formats for Automated Theorem Proving in Large Mathematical Knowledge Bases, Charles University grant (205-10/203336), Co-investogator, CZK 553000
2/04 - 8/04,
CALCULEMUS, European Marie-Curie Research Training Network –2/02 - 8/02
– (HPRN-CT-2000-00102), Young Visiting Researcher
Selected Journal Publications:
1. J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban. A learning-based fact
selector for Isabelle/HOL . J. Autom. Reasoning, in press, 2016.
2. J. C. Blanchette, C. Kaliszyk, L.C. Paulson, J. Urban. Hammering towards QED J. Formalized
Reasoning, 9(1): 101-148, 2016.
3. C. Kaliszyk and J. Urban. Learning-assisted Theorem Proving with Millions of Lemmas, J. Symbolic
Computation, 69:109–128, 2015. http://dx.doi.org/10.1016/j.jsc.2014.09.032 .
4. C. Kaliszyk and J. Urban. MizAR 40 for Mizar 40, J. Autom. Reasoning 55(3): 245–256 (2015).
5. D. Kühlwein and J. Urban. MaLeS: A Framework for Automatic Tuning of Automated Theorem
Provers, J. Autom. Reasoning 55(2): 91–116 (2015).
6. C. Kaliszyk and J. Urban. HOL(y)Hammer: Online ATP service for HOL Light. Mathematics in
Computer Science, 9(1): 5–22 (2015). http://dx.doi.org/10.1007/s11786-014-0182-0 .
7. C. Kaliszyk and J. Urban. Learning-assisted Automated Reasoning with Flyspeck. J. Autom. Reasoning 53(2):173–213, 2014.
Page 1 of 8

UrbanCV

8. J. Alama, D. Kühlwein, E. Tsivtsivadze, J. Urban, T. Heskes. Premise Selection for Mathematics by
Corpus Analysis and Kernel Methods. J. Autom. Reasoning, 52(2):191–213, 2014.
9. J. Urban, P. Rudnicki, and G. Sutcliffe. ATP and Presentation Service for Mizar Formalizations. J.
Autom. Reasoning, 50(2): 229–241, 2013.
10. M. Iancu, M. Kohlhase, F. Rabe, J. Urban. The Mizar Mathematical Library in OMDoc: Translation
and Applications. J. Autom. Reasoning, 50(2): 191–202, 2013.
11. J. Urban, S. Trac, G. Sutcliffe, and Y. Puzis. Combining Mizar and TPTP Semantic Presentation
and Verification Tools. Studies in Logic, Grammar and Rhetoric, 18(31):121–136, 2009.
12. J. Urban and G. Sutcliffe. ATP-based Cross-verification of Mizar Proofs: Method, Systems, and First
Experiments. Mathematics in Computer Science, 2(2):231–251, 2008.
13. J. Urban. MPTP 0.2: Design, Implementation, and Initial Experiments. J. Autom. Reasoning,37(1-2):21–43, 2006.
14. J. Urban. MoMM - Fast Interreduction and Retrieval in Large Libraries of Formalized Mathematics.
International Journal on Artificial Intelligence Tools, 15(1):109–130, 2006.
15. J. Urban. MizarMode - an Integrated Proof Assistance Tool for the Mizar Way of Formalizing
Mathematics. Journal of Applied Logic, 4(4):414–427, 2006.
16. J. Urban. MPTP - motivation, implementation, first experiments. Journal of Automated Reasoning,33(3-4):319–339, 2004.
17. J. Urban. Free Order Sorted Universal Algebra, Formalized Mathematics, 10(3):211–225, 2002
18. J. Urban. Order Sorted Quotient Algebra, Formalized Mathematics, 10(3):201–210, 2002
19. J. Urban. Homomorphisms of Order Sorted Algebras, Formalized Mathematics, 10(3):197–200, 2002
20. J. Urban. Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras, Formalized Mathematics,
10(3):189–196, 2002
21. J. Urban. Order Sorted Algebras, Formalized Mathematics, 10(3):179–188, 2002
22. J. Urban. Mahlo and Inaccessible Cardinals, Formalized Mathematics, 9(3):485–489, 2001
23. J. Urban. Basic Facts about Inaccessible and Measurable Cardinals, Formalized Mathematics,
8(2):323–329, 2001
Chapters in Collective Volumes as Main Author
1. J. R. Harrison, J. Urban, F. Wiedijk. Interactive Theorem Proving. In D. M. Gabbay, J. Siekmann,
J. Woods, Handbook of the History of Logic, Volume 9: Computational Logic, Elsevier, 2014 (in press).
2. J. Urban, J. Vyskočil. Theorem Proving in Large Formal Mathematics as an Emerging AI Field.
Automated Reasoning and Mathematics: Essays in Memory of William McCune, LNAI 7788:240-257,
Springer 2013.
3. J. Urban, J. Vyskočil, P. Štěpánek. Automatické uvažovánı́ (Automated Reasoning). In V. Mařı́k, J.
Lažanský, O. Štěpánková, Umělá inteligence 6 (Artificial Intelligence 6), Academia, Prague, 2013.
Selected Other Publications:
1. C. Kaliszyk, K. Pak, J. Urban: Towards a Mizar environment for Isabelle: foundations and language.
CPP 2016, ACM, 58–65, 2016
2. C. Kaliszyk, S. Schulz, J. Urban, J. Vyskocil. System Description: E.T. 0.1. CADE 2015, LNCS
9195:389–398, 2015.
3. C. Kaliszyk, J. Urban, J. Vyskocil. Certified Connection Tableaux Proofs for HOL Light and TPTP.
CPP 2015, ACM, 59–66, 2015.
4. C. Kaliszyk, J. Urban, J. Vyskocil. Efficient Semantic Features for Automated Reasoning over Large
Theories. IJCAI 2015, AAAI Press 2015, 3084–3090, 2015.
5. C. Kaliszyk, J. Urban, J. Vyskocil. Lemmatization for Stronger Reasoning in Large Theories. FroCoS
2015, LNCS 9322, 341–356, 2015.
6. C. Kaliszyk, J. Urban, J. Vyskocil. Learning to Parse on Aligned Corpora (Rough Diamond). ITPPage 2 of 8

UrbanCV

2015, LNCS 9236, 227–233, 2015.
7. C. Kaliszyk, J. Urban. FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover. LPAR
2015, LNCS 9450, 88–96, 2015.
8. G. Bancerek, C. Bylinski, A. Grabowski, A. Kornilowicz, R. Matuszewski, A. Naumowicz, K. Pak, J.
Urban. Mizar: State-of-the-art and Beyond. CICM 2015, LNCS 9150, 261–279, 2015.
9. C. Kaliszyk, J. Urban, U. Siddique, S. Khan Afshar, C. Dunchev, S. Tahar. Formalizing Physics:
Automation, Presentation and Foundation Issues. CICM 2015, LNCS 9150, 288–295, 2015.
10. J. Urban. BliStr: The Blind Strategymaker. GCAI 2015: EPiC Series 36, 312–319, 2015.
11. C. Kaliszyk, J. Urban, J. Vyskocil, H. Geuvers. Developing Corpus-Based Translation Methods
between Informal and Formal Mathematics: Project Description. CICM 2014, LNCS 8543, 435–439,
2014.
12. C. Kaliszyk, L. Mamane, J. Urban. Machine Learning of Coq Proof Guidance: First Experiments.
SCSS 2014, EPiC Series 30, 27–34, 2014.
13. S. Joosten, C. Kaliszyk, J. Urban. Initial Experiments with TPTP-style Automated Theorem Provers
on ACL2 Problems. ACL2 2014, EPTCS 152, 77–85, 2014.
14. C. Kaliszyk, J. Urban, J. Vyskocil. Machine Learner for Automated Reasoning 0.4 and 0.5. PAAR
2014: EPiC Series 31, 60–66, 2014.
15. J. Urban. Parallelizing Mizar. Trends in Contemporary Computer Science, Podlasie 2014: Bialystok
University of Technology Publishing Office, 109–123, 2014.
16. D. Kühlwein, J. C. Blanchette, C. Kaliszyk, J. Urban. MaSh: Machine Learning for Sledgehammer.
ITP 2013, LNCS 7998, 35–50, 2013.
17. C. Tankink, C. Kaliszyk, J. Urban, H. Geuvers. Communicating Formal Proofs: The Case of Flyspeck.
ITP 2013, LNCS 7998, 451–456, 2013.
18. C. Kaliszyk, J. Urban. Lemma Mining over HOL Light . LPAR 2013, LNCS 8312:503–517, 2013.
19. C. Kaliszyk, J. Urban. PRocH: Proof Reconstruction for HOL Light. CADE 2013, LNCS 7898:267–
274, 2013.
20. D. Kühlwein, S. Schulz, J. Urban. E-MaLeS 1.1. CADE 2013, LNCS 7898:407–413, 2013.
21. C. Kaliszyk, J. Urban. Automated Reasoning Service for HOL Light. CICM 2013, LNCS 7961:120–
135, 2013.
22. C. Kaliszyk, J. Urban: Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE 2013: EPiC Series 14, 87–95, 2013.
23. C. Tankink, C. Kaliszyk, Josef Urban, H. Geuvers: Formal Mathematics on Display: A Wiki for
Flyspeck. MKM/Calculemus/DML 2013, LNCS 7961: 152–167, 2013.
24. D. Kühlwein, T. van Laarhoven, E. Tsivtsivadze, J. Urban, T. Heskes. Overview and Evaluation ofPremise Selection Techniques for Large-Theory Mathematics. IJCAR 2012, LNCS 7364:378–392, 2012.
25. J. Alama, D. Kühlwein, J. Urban. Automated and Human Proofs in General Mathematics: An Initial
Comparison. LPAR 2012, LNCS 7180: 37–45, 2012.
26. J. Alama, L. Mamane, J. Urban. Dependencies in Formal Mathematics: Applications and Extraction
for Coq and Mizar. CICM 2012, LNCS 7362: 1–16, 2012.
27. C. Tankink, C. Lange, J. Urban. Point-and-Write - Documenting Formal Mathematics by Reference.
CICM 2012, LNCS 7362: 169–185, 2012.
28. C. Kaliszyk, J. Urban. Initial Experiments with External Provers and Premise Selection on HOL
Light Corpora. PAAR@IJCAR 2012: EPiC Series 21:72–81, 2012.
29. D. Kuehlwein, J. Urban. Learning from Multiple Proofs: First Experiments. PAAR@IJCAR 2012:
EPiC Series 21:82–94, 2012.
30. J. Urban, J. Vyskočil, and P. Štěpánek. MaLeCoP: Machine Learning Connection Prover. TABLEAUX
2011, LNCS 6793: 263–277, 2011.
31. J. Urban An Overview of Methods for Large-Theory Automated Theorem Proving (Invited Paper).
ATE 2011, CEUR 760: 3–8. 2011.
Page 3 of 8

UrbanCV

32. E. Tsivtsivadze, J. Urban, H. Geuvers, T. Heskes. Semantic Graph Kernels for Automated Reasoning.
SDM 2011: 795–803, SIAM / Omnipress, 2011.
33. J. Urban, Content-based encoding of mathematical and code libraries. MathWikis 2011, CEUR 767:
49–53, 2011.
34. D. Kuehlwein, J. Urban, E. Tsivtsivadze, H. Geuvers, and T. Heskes. Multi-Output Ranking for
Automated Reasoning. KDIR 2011.
35. D. Kuehlwein, J. Urban, E. Tsivtsivadze, H. Geuvers, T. Heskes. Learning2Reason. Calculemus/MKM
2011, LNCS 6824: 298–300, 2011.
36. J. Alama, K. Brink, L. Mamane and J. Urban. Large Formal Wikis: Issues and Solutions, Calculemus/MKM 2011, LNCS 6824: 133–148, 2011.
37. J. Alama, M. Kohlhase, L. Mamane, A. Naumowicz, P. Rudnicki, J. Urban. Licensing the Mizar
Mathematical Library, Calculemus/MKM 2011, LNCS 6824: 149–163, 2011.
38. J. Urban, K. Hoder, and A. Voronkov. Evaluation of Automated Theorem Proving on the Mizar
Mathematical Library. ICMS 2010, LNCS 6327: 155–166, 2010.
39. J. Urban, J. Alama, P. Rudnicki, and H. Geuvers. A Wiki for Mizar: Motivation, Considerations, andInitial Prototype. MKM 2010: LNCS 6167: 455-469, 201040. J. Vyskočil, D. Stanovský, and J. Urban. Automated Proof Compression by Invention of New Definitions. LPAR 2010, LNAI 6355:447-462, 2010.
41. J. Urban and G. Sutcliffe. Automated Reasoning and Presentation Support for Formalizing Mathematics in Mizar. AISC 2010, LNCS 6167: 132–146, 2010.
42. J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskocil. MaLARea SG1 - Machine Learner for AutomatedReasoning with Semantic Guidance. IJCAR 2008, LNCS 5195: 441–456, 2008.
43. J. Urban. Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange.
LPAR Workshops 2008, CEUR 418: 1–16. 2008.
44. J. Urban and G. Sutcliffe. ATP Cross-verification of the Mizar MPTP Challenge problems. LPAR
2007, LNCS 4790: 546–560, 2007.
45. J. Urban. MaLARea: a Metasystem for Automated Reasoning in Large Theories. ESARLT 2007,
CEUR 257: 45–58. 2007.
46. J. Urban. XML-izing Mizar: making semantic processing and presentation of MML easy. MKM 2005,
LNAI 3863: 346–360. 2006.
47. J. Urban and G. Bancerek. Presenting and Explaining Mizar. UITP 2006, ENTCS 174: 63–74, 2007.
48. G. Bancerek and J. Urban. Integrated semantic browsing of the Mizar Mathematical Library for
authoring Mizar articles. MKM 2004, LNCS 3119: 44–57. 2004.
49. J. Urban MPTP 0.1: System Description. FTP 2013, ENTCS 86(1): 147–152. 2003.
50. J. Urban. Translating Mizar for first order theorem provers. MKM 2003, LNCS 2594: 203–215. 2003.
Edited Volumes
1. J. R. Harrison, J. Urban and F. Wiedijk, editors. Special Issue of the Journal of Formalized Reasoning
on Twenty Years of the QED Manifesto, Volume 9, Number 1, 2016.
2. Stephen Watt, James H. Davenport, Alan Sexton, Peter Sojka and Josef Urban, editors. Intelligent
Computer Mathematics (MKM, Calculemus, DML, and Systems and Projects 2014, Coimbra, Portugal,
July 7-11, 2014). Lecture Notes in Computer Science 8543, Springer 2014.
3. Matthew England, James H. Davenport, Andrea Kohlhase, Michael Kohlhase, Paul Libbrecht, Walther
Neuper, Pedro Quaresma, Alan P. Sexton, Petr Sojka, Josef Urban, Stephen M. Watt (Eds.). Joint
Proceedings of the MathUI, OpenMath and ThEdu Workshops and Work in Progress track at CICM,
co-located with Conferences on Intelligent Computer Mathematics (CICM 2014), Coimbra, Portugal,
July 7-11, 2014. CEUR Workshop Proceedings 1186, CEUR-WS.org 2014.
4. Jasmin Blanchette and Josef Urban, editors. PxTP 2013 - Third International Workshop on Proof
Exchange for Theorem Proving. Lake Placid, USA, June 2013. EasyChair Proceedings in Computing,
Page 4 of 8

UrbanCV

Vol 14, ISSN 2040-557X, EasyChair 2013.
5. James H. Davenport, William M. Farmer, Josef Urban and Florian Rabe, editors. Intelligent Computer
Mathematics (18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011,
Bertinoro, Italy, July 18-23, 2011). Lecture Notes in Computer Science 6824, Springer 2011.
6. Conference on Intelligent Computer Mathematics Work-in-Progress Papers Proceedings A. Asperti,
J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, editors. Technical Report UBLCS-2011-04,
University of Bologna, 2011.
7. Christoph Lange and Josef Urban, editors. Proceedings of the ITP 2011 Workshop on MathematicalWikis, CEUR WS, Vol 767, ISSN 1613-0073.
8. Josef Urban, Stephan Schulz, and Geoff Sutcliffe, editors. Proceedings of the CADE-21 Workshop on
Empirically Successful Automated Reasoning in Large Theories, CEUR WS, Vol 257, ISSN 1613-0073.
Invited talks:
1. Learning Reasoning and Understanding in Mathematics, Semantic Representation of Mathematical
Knowledge, Fields Institute, Toronto, 3-5/02/2016
2. Learning Intelligent Theorem Proving from Large Formal Corpora, International Symposium on Artificial Intelligence and Mathematics (ISAIM’16), Fort Laudardale, 4-6/01/2016
3. Computer-Understandable Mathematics: Is It Coming?, 53rd Summer School on General Algebra andOrdered Sets, Srnı́, Czech Republic, 29/08-4/09, 2015.
4. Inductive and Deductive AI over Large Formal Libraries, Formalization of Mathematics in Proof Assistants, Institut Henri Poincaré, Paris, France, 5-9/05/2014
5. AI over Large Formal Knowledge Bases: The First Decade, ARW’2013, Dundee, UK, 11-12/04/2013
6. Theorem Proving over Mizar, Flyspeck and Isabelle, ADAM’2013, Albuquerque, USA, 6-8/06/2013
7. AI via/for Large Mathematical Knowledge Bases Dagstuhl Seminar 12271: AI meets Formal Software
Development, Leibniz Center for Informatics, Dagstuhl, Germany, 1-6/07/2012
8. An Overview of Methods for Large-Theory Automated Theory Proving, CADE23 Workshop on Automated Theory Engineering, Wroclaw, Poland, 31/07/2011
9. Large Formal Libraries: Birthplace of Strong AI?, Deduction Seminar: Deduction at Scale, Max-Planck
Institute for Informatics, Germany, 7-11/03/2011
10. Automated Reasoning over the Mizar Library, AMS Special Session on Formal Math. for Mathematicians: Developing Large Repositories of Advanced Mathematics, New Orleans, USA, 6-9/01/2011
11. Automation and AI Tools for Mizar, Symposium and General Assembly of Mizar Japan,Tokyo, 06/09/2010
12. AI Methods in Automated Reasoning, ISLA 2010, Hyderabad, India, 25-28/01/2010
13. Automated Reasoning for Mizar: AI through Knowledge Exchange, KEAPPA and IWIL, Qatar, 22/10/2008.
14. Accessing Mizar and its Semantics on the Web, ICMS’2006, Castro Urdiales, Spain, 1-3/09/2006.
Prizes and awards:
1. LTB, HOL and MZR category of the CASC competition at the 2013 CADE Conference: 1st place ofthe MaLARea system
2. MZR category of the CASC competition at the 2012 Turing Centenary Conference (Manchester): mostproblems solved ans 2nd place by the MaLARea system (£1000), 3rd place of the PS-E system (£500).
3. FOF category of the same competition: 2nd place of the E-MaLeS system. (£1000)
4. FOF category of the CASC competition at IJCAR 2012: 2nd place of the E-MaLeS system.
5. FOF category of the 2011 CASC competition in Wroclaw: 3rd place of the E-MaLeS system
6. MZR category of the 2008 CASC competition in Sydney: 1st place of the MaLARea system
7. The Annual SUMO Reasoning Prizes at CASC (2008): 2nd place of the MaLARea system ($1000)
Selected Service Activities:• Journal editorial boards: Formalized Mathematics (since 2006), Central European J. of Computer

Page 5 of 8

UrbanCV

Science (since 2010)• Special issue journal editing: Journal of Formalized Reasoning• Journal reviewer: Mathematical Reviews (since 2016)• Other journals reviewed for: J. of Automated Reasoning, Communication of ACM, International J. on
Artificial Intelligence Tools, Logical Methods in Computer Science, J. of Logic and Computation, AI
Communications, J. of Applied Logic, Mathematics in Computer Science, J. of Symbolic Computation• Graduate students: K. Hoder (MS), O. Kuncar (MS/PhD), Daniel Kuehlwein (PhD), Vl. Sisma (PhD),
W. Geraedts (MS), M. Adams (PhD)• Member of the Assembly of the Czech Institute of Informatics, Robotics, and Cybernetics (since 2016)• Professional Societies: Association for Automated Reasoning, Association of Mizar Users (Head of theLicensing Committee), Mathematical Knowledge Management Interest Group (Trustee for years 20132016), Association for Computing Machinery’s Special Interest Group on Programming Languages.
Teaching: (Charles University in Prague, Radboud University Nijmegen, Czech Technical University)• Lectures: Automated Reasoning and Theorem Proving, Formalization and Verification of Mathematics• Exercises: Propositional and Predicate Logic, Non-procedural Programming, Analyses of Algorithms• Seminars: Automated Theorem Proving, Automated Reasoning Seminar
Program Committees:
1. Artificial Intelligence and Theorem Proving, Obergurgl, 2016, PC co-chair
2. Practical Aspects of Automated Reasoning, Coimbra, 2016, PC co-chair
3. International Joint Conference on Automated Reasoning, Coimbra, 2016, PC member
4. Conferences on Intelligent Computer Mathematics, Bialystok, 2016, PC member
5. First International Workshop on Hammers for Type Theories, Coimbra, 2016, PC member
6. International Workshop on the Implementation of Logics, Suva, 2015, PC member
7. Conferences on Intelligent Computer Mathematics, Washington DC, 2015, PC member
8. Proof Exchange for Theorem Provers, Berlin, 2015, PC member
9. Formal Mathematics for Mathematicians, Washington DC, 2015, PC member
10. 22nd Workshop on Logic, Language, Information and Computation, 2015, Bloomington, USA, PC
member
11. 2nd International Workshop about Sets and Tools, 2015, Oslo, Norway, PC member
12. Mathematical Knowledge Management, Coimbra, Portugal, 2014, PC chair
13. Twenty Years of the QED Manifesto, Vienna, 2014, PC co-chair
14. Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, 2014, PC
member
15. 3rd International Workshop on Semantic Web Collaborative Spaces, Trentino, Italy, 2014, PC member
16. International Symposium on Frontiers of Combining Systems, Nancy, 2013, PC member
17. Conferences on Intelligent Computer Mathematics, Bath, 2013, PC member
18. Proof Exchange for Theorem Provers, Lake Placid, 2013, PC co-chair
19. Knowledge Intensive Automated Reasoning, Lake Placid, 2013, PC member
20. Semantic Web Collaborative Spaces, Montpellier, 2013, PC member
21. Conferences on Intelligent Computer Mathematics, Bremen, 2012, PC member
22. User Interfaces for Theorem Provers, Bremen, 2012, PC member
23. Automated Theory eXploration, Manchester, 2012, PC member
24. Semantic Web Collaborative Spaces, Lyon, 2012, PC member
25. Conferences on Intelligent Computer Mathematics, Bertinoro, 2011, PC Chair of the Systems track
26. The ITP 2011 Workshop on Mathematical Wikis, Nijmegen, 2011, PC co-chair
27. Practical Aspects of Automated Reasoning, Edinburgh, 2010, PC member
28. Workshop on Mathematically Intelligent Proof Search, Paris, 2010, PC member

Page 6 of 8

UrbanCV

29. Mathematical Knowledge Management, Grand Bend, 2009, PC member
30. Knowledge Exchange: Automated Provers and Proof Assistants, Qatar, 2008, PC member
31. Practical Aspects of Automated Reasoning, Sydney, 2008, PC member
32. Empirically Successful Automated Reasoning for Mathematics, Birmingham, 2008, PC member
33. Programming Languages for Mechanized Mathematics, 2008, Birmingham, PC member
34. Empirically Successful Automated Reasoning in Large Theories, Bremen, 2007, PC co-chair
35. Programming Languages for Mechanized Mathematics, Hagenberg, 2007, PC member
Other academic and educational activities:• Founded the ATP and ITP courses and seminar at Charles Univ. in Prague. Co-founded (with
P. Stepanek) the Prague Automated Reasoning Group.1 The group members and alumni include:
J. Vyskocil (CTU), J. Jakubuv (Heriot-Watt, CTU), M. Suda (MPI Saarbrucken, U. Manchester), P.
Pudlak (CTU, Google), M. Janota (UC Dublin, INESC-ID Lisboa), K. Hoder (U. Manchester, Google),
O. Kuncar (TU Munich), D. Stanovsky (Charles U.).
Languages:
Czech (native), English (fluent), Polish (fluent), German (advanced), Russian (advanced), French (intermed.)
Selected Projects Implemented:• Machine Learner for Automated Reasoning: (MaLARea) combining deductive ATP and counterexample finding with machine learning in a closed loop. The strongest existing meta-system for automated reasoning with large amount of previous proof knowledge.
• HOL(y) Hammer: (with C. Kaliszyk) AI/ATP system proving conjectures over the Flyspeck corpus
by a number of inductive/deductive methods. The system uses 14 complementary learning/deductive
strategies in parallel to prove (as of April 2013) 47% of the Flyspeck theorems and lemmas fully
automatically.
• Blind Strategymaker: (BliStr) evolves new ATP strategies for classes of similar problems by interleaving fast low-time strategy iterative evolution steps with high-time strategy evaluation and reclassification steps. 30 hours of such evolution improved the E prover by 25% on the Mizar problems.
• MPTP: Mizar Problems for Theorem Proving. Project bringing the largest formal mathematicallibrary to the world of automated reasoning and related AI methods. Translation of Mizar logic andlibrary to first-order ATP formats, preserving completeness and correctness, and providing consistentnamespaces for symbols and theorems. That in turn allows machine learning from the proofs in thewhole library, and makes research in combined ATP/AI metasystems like MaLARea possible.
• MizAR: parallelized AI/ATP, verification, and presentation service for Mizar2 . Provides: article
verification, linked HTML presentation, AI/ATP solving and explanation of Mizar problems, lemmasuggestion. Proves (as of September 2013) 40% of the Mizar theorems and lemmas fully automatically.
• MPTP Challenge: Design and implementation (with G. Sutcliffe) of the first large-theory AI/ATP
benchmark3 . This gave rise to the Large Theory Batch division of the annual CASC ATP competition.
• Mizar, HOL Light, and Isabelle proof advisors: Used machine learning on the tens of thousandsof proofs in the large Mizar Mathematical Library to train a lemma-selection advisor. Similar work forHales’ proof of Jordan theorem in HOL, and for Isabelle (experimental). Combining the advisors with
ATP systems to provide strong methods for reasoning over large complex theories.
• Machine Learning Connection Prover: (MaLeCoP - with Jiri Vyskocil) A connection tableaux
prover using machine learning from a large body of solved problems and successful proof decisions toguide the internal ATP proof search process.
1

http://arg.ciirc.cvut.cz/
http://mizar.cs.ualberta.ca/~mptp/MizAR.html
3
http://www.tptp.org/MPTPChallenge/
2

Page 7 of 8

UrbanCV• MoMM: System using ATP indexing methods for fast interreduction of ca. one million mathematical
propositions, and for real-time retrieval of relevant information from that knowledge base. Integration
into the Emacs authoring environment for Mizar, its use for real-time searching of the Mizar library.
• Formal mathematical wiki for Coq and Mizar: Wikis for collaborative editing, verification,versioning, and web-presentation of computer-verified mathematics. Ongoing NWO-funded project.4• E-MaLeS: Machine Learning of Strategies for E prover (with D. Kuhlwein and E. Tsivtsivadze). Usingmachine learning methods to find optimal strategies for the E ATP system. Ongoing project.
• MizarMode: Authoring environment for Mizar, used by the majority of Mizar authors. Integrates
number of proof assistance methods, searching and presentation tools, AI and ATP advisors.
• XML-ization of Mizar: XML-based re-implementation of Mizar internal format and datastructures.
Used by a number of projects to understand and link with Mizar.
• Otter2Mizar: Tool automatically translating the Otter and Prover9 proofs into Mizar. This allows
import of ATP proofs back to Mizar and their Mizar verification.
• Formalization of the theory of order sorted algebras: Developed order sorted algebras, theirsubalgebras, homomorphisms, quotient and free (term) algebras in Mizar.
• Formalization of the theory of large cardinals: Formal Mizar development including proofs thatmeasurable and Mahlo cardinals are inaccessible, and that inaccessible cardinals give a model of ZF.

4

http://mws.cs.ru.nl/mwiki/, http://mws.cs.ru.nl/cwiki/, www.fnds.cs.ru.nl/fndswiki/Research/MathWiki

Page 8 of 8