Statistical testing procedure for lengths of formalized proofs
Ivan Kramosil · Czech digital mathematics library · 1980
A statistical testing procedure is proposed, which enables to test, given a formula of a for-malized theory, whether there exists a proof of this formula the length of which does not exceed an a priori given threshold value. Such a decision rule may be of great importance when applied to automated problem solving as it prevents us from looking for solutions which are inappropriate from applicational points of view. 1.