Edit Profile Urban, Josef Compute Distance To: Compute Author ID: urban.josef Published as: Urban, Josef Documents Indexed: 76 Publications since 2003, including 3 Books all top 5 Co-Authors 6 single-authored 25 Kaliszyk, Cezary 9 Vyskočil, Jiří 8 Kühlwein, Daniel 8 Sutcliffe, Geoff 7 Geuvers, Jan Herman 7 Jakubův, Jan 6 Alama, Jesse 4 Bancerek, Grzegorz 4 Davenport, James Harold 4 Schulz, Stephan 3 Blanchette, Jasmin Christian 3 Heskes, Tom M. 3 Mamane, Lionel Elie 3 Naumowicz, Adam 3 Rudnicki, Piotr 3 Tankink, Carst 3 Tsivtsivadze, Evgeni 3 Wiedijk, Freek 2 Brown, Chad Edward 2 Gauthier, Thibault 2 Goertzel, Zarathustra 2 Harrison, John R. 2 Kohlhase, Michael 2 Labahn, George 2 Piotrowski, Bartosz 2 Rabe, Florian 1 Adams, Mark 1 Bauer, Gertrud 1 Blaauwbroek, Lasse 1 Brink, Kasper 1 Byliński, Czesław 1 Chvalovský, Karel 1 Dang, Tat Dat 1 Dunchev, Cvetan 1 Färber, Michael 1 Farmer, William M. 1 Grabowski, Adam 1 Greenaway, David 1 Hales, Thomas Callister 1 Harrison, John 1 Hoang, Le Truong 1 Hoder, Kryštof 1 Iancu, Mihnea 1 Kauers, Manuel 1 Khan Afshar, Sanaz 1 Korniłowicz, Artur 1 Lange, Christoph 1 Magron, Victor 1 Matuszewski, Roman 1 McLaughlin, Sean 1 Nguyen, Quang Truong 1 Nguyen, Tat Thang 1 Nipkow, Tobias 1 Obua, Steven 1 Pąk, Karol 1 Paulson, Lawrence Charles 1 Pease, Adam 1 Pleso, Joseph 1 Pudlák, Pavel 1 Rute, Jason 1 Sexton, Alan P. 1 Siddique, Umair 1 Sojka, Petr 1 Solovyev, Alexey 1 Stanovský, David 1 Štěpánek, Petr 1 Suda, Martin 1 Ta Thi Hoai An 1 Tahar, Sofiène 1 Tran, Nam Trung 1 Trieu, Thi Diep 1 van Laarhoven, Twan 1 Voronkov, Andrei 1 Vu, Ky Minh 1 Wang, Qingxiang 1 Watt, Stephen Michael 1 Zumkeller, Roland all top 5 Serials 10 Journal of Automated Reasoning 3 Lecture Notes in Computer Science 3 Mathematics in Computer Science 2 Journal of Formalized Reasoning 1 Journal of Symbolic Computation 1 AI Communications 1 Nieuw Archief voor Wiskunde. Vijfde Serie 1 Journal of Applied Logic 1 Forum of Mathematics, Pi all top 5 Fields 74 Computer science (68-XX) 10 Mathematical logic and foundations (03-XX) 5 General and overarching topics; collections (00-XX) 2 History and biography (01-XX) 2 Convex and discrete geometry (52-XX) 1 Numerical analysis (65-XX) 1 Optics, electromagnetic theory (78-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH 52 Publications have been cited 467 times in 189 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 74 2015 MPTP 0.2: Design, implementation, and initial experiments. Zbl 1113.68095Urban, Josef 23 2006 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283Kaliszyk, Cezary; Urban, Josef 22 2014 ATP and presentation service for Mizar formalizations. Zbl 1260.68380Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 21 2013 XML-izing Mizar: Making semantic processing and presentation of MML easy. Zbl 1151.68681Urban, Josef 21 2006 MizAR 40 for Mizar 40. Zbl 1356.68191Kaliszyk, Cezary; Urban, Josef 19 2015 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 19 2014 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří 17 2008 MPTP-motivation, implementation, first experiments. Zbl 1075.68081Urban, Josef 16 2004 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177Kaliszyk, Cezary; Urban, Josef 13 2015 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 12 2013 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 11 2017 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 11 2013 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 10 2003 MaLeCoP. Machine learning connection prover. Zbl 1332.68206Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr 9 2011 Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128Urban, Josef; Hoder, Krystof; Voronkov, Andrei 9 2010 MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103Urban, Josef 9 2006 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 8 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 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 7 2016 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220Kaliszyk, Cezary; Urban, Josef 7 2015 PRocH: proof reconstruction for HOL Light. Zbl 1381.68271Kaliszyk, Cezary; Urban, Josef 7 2013 Automated and human proofs in general mathematics: an initial comparison. Zbl 1352.68211Alama, Jesse; Kühlwein, Daniel; Urban, Josef 7 2012 A Wiki for Mizar: motivation, considerations, and initial prototype. Zbl 1286.68434Urban, Josef; Alama, Jesse; Rudnicki, Piotr; Geuvers, Herman 7 2010 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ří 5 2013 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 06528775Kaliszyk, Cezary; Urban, Josef 4 2015 Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Zbl 1293.68035Watt, Stephen M. (ed.); Davenport, James H. (ed.); Sexton, Alan P. (ed.); Sojka, Petr (ed.); Urban, Josef (ed.) 4 2014 Lemma mining over HOL Light. Zbl 1407.68437Kaliszyk, Cezary; Urban, Josef 4 2013 Formal mathematics on display: a wiki for Flyspeck. Zbl 1390.68751Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 4 2013 Automated proof compression by invention of new definitions. Zbl 1253.68293Vyskočil, Jiří; Stanovský, David; Urban, Josef 4 2010 System description: E.T. 0.1. Zbl 06515521Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 3 2015 Developing corpus-based translation methods between informal and formal mathematics: project description. Zbl 1304.68172Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří; Geuvers, Herman 3 2014 Automated reasoning service for HOL Light. Zbl 1390.68576Kaliszyk, Cezary; Urban, Josef 3 2013 Automated reasoning and presentation support for formalizing mathematics in MizAR. Zbl 1286.68403Urban, Josef; Sutcliffe, Geoff 3 2010 Hammering towards QED. Zbl 07106506Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 2 2016 Lemmatization for stronger reasoning in large theories. Zbl 06688824Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 2 2015 MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193Kühlwein, Daniel; Urban, Josef 2 2015 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2 2013 E-MaLeS 1.1. Zbl 1381.68273Kühlwein, Daniel; Schulz, Stephan; Urban, Josef 2 2013 Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Zbl 1218.68014Davenport, James H. (ed.); Farmer, William M. (ed.); Urban, Josef (ed.); Rabe, Florian (ed.) 2 2011 Presenting and explaining Mizar. Zbl 1278.68283Urban, Josef; Bancerek, Grzegorz 2 2007 GRUNGE: a grand unified ATP challenge. Zbl 07178973Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 1 2019 Automating formalization by statistical and semantic parsing of mathematics. Zbl 06821841Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2017 Detecting inconsistencies in large first-order knowledge bases. Zbl 06778411Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam 1 2017 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 Learning to parse on aligned corpora (rough diamond). Zbl 06481866Kaliszyk, 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 GRUNGE: a grand unified ATP challenge. Zbl 07178973Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef 1 2019 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 11 2017 Automating formalization by statistical and semantic parsing of mathematics. Zbl 06821841Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2017 Detecting inconsistencies in large first-order knowledge bases. Zbl 06778411Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam 1 2017 A learning-based fact selector for Isabelle/HOL. Zbl 1386.68149Blanchette, Jasmin Christian; Greenaway, David; Kaliszyk, Cezary; Kühlwein, Daniel; Urban, Josef 7 2016 Hammering towards QED. Zbl 07106506Blanchette, Jasmin C.; Kaliszyk, Cezary; Paulson, Lawrence C.; Urban, Josef 2 2016 Extracting higher-order goals from the Mizar Mathematical Library. Zbl 1344.68203Brown, Chad E.; 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 74 2015 MizAR 40 for Mizar 40. Zbl 1356.68191Kaliszyk, Cezary; Urban, Josef 19 2015 HOL(y)Hammer: online ATP service for HOL Light. Zbl 1322.68177Kaliszyk, Cezary; Urban, Josef 13 2015 Learning-assisted theorem proving with millions of lemmas. Zbl 1315.68220Kaliszyk, Cezary; Urban, Josef 7 2015 FEMaLeCoP: fairly efficient machine learning connection prover. Zbl 06528775Kaliszyk, Cezary; Urban, Josef 4 2015 System description: E.T. 0.1. Zbl 06515521Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří 3 2015 Lemmatization for stronger reasoning in large theories. Zbl 06688824Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 2 2015 MaLeS: a framework for automatic tuning of automated theorem provers. Zbl 1356.68193Kühlwein, Daniel; Urban, Josef 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 06481866Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří 1 2015 Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\). Zbl 1314.68283Kaliszyk, Cezary; Urban, Josef 22 2014 Premise selection for mathematics by corpus analysis and kernel methods. Zbl 1315.68217Alama, Jesse; Heskes, Tom; Kühlwein, Daniel; Tsivtsivadze, Evgeni; Urban, Josef 19 2014 Intelligent computer mathematics. International conference, CICM 2014, Coimbra, Portugal, July 7–11, 2014. Proceedings. Zbl 1293.68035Watt, Stephen M. (ed.); Davenport, James H. (ed.); Sexton, Alan P. (ed.); Sojka, Petr (ed.); Urban, Josef (ed.) 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 3 2014 ATP and presentation service for Mizar formalizations. Zbl 1260.68380Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff 21 2013 The Mizar Mathematical Library in OMDoc: translation and applications. Zbl 1260.68375Iancu, Mihnea; Kohlhase, Michael; Rabe, Florian; Urban, Josef 12 2013 MaSh: machine learning for Sledgehammer. Zbl 1317.68215Kühlwein, Daniel; Blanchette, Jasmin Christian; Kaliszyk, Cezary; Urban, Josef 11 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ří 5 2013 Lemma mining over HOL Light. Zbl 1407.68437Kaliszyk, Cezary; Urban, Josef 4 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 Communicating formal proofs: the case of Flyspeck. Zbl 1317.68232Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman 2 2013 E-MaLeS 1.1. Zbl 1381.68273Kühlwein, Daniel; Schulz, Stephan; Urban, Josef 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 8 2012 Automated and human proofs in general mathematics: an initial comparison. Zbl 1352.68211Alama, Jesse; Kühlwein, Daniel; Urban, Josef 7 2012 Dependencies in formal mathematics: applications and extraction for Coq and Mizar. Zbl 1335.68221Alama, Jesse; Mamane, Lionel; Urban, Josef 6 2012 Licensing the Mizar Mathematical Library (MML). Zbl 1278.68290Alama, Jesse; Kohlhase, Michael; Mamane, Lionel; Naumowicz, Adam; Rudnicki, Piotr; Urban, Josef 17 2011 MaLeCoP. Machine learning connection prover. Zbl 1332.68206Urban, Josef; Vyskočil, Jiří; Štěpánek, Petr 9 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.68014Davenport, James H. (ed.); Farmer, William M. (ed.); Urban, Josef (ed.); Rabe, Florian (ed.) 2 2011 Evaluation of automated theorem proving on the Mizar mathematical library. Zbl 1294.68128Urban, Josef; Hoder, Krystof; Voronkov, Andrei 9 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 3 2010 MaLARea SG1 – machine learner for automated reasoning with semantic guidance. Zbl 1165.68434Urban, Josef; Sutcliffe, Geoff; Pudlák, Petr; Vyskočil, Jiří 17 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 23 2006 XML-izing Mizar: Making semantic processing and presentation of MML easy. Zbl 1151.68681Urban, Josef 21 2006 MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103Urban, Josef 9 2006 MPTP-motivation, implementation, first experiments. Zbl 1075.68081Urban, Josef 16 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 10 2003 all cited Publications top 5 cited Publications all top 5 Cited by 214 Authors 27 Urban, Josef 19 Kaliszyk, Cezary 16 Coghetto, Roland 14 Pąk, Karol 14 Shidama, Yasunari 11 Grabowski, Adam 11 Korniłowicz, Artur 9 Futa, Yuichi 9 Naumowicz, Adam 8 Kohlhase, Michael 8 Nakasho, Kazuhisa 7 Blanchette, Jasmin Christian 7 Rabe, Florian 5 Alama, Jesse 5 Okazaki, Hiroyuki 5 Schwarzweller, Christoph 5 Vyskočil, Jiří 4 Bancerek, Grzegorz 4 Iancu, Mihnea 4 Koch, Sebastian 3 Benzmüller, Christoph Ewald 3 Böhme, Sascha 3 Endou, Noboru 3 Gauthier, Thibault 3 Jaeger, Peter 3 Janičić, Predrag 3 Kühlwein, Daniel 3 Narita, Keiko 3 Nipkow, Tobias 3 Paulson, Lawrence Charles 3 Sutcliffe, Geoff 3 Voronkov, Andrei 3 Ziobro, Rafał 2 Acewicz, Marcin 2 Brown, Chad Edward 2 Byliński, Czesław 2 Färber, Michael 2 Geuvers, Jan Herman 2 Gransden, Thomas 2 Guidi, Ferruccio 2 Heras, Jónathan 2 Heskes, Tom M. 2 Jakubův, Jan 2 Komendantskaya, Ekaterina 2 Leitsch, Alexander 2 Mamane, Lionel Elie 2 Matuszewski, Roman 2 Narboux, Julien 2 Popescu, Andrei 2 Raman, Rajeev 2 Rudnicki, Piotr 2 Sacerdoti Coen, Claudio 2 Schulz, Stephan 2 Siddique, Umair 2 Smallbone, Nicholas 2 Stojanović Đurđević, Sana 2 Tahar, Sofiène 2 Tsivtsivadze, Evgeni 2 Walkinshaw, Neil 2 Watase, Yasushige 2 Wenzel, Makarius 2 Wiesing, Tom 2 Woltzenlogel Paleo, Bruno 1 Abbasi, Mohsin Manshad 1 Abraham, Uri 1 Adams, Mark 1 Alt, Helmut 1 Aransay, Jesús 1 Aspinall, David 1 Bauer, Gertrud 1 Beeson, Michael J. 1 Bel’tyukov, Anatoliĭ Petrovich 1 Bentkamp, Alexander 1 Bezem, Marc 1 Bogoşel, Beniamin 1 Brink, Kasper 1 Buchin, Kevin 1 Bucur, Dorin 1 Cairns, Paul 1 Caminati, Marco Bright 1 Carette, Jacques 1 Chaplick, Steven 1 Chen, Shuwei 1 Cheong, Otfried 1 Chojecki, Przemyslaw 1 Claessen, Koen 1 Corneli, Joseph 1 Czajka, Łukasz 1 Dang, Tat Dat 1 Divasón, Jose 1 Dixon, Lucas 1 Dunchev, Cvetan 1 Elizarov, A. M. 1 Farmer, William M. 1 Fleury, Mathias 1 Ford, Ian J. 1 Fragalà, Ilaria 1 Furbach, Ulrich 1 Ganesalingam, Mohan 1 Giero, Mariusz ...and 114 more Authors all top 5 Cited in 19 Serials 65 Formalized Mathematics 32 Journal of Automated Reasoning 4 Mathematics in Computer Science 3 Annals of Mathematics and Artificial Intelligence 2 Theoretical Computer Science 2 Journal of Symbolic Computation 2 Formal Aspects of Computing 1 Artificial Intelligence 1 Applied Mathematics and Optimization 1 Information Sciences 1 Information and Computation 1 Bulletin of the American Mathematical Society. New Series 1 Lobachevskii Journal of Mathematics 1 Computer Languages, Systems & Structures 1 Journal of Applied Logic 1 Logica Universalis 1 Logical Methods in Computer Science 1 Forum of Mathematics, Pi 1 Vestnik Udmurtskogo Universiteta. Matematika. Mekhanika. Komp’yuternye Nauki all top 5 Cited in 27 Fields 125 Computer science (68-XX) 87 Mathematical logic and foundations (03-XX) 14 Number theory (11-XX) 12 Geometry (51-XX) 8 General topology (54-XX) 6 Field theory and polynomials (12-XX) 6 Commutative algebra (13-XX) 5 Order, lattices, ordered algebraic structures (06-XX) 5 Linear and multilinear algebra; matrix theory (15-XX) 4 Real functions (26-XX) 4 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Measure and integration (28-XX) 3 Sequences, series, summability (40-XX) 3 Operator theory (47-XX) 2 General and overarching topics; collections (00-XX) 2 Combinatorics (05-XX) 2 Algebraic geometry (14-XX) 2 Group theory and generalizations (20-XX) 2 Convex and discrete geometry (52-XX) 2 Probability theory and stochastic processes (60-XX) 2 Optics, electromagnetic theory (78-XX) 1 Topological groups, Lie groups (22-XX) 1 Functional analysis (46-XX) 1 Calculus of variations and optimal control; optimization (49-XX) 1 Operations research, mathematical programming (90-XX) 1 Information and communication theory, circuits (94-XX) 1 Mathematics education (97-XX) Citations by Year