Date: 20 February 2015
Host: Dr. Ekaterina Komendantskaya
Title: Learning and Exploration in Automated Theorem Proving
I will talk about the work in automated inductive theorem proving at Chalmers University. We are developing HipSpec, an automated theorem prover for proving inductive properties about Haskell programs. HipSpec uses a technique called theory exploration to automatically derive basic equational lemmas about recursively defined functions and datatypes. This is useful both as a method for automatically generating a specification of a program, and also provides the basis for a background theory which allows more complicated user-given properties to be proved automatically.
Our current work aims at improving the power and efficiency of the theory exploration part. I will also say something about a new project due to start this summer which aims at exploiting libraries of existing proofs to learn what kind of lemmas are likely to be useful for new proofs. This continues some initial work done in collaboration with Katya Komendantskaya here in Dundee.