leanCoP : lean connection-based theorem proving

The Prolog program implements a theorem prover for classical first-order (clausal) logic which is based on the connection calculus. It is sound and complete (provided that an arbitrarily large I is iteratively given), and demonstrates a comparatively strong performance.