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!


Try it out! tactician logo

See also the original project description

For all results see the publications list