Michael Färber


This page is about my tactics for automated theorem provers.

We offer a package that integrates leanCoP, nanoCoP, and Metis in HOL Light. The Metis tactic has since been integrated into HOL Light. The package also includes utilities to evaluate reconstruction performance.

For Isabelle, we offer an experimental integration of leanCoP.


leanCoP + nanoCoP + Metis for HOL Light:

isaCoP (tested with Isabelle2015):