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:
- (A) uniform learning methods
- (B) reusable ATP encoding components for different foundational aspects
- (C) integration of proof reconstruction, and
- (D) methods for knowledge extraction, reuse and content merging
Main results so far:
CoqHammer: First Hammer for Type TheoryIt 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!