ABSTRACT
In this paper the following problem is explored: if T is an equational fragment of Arithmetic PRA and S is a theorem proved by an automated prover through rewrite rules and induction rule, i.e. through a proof P in T +Induction, to assign a probability p(S) for S to belong to T . The notion of probability is produced via the new concepts of entropy or quantity of information of a proof and of virtual proof. The entropy of a proof is defined through an extension to a logical context of Shannon’s Information Theory; the notion of virtual proof is based on the possibility to estimate the length and the set of proper T-axioms of a possible proof Q of S in T. To this end a proof-theory for equational logic is proposed, a normal form for proofs is defined and a normal form theorem is given; properties of normal proofs are investigated and criteria to estimate the length of proofs are given.
