The main goal of the project is to:

   develop a strong and uniform learning-reasoning system
   available for multiple logical foundations

Project workpackages and tasks:

project overview

Main results so far:

CoqHammer: First Hammer for Type Theory

It is already able to completely automatically prove half of the goals in the Coq standard library and has helped a number of other projects.
Try it out! hh logo

HOL(y)Hammer and TacticToe

Strong automation for HOL systems. Our systems are included in the HOL4 distribution!

Tactician

Try it out! tactician logo

Various results categorised:

WP A: Better Representation and Learning for ITPs

WP B: Monte-Carlo Tableaux

WB B: Guidance for Superposition

WP C: Isabelle/Mizar and Automation for it

WP C: Automation for Type Theory

WP D: Knowledge Re-use: Concept and libary merging

WP D: Evaluations for the methods for various provers

For all results see the publications list