CTU Events

 Today
«  January  2017  »
Mo Tu We Th Fr Sa Su
            1
2 3 4 5 6 7 8
9 10 11 12 13 14 15
16 17 18 19 20 21 22
23 24 25 26 27 28 29
30 31          

Back to calendar

PIS ? dr. Josef Urban: Artificial Intelligence and Theorem Proving

26 Jan 2017   16:00

LECTURE ANNOTATION:

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.

I will show examples of AI systems implementing positive feedback loops between induction and deduction, and show the performance of the current methods over large libraries of existing proof assistants such as Isabelle, Mizar, and HOL. Finally, I will mention emerging AI systems that combine statistical parsing of informal mathematics with such strong theorem proving methods.

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.

ABOUT THE PRAGUE COMPUTER SCIENCE SEMINAR:

The seminar will take place on the 4th Thursday of each month at 4:00pm (except June, July, August and December) alternately in the buildings of Faculty of Electrical Engineering, Czech Technical University, Karlovo nám. 13, Praha 2 and Faculty of Mathematics and Physics, Charles University, Malostranské nám. 25, Praha 1.

Its program will consist of a one-hour lecture followed by a discussion. The lecture should be based on an (internationally) exceptional or remarkable achievement of the lecturer, presented in a way which is comprehensible and interesting to a broad computer science community. The lectures will be in English.
The seminar framework was laid out by the preparatory committee consisting of Michal Chytil (Czech Academy of Sciences, Computer Science Institute), Pavel Kordík (Czech Tech. Univ., Faculty of Information Technologies), Jan Kybic (Czech Tech. Univ., Faculty of Electrical Engineering), Michal Pěchouček Czech Tech. Univ., Faculty of Electrical Engineering), Jiří Sgall (Charles University, Faculty of Mathematics and Physics), Vojtěch Svátek (University of Economics, Faculty of Informatics and Statistics), Michal Šorel (Czech Academy of Sciences,Institute of Information Theory and Automation), and Filip Železný (Czech Tech. Univ., Faculty of Electrical Engineering)

The idea to organize this seminar emerged in discussions of the representatives of several research institutes on how to avoid the undesired fragmentation of the Czech computer science community.

Place
MFF UK, Posluchárna S5, MFF UK, Malostranské nám. 25, Praha 1
Organizer
Přípravný výbor PIS
Contact person
Veronika Šínová, info@praguecomputerscience.cz, 224 35 7667
More information
http://www.praguecomputerscience.cz/index.php?l=en&p=25
Attachment
Download