The Prague Computer Science seminar series, coorganized by Department of Computer Science, presents:
Artificial Intelligence and Theorem Proving by Josef Urban
Thursday, January 26 at 4 p.m. in Auditorium S5, MFF UK (Malostranské nám. 25, Praha 1).
The talk will cover several AI methods used to learn proving of conjectures over large formal mathematical corpora. This includes (i) machine-learning methods that learn from previous proofs how to suggest the most relevant lemmas for proving the next conjectures, (ii) methods that guide low-level proof-search algorithms based on previous proof traces, and (iii) methods that automatically invent suitable theorem-proving strategies on classes of problems.
More about the lecturer:
Josef Urban is a senior 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 main interest is development of combined inductive and deductive AI methods over large formal (fully semantically specified) knowledge bases, such as large corpora of formally stated mathematical definitions, theorems and proofs. His systems have won several competitions in this field. 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.