Learning-Assisted Automated Reasoning

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.

More info at http://phdopen.mimuw.edu.pl/index.php?page=z18w2.