randoCoP: Randomizing the Proof Search Order in the Connection Calculus. We present randoCoP , a theorem prover for classical first-order logic, which integrates randomized search techniques into the connection prover leanCoP 2.0. By randomly reordering the axioms of the problem and the literals within its clausal form, the incomplete search variants of leanCoP 2.0 can be improved signi cantly. We introduce details of the implementation and present comprehensive practical results by comparing the performance of randoCoP with leanCoP and other theorem provers on the TPTP library and problems involving large theories.
References in zbMATH (referenced in 1 article )
Showing result 1 of 1.