Learning-Assisted Automated Reasoning
Cezary Kaliszyk
(University of Innsbruck).
Course Summary |
About the lecturer |
Location and schedule |
Materials
|
Assignment
In this course we will look at a number of classical automated reasoning problems and explore to what extent machine learning can be used to solve them. We will start with the basic reasoning calculi: tableaux and resolution and their extensions to reasoning with orderings and equality. We will survey the methods used for learning orderings, reasoning sub-procedures, and individual step selection. In the second part of the course we will look at the selection of relevant knowledge from a large axiom database. The problem has seen many applications of heuristics replaced by multi-label classifiers. We will finally look at the open problems in the automation of reasoning including conjecturing and theory exploration.
About the lecturer:Cezary Kaliszyk is an tenure-track associate professor at the University of Innsbruck, Austria. His research focuses on proof advice and automation for formal proofs. He received his MSc from the University of Warsaw, Poland in 2005, and his PhD in 2009, from the Radboud University, Netherlands. After two postdocs, one at TU Munich working on Nominal Logic and one at the University of Tsukuba, he joined the University of Innsbruck, Austria. He has received grants from the Austrian Science Fund, Japan Society for the Promotion of Science, and worked with Google Research on automating formalization. He is currently leading an ERC grant on sharing proofs across logical foundations.
Location and schedule:Room 4420. Schedule:
|
|
|
|||||||||||||||||||||||||