Michael Färber


This page is about my tactics for automated theorem provers.

The newest tactic addition is isaCoP, which uses leanCoP to search for and reconstruct proofs in Isabelle.

Furthermore, this page archives my HOL Light version of the Metis tactic that can be used for proof reconstruction and proof search. In the meanwhile, this tactic has been integrated into HOL Light. For comparison, the package also includes the leanCoP tactic implemented by Cezary Kaliszyk, as well as utilities and datasets to evaluate reconstruction performance.


isaCoP (tested with Isabelle2015):

Metis + leanCoP for HOL Light: