Statistical methods for comparing theorem proving algorithms
Ivan Kramosil, Zbigniew Zwinogrodzki · Czech digital mathematics library · 1974
In this paper a binary relation on a set of theorem proving algorithms is defined, using some basic notions of statistics and probability theory.This relation is proved to generate a linear ordering in any given set of theorem proving algorithms, it means to serve as an attempt to formalize somehow the often used phrase: "Algorithm A is better than algorithm B", at least in the case of theorem proving algorithms.A number of assertions describing some basic properties of this relation is stated and proved.The notion apparatus used here is close to that from [1]-[4].