Josef Urban

I am a distinguished researcher at the Czech Institute of of Informatics, Robotics and Cybernetics (CIIRC) heading the ERC Consolidator project AI4REASON. Before that I was a postdoc researcher in the Foundations Group of ICIS at the Radboud University, Nijmegen, an assistant professor at the Department of Theoretical Computer Science and Mathematical Logic at Charles University in Prague (I co-founded the Prague Automated Reasoning Group), and a Marie-Curie fellow at the Department of Computer Science at University of Miami. (Scientific CV)

Education

Ph.D. in Computer Science (2004), Faculty of Mathematics and Physics, Charles University, Prague, (Full thesis)
M.S. in Mathematics (1998), Faculty of Mathematics and Physics, Charles University, Prague, (English summary)
B.S. in Economics (1995), Faculty of Social Sciences, Charles University, Prague

Research Interests

I am interested in automated reasoning in large semantically specified knowledge bases (some people call this "strong artificial intelligence"). It involves automated deductive reasoning (automated theorem proving), inductive reasoning (machine learning and discovery) and their combining. I am also quite involved in formalization and computer-verification of mathematics (see the QED Manifesto), especially in Mizar.

Here is a 2013 interview, a 2013 2-page paper (coming with a talk and slides) and a 2012 longer paper explaining what I have been doing for more than a decade and why. A lot of motivation is also in my earliest JAR paper about the first AI/ATP experiments done over Mizar in 2003. In 2014, I declared several AI/TP challenges and bets, and in 2018, I gave a long AGI 2018 keynote "No one shall drive us from the semantic AI paradise of computer-understandable math and science". Some history bits and motivation seen from 2021 are in an episode of Sean Welleck's Thesis Review Podcast. In 2023, I gave a long interview about my research and AI/TP topics to Hykel Hosni at The Reasoner.