Introduction

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.

Downloads

leanCoP + nanoCoP + Metis for HOL Light:

• Version 2018-08-28
• Version 2018-02-07
• Version 1.0 (2015-07-17)

isaCoP (tested with Isabelle2015):

• Version 0.1 (2016-03-07)