Informational logic in knowledge representation and automated deduction

Informational logic is a new approach to the formalization of the notion of rational conjecture that is of interest both from the epistemic and the automated reasoning point of view. Given a logical system T, an informational logic is based on a new measure of logical information (which is defined on T-formulas) and on a mathematical definition of estimate criteria for proofs in T. This allows us to obtain a notion of informational theorem (L, p(L)) of a system T, where p(L) is the probability of L to be provable in T. The notion of probability is entirely founded on proof-theoretic concepts. In this paper, informational logic is presented, and applications of this idea to the representation of inductive reasoning and to automated theorem proving are shown.