Thursday, 19th of January 2017, 12:00 – 1:00

Strong Modular Proof Assistance: Reasoning across Theories

SR 1/2, ICT Building,
Technikerstraße 21a, 6020 Innsbruck


Cezary Kaliszyk
Research assistant at CL group, University of Innsbruck


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.