First-Order Theorem Prover Evaluation w.r.t. Relation- and Kleene Algebra

erschienen 2008 in R. Berghammer, B. Möller, Struth, G. (eds.): Relations and Kleene algebra in computer science. PhD Programme
Technical Report 2008-04, Institute of Computer Science, University of Augsburg, 2008, pp. 48-52

Abstract:
Recently it has been shown that off-the-shelf first-order auto- mated theorem provers can successfully verify statements of substantial complexity in relation and Kleene algebras. Until now most of our proof automation had been done using McCune’s theorem prover Prover9, while others like SPASS and Vampire were not used extensively. In this paper we use more than 500 theorems to compare and evaluate 13 first- order theorem provers.