21 November 2016: Cezary Kaliszyk

As proofs of correctness of programs become more important in modern complex designs, automatically providing proof advice becomes a principal challenge. The strongest general purpose advice and automation for formal proofs is today provided by learning-reasoning systems called hammers. In this talk we will discuss several limitations of the current early generation of hammer systems and discuss new AI methods that will combine the knowledge and the reasoning techniques present in the current systems into a smart learning and reasoning system working over a large part of today's body of formalized knowledge. We will also show how the uniform learning methods and encoding components generalize advice for different proof assistants into a general advice system for semi-formal and informal proofs.