Edit Profile (opens in new tab) Urban, Josef Co-Author Distance Author ID: urban.josef Published as: Urban, Josef Videos: carmin.tv Documents Indexed: 89 Publications since 2003 7 Contributions as Editor Co-Authors: 87 Co-Authors with 90 Joint Publications 1,349 Co-Co-Authors all top 5 Co-Authors 6 single-authored 33 Kaliszyk, Cezary 13 Jakubův, Jan 9 Vyskočil, Jiří 8 Kühlwein, Daniel 8 Olšák, Miroslav 8 Sutcliffe, Geoff 7 Geuvers, Jan Herman 6 Alama, Jesse 5 Schulz, Stephan 4 Bancerek, Grzegorz 4 Brown, Chad Edward 4 Chvalovský, Karel 4 Davenport, James Harold 4 Gauthier, Thibault 4 Goertzel, Zarathustra Amadeus 4 Heskes, Tom M. 4 Piotrowski, Bartosz 3 Blaauwbroek, Lasse 3 Blanchette, Jasmin Christian 3 Mamane, Lionel Elie 3 Naumowicz, Adam 3 Rudnicki, Piotr 3 Tankink, Carst 3 Tsivtsivadze, Evgeni 3 Wiedijk, Freek 3 Zombori, Zsolt 2 Färber, Michael 2 Kohlhase, Michael 2 Labahn, George 2 Pease, Adam 2 Piepenbrock, Jelle 2 Rabe, Florian 2 Suda, Martin 2 Zhang, Liao 1 Adams, Mark 1 Bauer, Gertrud 1 Brink, Kasper 1 Byliński, Czesław 1 Černỳ, Prokop 1 Csiszárik, Adrián 1 Dang, Tat Dat 1 Dunchev, Cvetan 1 Farmer, William M. 1 Fontaine, Pascal 1 Grabowski, Adam 1 Greenaway, David 1 Hales, Thomas Callister 1 Hoàng Lê Trường 1 Hoder, Kryštof 1 Iancu, Mihnea 1 Janota, Mikoláš 1 Kauers, Manuel 1 Khan Afshar, Sanaz 1 Korniłowicz, Artur 1 Kumar, Ramana 1 Lange, Christoph 1 Macke, Jaroslav 1 Magron, Victor 1 Matuszewski, Roman 1 McLaughlin, Sean 1 Michalewski, Henryk 1 Nguyen, Quang Truong 1 Nguyen, Tat Thang 1 Nipkow, Tobias 1 Norrish, Michael 1 Obua, Steven 1 Pąk, Karol 1 Paulson, Lawrence Charles 1 Pleso, Joseph 1 Pudlák, Pavel 1 Ramanayake, Revantha 1 Sedlář, Jiří 1 Sexton, Alan P. 1 Siddique, Umair 1 Sivic, Josef 1 Sojka, Petr 1 Solovyev, Alexey 1 Stanovský, David 1 Tạ Thị Hoài An 1 Tahar, Sofiène 1 Tran, Nam Trung 1 Trieu, Thi Diep 1 van Laarhoven, Twan 1 Voronkov, Andrei 1 Wang, Qingxiang 1 Watt, Stephen Michael 1 Zumkeller, Roland all top 5 Serials 12 Journal of Automated Reasoning 4 Lecture Notes in Computer Science 3 AI Communications 3 Mathematics in Computer Science 2 Journal of Formalized Reasoning 1 Journal of Symbolic Computation 1 International Journal of Approximate Reasoning 1 Nieuw Archief voor Wiskunde. Vijfde Serie 1 Journal of Applied Logic 1 Forum of Mathematics, Pi all top 5 Fields 95 Computer science (68-XX) 7 General and overarching topics; collections (00-XX) 5 Mathematical logic and foundations (03-XX) 2 History and biography (01-XX) 2 Convex and discrete geometry (52-XX) 2 Numerical analysis (65-XX) 1 Number theory (11-XX) 1 Group theory and generalizations (20-XX) 1 Optics, electromagnetic theory (78-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 79 Publications have been cited 1,045 times in 420 Documents Cited by ▼ Year ▼ Mizar: state-of-the-art and beyond. Zbl 1417.68201 Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef 156 2015 A formal proof of the Kepler conjecture. Zbl 1379.52018 Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 58 2017 MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095 Urban, Josef 45 2006 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217 Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 39 2014 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283 Kaliszyk, Cezary; Urban, Josef 38 2014 Hammering towards QED. Zbl 1451.68318 Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 38 2016 ATP and presentation service for Mizar formalizations. Zbl 1260.68380 Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 36 2013 MizAR 40 for Mizar 40. Zbl 1356.68191 Kaliszyk, Cezary; Urban, Josef 35 2015 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177 Kaliszyk, Cezary; Urban, Josef 34 2015 MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434 Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří 30 2008 MPTP-motivation, implementation, first experiments. Zbl 1075.68081 Urban, Josef 23 2004 XML-izing Mizar: Making semantic processing and presentation of MML easy. Zbl 1151.68681 Urban, Josef 23 2006 MaLeCoP. Machine learning connection prover. Zbl 1332.68206 Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr 20 2011 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375 Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 19 2013 ENIGMA: efficient learning-based inference guiding machine. Zbl 1367.68249 Jakubův, Jan; Urban, Josef 18 2017 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290 Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. Zbl 1535.68449 Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef 17 2019 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149 Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 17 2016 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312 Kaliszyk, Cezary; Urban, Josef 17 2015 MaSh: machine learning for Sledgehammer. Zbl 1317.68215 Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 16 2013 Overview and evaluation of premise selection techniques for large theory mathematics. Zbl 1358.68259 Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom 13 2012 History of interactive theorem proving. Zbl 1404.03010 Harrison, John; Urban, Josef; Wiedijk, Freek 13 2014 ENIGMA anonymous: symbol-independent inference guiding machine (system description). Zbl 07614690 Jakubův, Jan; Chvalovský, Karel; Olšák, Miroslav; Piotrowski, Bartosz; Suda, Martin; Urban, Josef 13 2020 Translating Mizar for first order theorem provers. Zbl 1022.68622 Urban, Josef 12 2003 TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224 Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef 12 2017 MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103 Urban, Josef 12 2006 Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. Zbl 1108.68583 Bancerek, Grzegorz; Urban, Josef 11 2004 Large formal wikis: issues and solutions. Zbl 1335.68220 Alama, Jesse; Brink, Kasper; Mamane, Lionel; Urban, Josef 10 2011 Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128 Urban, Josef; Hoder, Krystof; Voronkov, Andrei 10 2010 Automated and human proofs in general mathematics: an initial comparison. Zbl 1352.68211 Alama, Jesse; Kühlwein, Daniel; Urban, Josef 9 2012 ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Zbl 1178.68532 Urban, Josef; Sutcliffe, Geoff 9 2008 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220 Kaliszyk, Cezary; Urban, Josef 9 2015 Property invariant embedding for automated reasoning. Zbl 1464.68317 Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef 9 2020 TacticToe: learning to prove with tactics. Zbl 07356973 Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael 9 2021 Dependencies in formal mathematics: applications and extraction for Coq and Mizar. Zbl 1335.68221 Alama, Jesse; Mamane, Lionel; Urban, Josef 8 2012 Automated reasoning and presentation support for formalizing mathematics in MizAR. Zbl 1286.68403 Urban, Josef; Sutcliffe, Geoff 8 2010 A Wiki for Mizar: motivation, considerations, and initial prototype. Zbl 1286.68434 Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman 8 2010 Theorem proving in large formal mathematics as an emerging AI field. Zbl 1276.68139 Urban, Josef; Vyskočil, Jiří 8 2013 Enhancing ENIGMA given clause guidance. Zbl 1417.68184 Jakubův, Jan; Urban, Josef 8 2018 The Tactician. A seamless, interactive tactic learner and prover for Coq. Zbl 1455.68242 Blaauwbroek, Lasse; Urban, Josef; Geuvers, Herman 8 2020 Hierarchical invention of theorem proving strategies. Zbl 1462.68213 Jakubův, Jan; Urban, Josef 8 2018 PRocH: proof reconstruction for HOL Light. Zbl 1381.68271 Kaliszyk, Cezary; Urban, Josef 7 2013 Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751 Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 7 2013 Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman 7 2014 Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Zbl 1293.68035 7 2014 GRUNGE: a grand unified ATP challenge. Zbl 1535.68447 Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 7 2019 Prolog technology reinforcement learning prover (system description). Zbl 07614694 Zombori, Zsolt; Urban, Josef; Brown, Chad E. 7 2020 Automated proof compression by invention of new definitions. Zbl 1253.68293 Vyskočil, Jiří; Stanovský, David; Urban, Josef 6 2010 Monte Carlo tableau proof search. Zbl 1494.68286 Färber, Michael; Kaliszyk, Cezary; Urban, Josef 6 2017 ATPboost: learning premise selection in binary setting with ATP feedback. Zbl 1511.68257 Piotrowski, Bartosz; Urban, Josef 6 2018 Lemma mining over HOL Light. Zbl 1407.68437 Kaliszyk, Cezary; Urban, Josef 5 2013 ENIGMAWatch: ProofWatch meets ENIGMA. Zbl 1435.68370 Goertzel, Zarathustra; Jakubův, Jan; Urban, Josef 5 2019 Lemmatization for stronger reasoning in large theories. Zbl 1471.68313 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 5 2015 Detecting inconsistencies in large first-order knowledge bases. Zbl 1494.68262 Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam 5 2017 System description: E.T. 0.1. Zbl 1465.68286 Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 5 2015 E-MaLeS 1.1. Zbl 1381.68273 Kühlwein, Daniel; Schulz, Stephan; Urban, Josef 4 2013 Automated reasoning service for HOL Light. Zbl 1390.68576 Kaliszyk, Cezary; Urban, Josef 4 2013 Hammering Mizar by learning clause guidance (short paper). Zbl 07649983 Jakubuv, Jan; Urban, Josef 4 2019 MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193 Kühlwein, Daniel; Urban, Josef 4 2015 ProofWatch: watchlist guidance for large theories in E. Zbl 1435.68369 Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef 4 2018 Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 4 2017 First neural conjecturing datasets and experiments. Zbl 1455.68261 Urban, Josef; Jakubův, Jan 4 2020 Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 3 2015 Machine learning guidance for connection tableaux. Zbl 07356974 Färber, Michael; Kaliszyk, Cezary; Urban, Josef 3 2021 Presenting and explaining Mizar. Zbl 1278.68283 Urban, Josef; Bancerek, Grzegorz 2 2007 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232 Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2 2013 Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Zbl 1218.68014 2 2011 Extending E prover with similarity based clause selection strategies. Zbl 1347.68303 Jakubův, Jan; Urban, Josef 2 2016 First experiments with neural translation of informal to formal mathematics. Zbl 1417.68195 Wang, Qingxiang; Kaliszyk, Cezary; Urban, Josef 2 2018 Guiding inferences in connection tableau by recurrent neural networks. Zbl 1455.68252 Piotrowski, Bartosz; Urban, Josef 2 2020 Alien coding. Zbl 1531.68164 Gauthier, Thibault; Olšák, Miroslav; Urban, Josef 2 2023 Online machine learning techniques for Coq: a comparison. Zbl 1485.68288 Zhang, Liao; Blaauwbroek, Lasse; Piotrowski, Bartosz; Černỳ, Prokop; Kaliszyk, Cezary; Urban, Josef 2 2021 The CADE-25 automated theorem proving system competition – CASC-25. Zbl 1373.68368 Sutcliffe, Geoff; Urban, Josef 1 2016 ATP cross-verification of the Mizar MPTP challenge problems. Zbl 1137.68576 Urban, Josef; Sutcliffe, Geoff 1 2007 Extracting higher-order goals from the Mizar Mathematical Library. Zbl 1344.68203 Brown, Chad E.; Urban, Josef 1 2016 System description: XSL-based translator of Mizar to LATEX. Zbl 1417.68202 Bancerek, Grzegorz; Naumowicz, Adam; Urban, Josef 1 2018 Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186 Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène 1 2015 Guiding an automated theorem prover with neural rewriting. Zbl 1512.68427 Piepenbrock, Jelle; Heskes, Tom; Janota, Mikoláš; Urban, Josef 1 2022 Towards finding longer proofs. Zbl 07532515 Zombori, Zsolt; Csiszárik, Adrián; Michalewski, Henryk; Kaliszyk, Cezary; Urban, Josef 1 2021 Alien coding. Zbl 1531.68164 Gauthier, Thibault; Olšák, Miroslav; Urban, Josef 2 2023 Guiding an automated theorem prover with neural rewriting. Zbl 1512.68427 Piepenbrock, Jelle; Heskes, Tom; Janota, Mikoláš; Urban, Josef 1 2022 TacticToe: learning to prove with tactics. Zbl 07356973 Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael 9 2021 Machine learning guidance for connection tableaux. Zbl 07356974 Färber, Michael; Kaliszyk, Cezary; Urban, Josef 3 2021 Online machine learning techniques for Coq: a comparison. Zbl 1485.68288 Zhang, Liao; Blaauwbroek, Lasse; Piotrowski, Bartosz; Černỳ, Prokop; Kaliszyk, Cezary; Urban, Josef 2 2021 Towards finding longer proofs. Zbl 07532515 Zombori, Zsolt; Csiszárik, Adrián; Michalewski, Henryk; Kaliszyk, Cezary; Urban, Josef 1 2021 ENIGMA anonymous: symbol-independent inference guiding machine (system description). Zbl 07614690 Jakubův, Jan; Chvalovský, Karel; Olšák, Miroslav; Piotrowski, Bartosz; Suda, Martin; Urban, Josef 13 2020 Property invariant embedding for automated reasoning. Zbl 1464.68317 Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef 9 2020 The Tactician. A seamless, interactive tactic learner and prover for Coq. Zbl 1455.68242 Blaauwbroek, Lasse; Urban, Josef; Geuvers, Herman 8 2020 Prolog technology reinforcement learning prover (system description). Zbl 07614694 Zombori, Zsolt; Urban, Josef; Brown, Chad E. 7 2020 First neural conjecturing datasets and experiments. Zbl 1455.68261 Urban, Josef; Jakubův, Jan 4 2020 Guiding inferences in connection tableau by recurrent neural networks. Zbl 1455.68252 Piotrowski, Bartosz; Urban, Josef 2 2020 ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. Zbl 1535.68449 Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef 17 2019 GRUNGE: a grand unified ATP challenge. Zbl 1535.68447 Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 7 2019 ENIGMAWatch: ProofWatch meets ENIGMA. Zbl 1435.68370 Goertzel, Zarathustra; Jakubův, Jan; Urban, Josef 5 2019 Hammering Mizar by learning clause guidance (short paper). Zbl 07649983 Jakubuv, Jan; Urban, Josef 4 2019 Enhancing ENIGMA given clause guidance. Zbl 1417.68184 Jakubův, Jan; Urban, Josef 8 2018 Hierarchical invention of theorem proving strategies. Zbl 1462.68213 Jakubův, Jan; Urban, Josef 8 2018 ATPboost: learning premise selection in binary setting with ATP feedback. Zbl 1511.68257 Piotrowski, Bartosz; Urban, Josef 6 2018 ProofWatch: watchlist guidance for large theories in E. Zbl 1435.68369 Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef 4 2018 First experiments with neural translation of informal to formal mathematics. Zbl 1417.68195 Wang, Qingxiang; Kaliszyk, Cezary; Urban, Josef 2 2018 System description: XSL-based translator of Mizar to LATEX. Zbl 1417.68202 Bancerek, Grzegorz; Naumowicz, Adam; Urban, Josef 1 2018 A formal proof of the Kepler conjecture. Zbl 1379.52018 Hales, Thomas; Adams, Mark; Bauer, Gertrud; Dang, Tat Dat; Harrison, John; Hoang Le Truong; Kaliszyk, Cezary; Magron, Victor; McLaughlin, Sean; Nguyen, Tat Thang; Nguyen, Quang Truong; Nipkow, Tobias; Obua, Steven; Pleso, Joseph; Rute, Jason; Solovyev, Alexey; Ta, Thi Hoai An; Tran, Nam Trung; Trieu, Thi Diep; Urban, Josef; Vu, Ky; Zumkeller, Roland 58 2017 ENIGMA: efficient learning-based inference guiding machine. Zbl 1367.68249 Jakubův, Jan; Urban, Josef 18 2017 TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224 Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef 12 2017 Monte Carlo tableau proof search. Zbl 1494.68286 Färber, Michael; Kaliszyk, Cezary; Urban, Josef 6 2017 Detecting inconsistencies in large first-order knowledge bases. Zbl 1494.68262 Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam 5 2017 Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 4 2017 Hammering towards QED. Zbl 1451.68318 Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 38 2016 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149 Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 17 2016 Extending E prover with similarity based clause selection strategies. Zbl 1347.68303 Jakubův, Jan; Urban, Josef 2 2016 The CADE-25 automated theorem proving system competition – CASC-25. Zbl 1373.68368 Sutcliffe, Geoff; Urban, Josef 1 2016 Extracting higher-order goals from the Mizar Mathematical Library. Zbl 1344.68203 Brown, Chad E.; Urban, Josef 1 2016 Mizar: state-of-the-art and beyond. Zbl 1417.68201 Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef 156 2015 MizAR 40 for Mizar 40. Zbl 1356.68191 Kaliszyk, Cezary; Urban, Josef 35 2015 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177 Kaliszyk, Cezary; Urban, Josef 34 2015 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312 Kaliszyk, Cezary; Urban, Josef 17 2015 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220 Kaliszyk, Cezary; Urban, Josef 9 2015 Lemmatization for stronger reasoning in large theories. Zbl 1471.68313 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 5 2015 System description: E.T. 0.1. Zbl 1465.68286 Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 5 2015 MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193 Kühlwein, Daniel; Urban, Josef 4 2015 Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 3 2015 Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186 Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène 1 2015 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217 Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 39 2014 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283 Kaliszyk, Cezary; Urban, Josef 38 2014 History of interactive theorem proving. Zbl 1404.03010 Harrison, John; Urban, Josef; Wiedijk, Freek 13 2014 Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172 Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman 7 2014 Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Zbl 1293.68035 7 2014 ATP and presentation service for Mizar formalizations. Zbl 1260.68380 Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 36 2013 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375 Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 19 2013 MaSh: machine learning for Sledgehammer. Zbl 1317.68215 Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 16 2013 Theorem proving in large formal mathematics as an emerging AI field. Zbl 1276.68139 Urban, Josef; Vyskočil, Jiří 8 2013 PRocH: proof reconstruction for HOL Light. Zbl 1381.68271 Kaliszyk, Cezary; Urban, Josef 7 2013 Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751 Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 7 2013 Lemma mining over HOL Light. Zbl 1407.68437 Kaliszyk, Cezary; Urban, Josef 5 2013 E-MaLeS 1.1. Zbl 1381.68273 Kühlwein, Daniel; Schulz, Stephan; Urban, Josef 4 2013 Automated reasoning service for HOL Light. Zbl 1390.68576 Kaliszyk, Cezary; Urban, Josef 4 2013 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232 Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2 2013 Overview and evaluation of premise selection techniques for large theory mathematics. Zbl 1358.68259 Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom 13 2012 Automated and human proofs in general mathematics: an initial comparison. Zbl 1352.68211 Alama, Jesse; Kühlwein, Daniel; Urban, Josef 9 2012 Dependencies in formal mathematics: applications and extraction for Coq and Mizar. Zbl 1335.68221 Alama, Jesse; Mamane, Lionel; Urban, Josef 8 2012 MaLeCoP. Machine learning connection prover. Zbl 1332.68206 Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr 20 2011 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290 Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 Large formal wikis: issues and solutions. Zbl 1335.68220 Alama, Jesse; Brink, Kasper; Mamane, Lionel; Urban, Josef 10 2011 Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Zbl 1218.68014 2 2011 Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128 Urban, Josef; Hoder, Krystof; Voronkov, Andrei 10 2010 Automated reasoning and presentation support for formalizing mathematics in MizAR. Zbl 1286.68403 Urban, Josef; Sutcliffe, Geoff 8 2010 A Wiki for Mizar: motivation, considerations, and initial prototype. Zbl 1286.68434 Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman 8 2010 Automated proof compression by invention of new definitions. Zbl 1253.68293 Vyskočil, Jiří; Stanovský, David; Urban, Josef 6 2010 MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434 Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří 30 2008 ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Zbl 1178.68532 Urban, Josef; Sutcliffe, Geoff 9 2008 Presenting and explaining Mizar. Zbl 1278.68283 Urban, Josef; Bancerek, Grzegorz 2 2007 ATP cross-verification of the Mizar MPTP challenge problems. Zbl 1137.68576 Urban, Josef; Sutcliffe, Geoff 1 2007 MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095 Urban, Josef 45 2006 XML-izing Mizar: Making semantic processing and presentation of MML easy. Zbl 1151.68681 Urban, Josef 23 2006 MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103 Urban, Josef 12 2006 MPTP-motivation, implementation, first experiments. Zbl 1075.68081 Urban, Josef 23 2004 Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. Zbl 1108.68583 Bancerek, Grzegorz; Urban, Josef 11 2004 Translating Mizar for first order theorem provers. Zbl 1022.68622 Urban, Josef 12 2003 all cited Publications top 5 cited Publications all top 5 Cited by 451 Authors 48 Urban, Josef 31 Kaliszyk, Cezary 23 Coghetto, Roland 21 Shidama, Yasunari 20 Grabowski, Adam 20 Pąk, Karol 19 Korniłowicz, Artur 16 Nakasho, Kazuhisa 14 Blanchette, Jasmin Christian 14 Kohlhase, Michael 13 Schwarzweller, Christoph 12 Endou, Noboru 12 Naumowicz, Adam 12 Rabe, Florian 11 Futa, Yuichi 11 Jakubův, Jan 10 Okazaki, Hiroyuki 9 Paulson, Lawrence Charles 9 Sutcliffe, Geoff 8 Vyskočil, Jiří 8 Watase, Yasushige 7 Bentkamp, Alexander 6 Alama, Jesse 6 Brown, Chad Edward 6 Gauthier, Thibault 6 Koch, Sebastian 6 Olšák, Miroslav 6 Suda, Martin 5 Benzmüller, Christoph Ewald 5 Mitsuishi, Takashi 5 Vukmirović, Petar 5 Yamazaki, Hiroshi 4 Bancerek, Grzegorz 4 Böhme, Sascha 4 Chvalovský, Karel 4 Cohn, Henry Lee 4 Cruanes, Simon 4 Iancu, Mihnea 4 Janičić, Predrag 4 Kühlwein, Daniel 4 Liu, Jun 4 Magron, Victor 4 Nipkow, Tobias 4 Popescu, Andrei 4 Reger, Giles 4 Tourret, Sophie 4 Waldmann, Uwe 4 Wenzel, Makarius 4 Xu, Yang 4 Zombori, Zsolt 3 Avigad, Jeremy 3 Byliński, Czesław 3 Chen, Shuwei 3 Färber, Michael 3 Heskes, Tom M. 3 Jaeger, Peter 3 Koutsoukou-Argyraki, Angeliki 3 Miyajima, Keiichi 3 Müller, Dennis 3 Narboux, Julien 3 Narita, Keiko 3 Nummelin, Visa 3 Otten, Jens 3 Piotrowski, Bartosz 3 Rowinska-Schwarzweller, Agnieszka 3 Schulz, Stephan 3 Tahar, Sofiène 3 Traytel, Dmitry 3 Voronkov, Andrei 3 Wernhard, Christoph 3 Ziobro, Rafał 2 Acewicz, Marcin 2 Bibel, Wolfgang 2 Blaauwbroek, Lasse 2 Caminati, Marco Bright 2 Cao, Feng 2 Carette, Jacques 2 Colbrook, Matthew J. 2 Corneli, Joseph 2 Czajka, Łukasz 2 Dahmen, Sander R. 2 Desharnais, Martin 2 Dubut, Jérémy 2 Farmer, William M. 2 Fleury, Mathias 2 Geuvers, Jan Herman 2 Goertzel, Zarathustra Amadeus 2 Gransden, Thomas 2 Guan, Yong 2 Guidi, Ferruccio 2 Gunther, Emmanuel 2 Hartman, Thomas E. 2 He, Xingxing 2 Heras, Jónathan 2 Holub, Štěpán 2 Janota, Mikoláš 2 Klakow, Dietrich 2 Koepke, Peter 2 Komendantskaya, Ekaterina 2 Leitsch, Alexander ...and 351 more Authors all top 5 Cited in 46 Serials 138 Formalized Mathematics 47 Journal of Automated Reasoning 8 Bulletin of the American Mathematical Society. New Series 5 AI Communications 5 Mathematics in Computer Science 4 Journal of Symbolic Computation 4 Logical Methods in Computer Science 3 Information Sciences 3 International Journal of Approximate Reasoning 3 Annals of Mathematics and Artificial Intelligence 2 Artificial Intelligence 2 Theoretical Computer Science 2 Annals of Pure and Applied Logic 2 Formal Aspects of Computing 2 Experimental Mathematics 2 Journal of High Energy Physics 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Mathematics of Computation 1 The Mathematical Intelligencer 1 ACM Transactions on Mathematical Software 1 Applied Mathematics and Optimization 1 Journal für die Reine und Angewandte Mathematik 1 Synthese 1 Computer Aided Geometric Design 1 Information and Computation 1 Computational Mechanics 1 Computational Mathematics and Modeling 1 Computational Geometry 1 Journal of Elasticity 1 Formal Methods in System Design 1 Soft Computing 1 Journal of the European Mathematical Society (JEMS) 1 Journal of Mathematical Logic 1 Lobachevskii Journal of Mathematics 1 La Gaceta de la Real Sociedad Matemática Española 1 Foundations of Computational Mathematics 1 Computer Languages, Systems & Structures 1 Journal of Applied Logic 1 Logica Universalis 1 São Paulo Journal of Mathematical Sciences 1 The Review of Symbolic Logic 1 Forum of Mathematics, Pi 1 Vestnik Udmurtskogo Universiteta. Matematika. Mekhanika. Komp’yuternye Nauki 1 Journal of Logical and Algebraic Methods in Programming 1 Modelirovanie i Analiz Informatsionnykh Sistem 1 Proceedings of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 41 Fields 340 Computer science (68-XX) 131 Mathematical logic and foundations (03-XX) 33 Number theory (11-XX) 18 Geometry (51-XX) 14 Field theory and polynomials (12-XX) 14 Commutative algebra (13-XX) 13 Real functions (26-XX) 13 Functional analysis (46-XX) 12 General and overarching topics; collections (00-XX) 12 Linear and multilinear algebra; matrix theory (15-XX) 10 Convex and discrete geometry (52-XX) 9 Group theory and generalizations (20-XX) 9 General topology (54-XX) 8 Order, lattices, ordered algebraic structures (06-XX) 8 Operator theory (47-XX) 6 Combinatorics (05-XX) 6 Measure and integration (28-XX) 6 Numerical analysis (65-XX) 6 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 5 History and biography (01-XX) 5 Operations research, mathematical programming (90-XX) 4 Algebraic geometry (14-XX) 4 Sequences, series, summability (40-XX) 4 Systems theory; control (93-XX) 3 Algebraic topology (55-XX) 3 Probability theory and stochastic processes (60-XX) 2 Associative rings and algebras (16-XX) 2 Category theory; homological algebra (18-XX) 2 Mechanics of particles and systems (70-XX) 2 Mechanics of deformable solids (74-XX) 2 Optics, electromagnetic theory (78-XX) 2 Quantum theory (81-XX) 2 Information and communication theory, circuits (94-XX) 2 Mathematics education (97-XX) 1 Nonassociative rings and algebras (17-XX) 1 Topological groups, Lie groups (22-XX) 1 Partial differential equations (35-XX) 1 Harmonic analysis on Euclidean spaces (42-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Statistics (62-XX) 1 Relativity and gravitational theory (83-XX) Citations by Year