randoCoP: Randomizing the Proof Search Order in the Connection Calculus

Abstract. We present randoCoP, a theorem prover for classical firstorder 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 significantly. 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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Thomas Raths, Jens Otten
• Keywords: Automated Reasoning, CADE 2008, Classical Firstorder Logic, Connection Prover LeanCoP, Incomplete Search Variants