Edit Profile (opens in new tab) Urban, Josef Compute Distance To: Compute Author ID: urban.josef Published as: Urban, Josef Documents Indexed: 84 Publications since 2003 6 Contributions as Editor Co-Authors: 87 Co-Authors with 84 Joint Publications 1,218 Co-Co-Authors all top 5 Co-Authors 6 single-authored 31 Kaliszyk, Cezary 11 Jakubův, Jan 9 Vyskočil, Jiří 8 Kühlwein, Daniel 8 Sutcliffe, Geoff 7 Geuvers, Jan Herman 6 Alama, Jesse 6 Olšák, Miroslav 5 Schulz, Stephan 4 Bancerek, Grzegorz 4 Chvalovský, Karel 4 Davenport, James Harold 4 Heskes, Tom M. 4 Piotrowski, Bartosz 3 Blanchette, Jasmin Christian 3 Brown, Chad Edward 3 Gauthier, Thibault 3 Goertzel, Zarathustra Amadeus 3 Mamane, Lionel Elie 3 Naumowicz, Adam 3 Rudnicki, Piotr 3 Tankink, Carst 3 Tsivtsivadze, Evgeni 3 Wiedijk, Freek 3 Zombori, Zsolt 2 Blaauwbroek, Lasse 2 Färber, Michael 2 Kohlhase, Michael 2 Labahn, George 2 Rabe, Florian 2 Suda, Martin 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 Pease, Adam 1 Piepenbrock, Jelle 1 Pleso, Joseph 1 Pudlák, Pavel 1 Rute, Jason 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 Zhang, Liao 1 Zumkeller, Roland all top 5 Serials 12 Journal of Automated Reasoning 3 AI Communications 3 Lecture Notes in Computer Science 3 Mathematics in Computer Science 2 Journal of Formalized Reasoning 1 Journal of Symbolic Computation 1 Nieuw Archief voor Wiskunde. Vijfde Serie 1 Journal of Applied Logic 1 Forum of Mathematics, Pi all top 5 Fields 89 Computer science (68-XX) 6 General and overarching topics; collections (00-XX) 6 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 Optics, electromagnetic theory (78-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 70 Publications have been cited 781 times in 298 Documents Cited by ▼ Year ▼ Mizar: state-of-the-art and beyond. Zbl 1417.68201Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef 110 2015 MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095Urban, Josef 41 2006 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 35 2014 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283Kaliszyk, Cezary; Urban, Josef 34 2014 ATP and presentation service for Mizar formalizations. Zbl 1260.68380Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 33 2013 MizAR 40 for Mizar 40. Zbl 1356.68191Kaliszyk, Cezary; Urban, Josef 32 2015 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, 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 27 2017 MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří 27 2008 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177Kaliszyk, Cezary; Urban, Josef 26 2015 MPTP-motivation, implementation, first experiments. Zbl 1075.68081Urban, Josef 23 2004 XML-izing Mizar: Making semantic processing and presentation of MML easy. Zbl 1151.68681Urban, Josef 22 2006 Hammering towards QED. Zbl 1451.68318Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 21 2016 MaLeCoP. Machine learning connection prover. Zbl 1332.68206Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr 17 2011 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 17 2013 ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\). Zbl 07178977Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef 15 2019 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 14 2013 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312Kaliszyk, Cezary; Urban, Josef 13 2015 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 12 2016 Translating Mizar for first order theorem provers. Zbl 1022.68622Urban, Josef 12 2003 ENIGMA: efficient learning-based inference guiding machine. Zbl 1367.68249Jakubův, Jan; Urban, Josef 11 2017 Overview and evaluation of premise selection techniques for large theory mathematics. Zbl 1358.68259Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom 11 2012 Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. Zbl 1108.68583Bancerek, Grzegorz; Urban, Josef 11 2004 Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128Urban, Josef; Hoder, Krystof; Voronkov, Andrei 10 2010 MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103Urban, Josef 10 2006 Automated and human proofs in general mathematics: an initial comparison. Zbl 1352.68211Alama, Jesse; Kühlwein, Daniel; Urban, Josef 9 2012 Large formal wikis: issues and solutions. Zbl 1335.68220Alama, Jesse; Brink, Kasper; Mamane, Lionel; Urban, Josef 8 2011 ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Zbl 1178.68532Urban, Josef; Sutcliffe, Geoff 8 2008 Enhancing ENIGMA given clause guidance. Zbl 1417.68184Jakubův, Jan; Urban, Josef 7 2018 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220Kaliszyk, Cezary; Urban, Josef 7 2015 A Wiki for Mizar: motivation, considerations, and initial prototype. Zbl 1286.68434Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman 7 2010 PRocH: proof reconstruction for HOL Light. Zbl 1381.68271Kaliszyk, Cezary; Urban, Josef 7 2013 TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef 7 2017 TacticToe: learning to prove with tactics. Zbl 07356973Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael 6 2021 Dependencies in formal mathematics: applications and extraction for Coq and Mizar. Zbl 1335.68221Alama, Jesse; Mamane, Lionel; Urban, Josef 6 2012 Theorem proving in large formal mathematics as an emerging AI field. Zbl 1276.68139Urban, Josef; Vyskočil, Jiří 6 2013 GRUNGE: a grand unified ATP challenge. Zbl 07178973Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 6 2019 The Tactician. A seamless, interactive tactic learner and prover for Coq. Zbl 1455.68242Blaauwbroek, Lasse; Urban, Josef; Geuvers, Herman 5 2020 Hierarchical invention of theorem proving strategies. Zbl 1462.68213Jakubův, Jan; Urban, Josef 5 2018 Lemma mining over HOL Light. Zbl 1407.68437Kaliszyk, Cezary; Urban, Josef 5 2013 Property invariant embedding for automated reasoning. Zbl 1464.68317Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef 5 2020 Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 4 2013 ATPboost: learning premise selection in binary setting with ATP feedback. Zbl 06958123Piotrowski, Bartosz; Urban, Josef 4 2018 Automated proof compression by invention of new definitions. Zbl 1253.68293Vyskočil, Jiří; Stanovský, David; Urban, Josef 4 2010 Monte Carlo tableau proof search. Zbl 1494.68286Färber, Michael; Kaliszyk, Cezary; Urban, Josef 4 2017 Automated reasoning and presentation support for formalizing mathematics in MizAR. Zbl 1286.68403Urban, Josef; Sutcliffe, Geoff 4 2010 Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Zbl 1293.68035 4 2014 Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman 4 2014 System description: E.T. 0.1. Zbl 1465.68286Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 4 2015 ENIGMAWatch: ProofWatch meets ENIGMA. Zbl 1435.68370Goertzel, Zarathustra; Jakubův, Jan; Urban, Josef 4 2019 History of interactive theorem proving. Zbl 1404.03010Harrison, John; Urban, Josef; Wiedijk, Freek 4 2014 Machine learning guidance for connection tableaux. Zbl 07356974Färber, Michael; Kaliszyk, Cezary; Urban, Josef 3 2021 Automated reasoning service for HOL Light. Zbl 1390.68576Kaliszyk, Cezary; Urban, Josef 3 2013 ProofWatch: watchlist guidance for large theories in E. Zbl 1435.68369Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef 3 2018 Detecting inconsistencies in large first-order knowledge bases. Zbl 1494.68262Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam 3 2017 E-MaLeS 1.1. Zbl 1381.68273Kühlwein, Daniel; Schulz, Stephan; Urban, Josef 3 2013 MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193Kühlwein, Daniel; Urban, Josef 3 2015 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232Tankink, 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 Presenting and explaining Mizar. Zbl 1278.68283Urban, Josef; Bancerek, Grzegorz 2 2007 Extending E prover with similarity based clause selection strategies. Zbl 1347.68303Jakubův, Jan; Urban, Josef 2 2016 Lemmatization for stronger reasoning in large theories. Zbl 1471.68313Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 2 2015 Guiding inferences in connection tableau by recurrent neural networks. Zbl 1455.68252Piotrowski, Bartosz; Urban, Josef 1 2020 First neural conjecturing datasets and experiments. Zbl 1455.68261Urban, Josef; Jakubův, Jan 1 2020 Extracting higher-order goals from the Mizar Mathematical Library. Zbl 1344.68203Brown, Chad E.; Urban, Josef 1 2016 Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène 1 2015 Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2017 The CADE-25 automated theorem proving system competition – CASC-25. Zbl 1373.68368Sutcliffe, Geoff; Urban, Josef 1 2016 Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2015 ATP cross-verification of the Mizar MPTP challenge problems. Zbl 1137.68576Urban, Josef; Sutcliffe, Geoff 1 2007 TacticToe: learning to prove with tactics. Zbl 07356973Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael 6 2021 Machine learning guidance for connection tableaux. Zbl 07356974Färber, Michael; Kaliszyk, Cezary; Urban, Josef 3 2021 The Tactician. A seamless, interactive tactic learner and prover for Coq. Zbl 1455.68242Blaauwbroek, Lasse; Urban, Josef; Geuvers, Herman 5 2020 Property invariant embedding for automated reasoning. Zbl 1464.68317Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef 5 2020 Guiding inferences in connection tableau by recurrent neural networks. Zbl 1455.68252Piotrowski, Bartosz; Urban, Josef 1 2020 First neural conjecturing datasets and experiments. Zbl 1455.68261Urban, Josef; Jakubův, Jan 1 2020 ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\). Zbl 07178977Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef 15 2019 GRUNGE: a grand unified ATP challenge. Zbl 07178973Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 6 2019 ENIGMAWatch: ProofWatch meets ENIGMA. Zbl 1435.68370Goertzel, Zarathustra; Jakubův, Jan; Urban, Josef 4 2019 Enhancing ENIGMA given clause guidance. Zbl 1417.68184Jakubův, Jan; Urban, Josef 7 2018 Hierarchical invention of theorem proving strategies. Zbl 1462.68213Jakubův, Jan; Urban, Josef 5 2018 ATPboost: learning premise selection in binary setting with ATP feedback. Zbl 06958123Piotrowski, Bartosz; Urban, Josef 4 2018 ProofWatch: watchlist guidance for large theories in E. Zbl 1435.68369Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef 3 2018 A formal proof of the Kepler conjecture. Zbl 1379.52018Hales, 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 27 2017 ENIGMA: efficient learning-based inference guiding machine. Zbl 1367.68249Jakubův, Jan; Urban, Josef 11 2017 TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef 7 2017 Monte Carlo tableau proof search. Zbl 1494.68286Färber, Michael; Kaliszyk, Cezary; Urban, Josef 4 2017 Detecting inconsistencies in large first-order knowledge bases. Zbl 1494.68262Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam 3 2017 Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2017 Hammering towards QED. Zbl 1451.68318Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 21 2016 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 12 2016 Extending E prover with similarity based clause selection strategies. Zbl 1347.68303Jakubův, Jan; Urban, Josef 2 2016 Extracting higher-order goals from the Mizar Mathematical Library. Zbl 1344.68203Brown, Chad E.; Urban, Josef 1 2016 The CADE-25 automated theorem proving system competition – CASC-25. Zbl 1373.68368Sutcliffe, Geoff; Urban, Josef 1 2016 Mizar: state-of-the-art and beyond. Zbl 1417.68201Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef 110 2015 MizAR 40 for Mizar 40. Zbl 1356.68191Kaliszyk, Cezary; Urban, Josef 32 2015 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177Kaliszyk, Cezary; Urban, Josef 26 2015 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312Kaliszyk, Cezary; Urban, Josef 13 2015 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220Kaliszyk, Cezary; Urban, Josef 7 2015 System description: E.T. 0.1. Zbl 1465.68286Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 4 2015 MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193Kühlwein, Daniel; Urban, Josef 3 2015 Lemmatization for stronger reasoning in large theories. Zbl 1471.68313Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 2 2015 Formalizing physics: automation, presentation and foundation issues. Zbl 1417.68186Kaliszyk, Cezary; Urban, Josef; Siddique, Umair; Khan-Afshar, Sanaz; Dunchev, Cvetan; Tahar, Sofiène 1 2015 Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2015 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 35 2014 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283Kaliszyk, Cezary; Urban, Josef 34 2014 Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Zbl 1293.68035 4 2014 Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman 4 2014 History of interactive theorem proving. Zbl 1404.03010Harrison, John; Urban, Josef; Wiedijk, Freek 4 2014 ATP and presentation service for Mizar formalizations. Zbl 1260.68380Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 33 2013 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 17 2013 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 14 2013 PRocH: proof reconstruction for HOL Light. Zbl 1381.68271Kaliszyk, Cezary; Urban, Josef 7 2013 Theorem proving in large formal mathematics as an emerging AI field. Zbl 1276.68139Urban, Josef; Vyskočil, Jiří 6 2013 Lemma mining over HOL Light. Zbl 1407.68437Kaliszyk, Cezary; Urban, Josef 5 2013 Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 4 2013 Automated reasoning service for HOL Light. Zbl 1390.68576Kaliszyk, Cezary; Urban, Josef 3 2013 E-MaLeS 1.1. Zbl 1381.68273Kühlwein, Daniel; Schulz, Stephan; Urban, Josef 3 2013 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2 2013 Overview and evaluation of premise selection techniques for large theory mathematics. Zbl 1358.68259Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom 11 2012 Automated and human proofs in general mathematics: an initial comparison. Zbl 1352.68211Alama, Jesse; Kühlwein, Daniel; Urban, Josef 9 2012 Dependencies in formal mathematics: applications and extraction for Coq and Mizar. Zbl 1335.68221Alama, Jesse; Mamane, Lionel; Urban, Josef 6 2012 MaLeCoP. Machine learning connection prover. Zbl 1332.68206Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr 17 2011 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 Large formal wikis: issues and solutions. Zbl 1335.68220Alama, Jesse; Brink, Kasper; Mamane, Lionel; Urban, Josef 8 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.68128Urban, Josef; Hoder, Krystof; Voronkov, Andrei 10 2010 A Wiki for Mizar: motivation, considerations, and initial prototype. Zbl 1286.68434Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman 7 2010 Automated proof compression by invention of new definitions. Zbl 1253.68293Vyskočil, Jiří; Stanovský, David; Urban, Josef 4 2010 Automated reasoning and presentation support for formalizing mathematics in MizAR. Zbl 1286.68403Urban, Josef; Sutcliffe, Geoff 4 2010 MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří 27 2008 ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Zbl 1178.68532Urban, Josef; Sutcliffe, Geoff 8 2008 Presenting and explaining Mizar. Zbl 1278.68283Urban, Josef; Bancerek, Grzegorz 2 2007 ATP cross-verification of the Mizar MPTP challenge problems. Zbl 1137.68576Urban, Josef; Sutcliffe, Geoff 1 2007 MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095Urban, Josef 41 2006 XML-izing Mizar: Making semantic processing and presentation of MML easy. Zbl 1151.68681Urban, Josef 22 2006 MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103Urban, Josef 10 2006 MPTP-motivation, implementation, first experiments. Zbl 1075.68081Urban, Josef 23 2004 Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. Zbl 1108.68583Bancerek, Grzegorz; Urban, Josef 11 2004 Translating Mizar for first order theorem provers. Zbl 1022.68622Urban, Josef 12 2003 all cited Publications top 5 cited Publications all top 5 Cited by 321 Authors 41 Urban, Josef 25 Kaliszyk, Cezary 20 Coghetto, Roland 18 Shidama, Yasunari 16 Grabowski, Adam 16 Pąk, Karol 13 Korniłowicz, Artur 12 Blanchette, Jasmin Christian 12 Nakasho, Kazuhisa 10 Futa, Yuichi 10 Kohlhase, Michael 10 Naumowicz, Adam 10 Rabe, Florian 8 Okazaki, Hiroyuki 8 Schwarzweller, Christoph 7 Endou, Noboru 7 Jakubův, Jan 6 Bentkamp, Alexander 6 Paulson, Lawrence Charles 6 Suda, Martin 6 Sutcliffe, Geoff 5 Alama, Jesse 5 Gauthier, Thibault 5 Koch, Sebastian 5 Olšák, Miroslav 5 Vukmirović, Petar 5 Vyskočil, Jiří 5 Watase, Yasushige 4 Bancerek, Grzegorz 4 Benzmüller, Christoph Ewald 4 Böhme, Sascha 4 Brown, Chad Edward 4 Chvalovský, Karel 4 Cruanes, Simon 4 Iancu, Mihnea 4 Janičić, Predrag 4 Kühlwein, Daniel 4 Nipkow, Tobias 4 Popescu, Andrei 4 Reger, Giles 4 Tourret, Sophie 4 Waldmann, Uwe 3 Färber, Michael 3 Heskes, Tom M. 3 Jaeger, Peter 3 Koutsoukou-Argyraki, Angeliki 3 Narboux, Julien 3 Narita, Keiko 3 Rowinska-Schwarzweller, Agnieszka 3 Schulz, Stephan 3 Traytel, Dmitry 3 Voronkov, Andrei 3 Wenzel, Makarius 3 Yamazaki, Hiroshi 3 Ziobro, Rafał 3 Zombori, Zsolt 2 Acewicz, Marcin 2 Byliński, Czesław 2 Carette, Jacques 2 Cohn, Henry Lee 2 Czajka, Łukasz 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 He, Xingxing 2 Heras, Jónathan 2 Holub, Štěpán 2 Koepke, Peter 2 Komendantskaya, Ekaterina 2 Leitsch, Alexander 2 Li, Yongdong 2 Liu, Jun 2 Maletzky, Alexander 2 Mamane, Lionel Elie 2 Matuszewski, Roman 2 Mitsuishi, Takashi 2 Miyajima, Keiichi 2 Nummelin, Visa 2 Otten, Jens 2 Piotrowski, Bartosz 2 Raman, Rajeev 2 Rawson, Michael 2 Rudnicki, Piotr 2 Sacerdoti Coen, Claudio 2 Sawicki, Damian 2 Schlichtkrull, Anders 2 Shi, Zhiping 2 Siddique, Umair 2 Sieg, Wilfried 2 Smallbone, Nicholas 2 Stojanović Đurđević, Sana 2 Tahar, Sofiène 2 Tsivtsivadze, Evgeni 2 Walkinshaw, Neil 2 Wernhard, Christoph 2 Wiesing, Tom ...and 221 more Authors all top 5 Cited in 32 Serials 97 Formalized Mathematics 45 Journal of Automated Reasoning 4 AI Communications 4 Mathematics in Computer Science 3 Journal of Symbolic Computation 3 Annals of Mathematics and Artificial Intelligence 3 Logical Methods in Computer Science 2 Theoretical Computer Science 2 Formal Aspects of Computing 2 Bulletin of the American Mathematical Society. New Series 2 Experimental Mathematics 1 Artificial Intelligence 1 Jahresbericht der Deutschen Mathematiker-Vereinigung (DMV) 1 Mathematics of Computation 1 The Mathematical Intelligencer 1 Applied Mathematics and Optimization 1 Information Sciences 1 Computer Aided Geometric Design 1 Information and Computation 1 Computational Mechanics 1 Computational Mathematics and Modeling 1 Journal of Elasticity 1 Soft Computing 1 Journal of High Energy Physics 1 Lobachevskii Journal of 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 all top 5 Cited in 36 Fields 227 Computer science (68-XX) 113 Mathematical logic and foundations (03-XX) 19 Number theory (11-XX) 16 Geometry (51-XX) 10 Commutative algebra (13-XX) 9 Field theory and polynomials (12-XX) 8 Order, lattices, ordered algebraic structures (06-XX) 8 Linear and multilinear algebra; matrix theory (15-XX) 8 Real functions (26-XX) 8 General topology (54-XX) 6 Functional analysis (46-XX) 6 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 5 General and overarching topics; collections (00-XX) 5 Convex and discrete geometry (52-XX) 4 Measure and integration (28-XX) 4 Sequences, series, summability (40-XX) 4 Operator theory (47-XX) 3 Combinatorics (05-XX) 3 Group theory and generalizations (20-XX) 3 Probability theory and stochastic processes (60-XX) 3 Operations research, mathematical programming (90-XX) 2 History and biography (01-XX) 2 Algebraic geometry (14-XX) 2 Numerical analysis (65-XX) 2 Mechanics of deformable solids (74-XX) 2 Optics, electromagnetic theory (78-XX) 1 Associative rings and algebras (16-XX) 1 Category theory; homological algebra (18-XX) 1 Topological groups, Lie groups (22-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Algebraic topology (55-XX) 1 Mechanics of particles and systems (70-XX) 1 Quantum theory (81-XX) 1 Systems theory; control (93-XX) 1 Information and communication theory, circuits (94-XX) 1 Mathematics education (97-XX) Citations by Year