×
Compute Distance To:
Author ID: urban.josef Recent zbMATH articles by "Urban, Josef"
Published as: Urban, Josef
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

Publications by Year

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.68201
Bancerek, 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.68095
Urban, Josef
41
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
35
2014
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283
Kaliszyk, Cezary; Urban, Josef
34
2014
ATP and presentation service for Mizar formalizations. Zbl 1260.68380
Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff
33
2013
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
32
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
27
2017
MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434
Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří
27
2008
HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177
Kaliszyk, Cezary; Urban, Josef
26
2015
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
22
2006
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
21
2016
MaLeCoP. Machine learning connection prover. Zbl 1332.68206
Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr
17
2011
Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290
Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef
17
2011
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
17
2013
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\). Zbl 07178977
Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef
15
2019
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
14
2013
FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312
Kaliszyk, Cezary; Urban, Josef
13
2015
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
12
2016
Translating Mizar for first order theorem provers. Zbl 1022.68622
Urban, Josef
12
2003
ENIGMA: efficient learning-based inference guiding machine. Zbl 1367.68249
Jakubův, Jan; Urban, Josef
11
2017
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
11
2012
Integrated semantic browsing of the Mizar mathematical library for authoring Mizar articles. Zbl 1108.68583
Bancerek, Grzegorz; Urban, Josef
11
2004
Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128
Urban, Josef; Hoder, Krystof; Voronkov, Andrei
10
2010
MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103
Urban, Josef
10
2006
Automated and human proofs in general mathematics: an initial comparison. Zbl 1352.68211
Alama, Jesse; Kühlwein, Daniel; Urban, Josef
9
2012
Large formal wikis: issues and solutions. Zbl 1335.68220
Alama, Jesse; Brink, Kasper; Mamane, Lionel; Urban, Josef
8
2011
ATP-based cross-verification of Mizar proofs: method, systems, and first experiments. Zbl 1178.68532
Urban, Josef; Sutcliffe, Geoff
8
2008
Enhancing ENIGMA given clause guidance. Zbl 1417.68184
Jakubův, Jan; Urban, Josef
7
2018
Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220
Kaliszyk, Cezary; Urban, Josef
7
2015
A Wiki for Mizar: motivation, considerations, and initial prototype. Zbl 1286.68434
Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman
7
2010
PRocH: proof reconstruction for HOL Light. Zbl 1381.68271
Kaliszyk, Cezary; Urban, Josef
7
2013
TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef
7
2017
TacticToe: learning to prove with tactics. Zbl 07356973
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael
6
2021
Dependencies in formal mathematics: applications and extraction for Coq and Mizar. Zbl 1335.68221
Alama, Jesse; Mamane, Lionel; Urban, Josef
6
2012
Theorem proving in large formal mathematics as an emerging AI field. Zbl 1276.68139
Urban, Josef; Vyskočil, Jiří
6
2013
GRUNGE: a grand unified ATP challenge. Zbl 07178973
Brown, 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.68242
Blaauwbroek, Lasse; Urban, Josef; Geuvers, Herman
5
2020
Hierarchical invention of theorem proving strategies. Zbl 1462.68213
Jakubův, Jan; Urban, Josef
5
2018
Lemma mining over HOL Light. Zbl 1407.68437
Kaliszyk, Cezary; Urban, Josef
5
2013
Property invariant embedding for automated reasoning. Zbl 1464.68317
Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef
5
2020
Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
4
2013
ATPboost: learning premise selection in binary setting with ATP feedback. Zbl 06958123
Piotrowski, Bartosz; Urban, Josef
4
2018
Automated proof compression by invention of new definitions. Zbl 1253.68293
Vyskočil, Jiří; Stanovský, David; Urban, Josef
4
2010
Monte Carlo tableau proof search. Zbl 1494.68286
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
4
2017
Automated reasoning and presentation support for formalizing mathematics in MizAR. Zbl 1286.68403
Urban, 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.68172
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman
4
2014
System description: E.T. 0.1. Zbl 1465.68286
Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří
4
2015
ENIGMAWatch: ProofWatch meets ENIGMA. Zbl 1435.68370
Goertzel, Zarathustra; Jakubův, Jan; Urban, Josef
4
2019
History of interactive theorem proving. Zbl 1404.03010
Harrison, John; Urban, Josef; Wiedijk, Freek
4
2014
Machine learning guidance for connection tableaux. Zbl 07356974
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
3
2021
Automated reasoning service for HOL Light. Zbl 1390.68576
Kaliszyk, Cezary; Urban, Josef
3
2013
ProofWatch: watchlist guidance for large theories in E. Zbl 1435.68369
Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef
3
2018
Detecting inconsistencies in large first-order knowledge bases. Zbl 1494.68262
Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam
3
2017
E-MaLeS 1.1. Zbl 1381.68273
Kühlwein, Daniel; Schulz, Stephan; Urban, Josef
3
2013
MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193
Kühlwein, Daniel; Urban, Josef
3
2015
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
Presenting and explaining Mizar. Zbl 1278.68283
Urban, Josef; Bancerek, Grzegorz
2
2007
Extending E prover with similarity based clause selection strategies. Zbl 1347.68303
Jakubův, Jan; Urban, Josef
2
2016
Lemmatization for stronger reasoning in large theories. Zbl 1471.68313
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
2
2015
Guiding inferences in connection tableau by recurrent neural networks. Zbl 1455.68252
Piotrowski, Bartosz; Urban, Josef
1
2020
First neural conjecturing datasets and experiments. Zbl 1455.68261
Urban, Josef; Jakubův, Jan
1
2020
Extracting higher-order goals from the Mizar Mathematical Library. Zbl 1344.68203
Brown, Chad E.; Urban, Josef
1
2016
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
Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2017
The CADE-25 automated theorem proving system competition – CASC-25. Zbl 1373.68368
Sutcliffe, Geoff; Urban, Josef
1
2016
Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2015
ATP cross-verification of the Mizar MPTP challenge problems. Zbl 1137.68576
Urban, Josef; Sutcliffe, Geoff
1
2007
TacticToe: learning to prove with tactics. Zbl 07356973
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael
6
2021
Machine learning guidance for connection tableaux. Zbl 07356974
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
3
2021
The Tactician. A seamless, interactive tactic learner and prover for Coq. Zbl 1455.68242
Blaauwbroek, Lasse; Urban, Josef; Geuvers, Herman
5
2020
Property invariant embedding for automated reasoning. Zbl 1464.68317
Olšák, Miroslav; Kaliszyk, Cezary; Urban, Josef
5
2020
Guiding inferences in connection tableau by recurrent neural networks. Zbl 1455.68252
Piotrowski, Bartosz; Urban, Josef
1
2020
First neural conjecturing datasets and experiments. Zbl 1455.68261
Urban, Josef; Jakubův, Jan
1
2020
ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\). Zbl 07178977
Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef
15
2019
GRUNGE: a grand unified ATP challenge. Zbl 07178973
Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef
6
2019
ENIGMAWatch: ProofWatch meets ENIGMA. Zbl 1435.68370
Goertzel, Zarathustra; Jakubův, Jan; Urban, Josef
4
2019
Enhancing ENIGMA given clause guidance. Zbl 1417.68184
Jakubův, Jan; Urban, Josef
7
2018
Hierarchical invention of theorem proving strategies. Zbl 1462.68213
Jakubův, Jan; Urban, Josef
5
2018
ATPboost: learning premise selection in binary setting with ATP feedback. Zbl 06958123
Piotrowski, Bartosz; Urban, Josef
4
2018
ProofWatch: watchlist guidance for large theories in E. Zbl 1435.68369
Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef
3
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
27
2017
ENIGMA: efficient learning-based inference guiding machine. Zbl 1367.68249
Jakubův, Jan; Urban, Josef
11
2017
TacticToe: learning to reason with HOL4 tactics. Zbl 1403.68224
Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef
7
2017
Monte Carlo tableau proof search. Zbl 1494.68286
Färber, Michael; Kaliszyk, Cezary; Urban, Josef
4
2017
Detecting inconsistencies in large first-order knowledge bases. Zbl 1494.68262
Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam
3
2017
Automating formalization by statistical and semantic parsing of mathematics. Zbl 1483.68490
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
1
2017
Hammering towards QED. Zbl 1451.68318
Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef
21
2016
A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149
Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef
12
2016
Extending E prover with similarity based clause selection strategies. Zbl 1347.68303
Jakubův, Jan; Urban, Josef
2
2016
Extracting higher-order goals from the Mizar Mathematical Library. Zbl 1344.68203
Brown, Chad E.; Urban, Josef
1
2016
The CADE-25 automated theorem proving system competition – CASC-25. Zbl 1373.68368
Sutcliffe, Geoff; 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
110
2015
MizAR 40 for Mizar 40. Zbl 1356.68191
Kaliszyk, Cezary; Urban, Josef
32
2015
HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177
Kaliszyk, Cezary; Urban, Josef
26
2015
FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 1471.68312
Kaliszyk, Cezary; Urban, Josef
13
2015
Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220
Kaliszyk, Cezary; Urban, Josef
7
2015
System description: E.T. 0.1. Zbl 1465.68286
Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří
4
2015
MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193
Kühlwein, Daniel; Urban, Josef
3
2015
Lemmatization for stronger reasoning in large theories. Zbl 1471.68313
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
2
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
Learning to parse on aligned corpora (rough diamond). Zbl 1465.68287
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří
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
35
2014
Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283
Kaliszyk, 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.68172
Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman
4
2014
History of interactive theorem proving. Zbl 1404.03010
Harrison, John; Urban, Josef; Wiedijk, Freek
4
2014
ATP and presentation service for Mizar formalizations. Zbl 1260.68380
Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff
33
2013
The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375
Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef
17
2013
MaSh: machine learning for Sledgehammer. Zbl 1317.68215
Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef
14
2013
PRocH: proof reconstruction for HOL Light. Zbl 1381.68271
Kaliszyk, Cezary; Urban, Josef
7
2013
Theorem proving in large formal mathematics as an emerging AI field. Zbl 1276.68139
Urban, Josef; Vyskočil, Jiří
6
2013
Lemma mining over HOL Light. Zbl 1407.68437
Kaliszyk, Cezary; Urban, Josef
5
2013
Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751
Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
4
2013
Automated reasoning service for HOL Light. Zbl 1390.68576
Kaliszyk, Cezary; Urban, Josef
3
2013
E-MaLeS 1.1. Zbl 1381.68273
Kühlwein, Daniel; Schulz, Stephan; Urban, Josef
3
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
11
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
6
2012
MaLeCoP. Machine learning connection prover. Zbl 1332.68206
Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr
17
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
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.68128
Urban, Josef; Hoder, Krystof; Voronkov, Andrei
10
2010
A Wiki for Mizar: motivation, considerations, and initial prototype. Zbl 1286.68434
Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman
7
2010
Automated proof compression by invention of new definitions. Zbl 1253.68293
Vyskočil, Jiří; Stanovský, David; Urban, Josef
4
2010
Automated reasoning and presentation support for formalizing mathematics in MizAR. Zbl 1286.68403
Urban, Josef; Sutcliffe, Geoff
4
2010
MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434
Urban, 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.68532
Urban, Josef; Sutcliffe, Geoff
8
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
41
2006
XML-izing Mizar: Making semantic processing and presentation of MML easy. Zbl 1151.68681
Urban, Josef
22
2006
MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103
Urban, Josef
10
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 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

Citations by Year