Josef Urban (Czech Technical University in Prague)
Josef Urban is a Principal Researcher at the Czech Institute of Informatics, Robotics and Cybernetics (CIIRC) of the Czech Technical University in Prague where he is heading the ERC-funded project AI4REASON. His interests include Automated Reasoning, Formal Verification and Machine Learning. In particular, he is interested in development of combined inductive/learning and deductive/reasoning “strong AI” methods and systems over large formal (fully semantically specified) knowledge bases. Examples are large corpora of formally stated definitions, theorems and proofs in mathematics, software verification and related fields. He has made such corpora available to the AI methods, created the first benchmarks, and developed first approaches and systems combining learning and reasoning over such corpora in various feedback loops. The systems developed by him and his colleagues have won several competitions and the methods today assist formal verification in proof assistants. He has also co-developed first learning/reasoning systems for automated formalization of informal mathematics, and co-founded the conference on Artificial Intelligence and Theorem Proving (AITP). He received his MSc in Mathematics and PhD in Computers Science from the Charles University in Prague, worked as an assistant professor in Prague, and as a researcher at the University of Miami and Radboud University Nijmegen.
ENSPM 2022 Presentation
Title: Some recent combinations of AI and theorem proving methods
Abstract: I will give an overview of several recent advances in combining Artificial Intelligence and Theorem Proving methods.