Sciweavers

CADE
2008
Springer

randoCoP: Randomizing the Proof Search Order in the Connection Calculus

14 years 3 months ago
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.
Thomas Raths, Jens Otten
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Thomas Raths, Jens Otten
Comments (0)