Michael Färber


This page is about the functional connection prover implementations developed by Michael Färber, Cezary Kaliszyk, and Josef Urban. They build on leanCoP/nanoCoP developed by Jens Otten and add various functions, such as machine learning and proof certification.


You can download the stand-alone connection provers here:

For the HOL tactics based on leanCoP/nanoCoP, see the Tactics page.