Introduction

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.

Downloads

You can download the stand-alone connection provers here:

• Version 2017-12-12

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