An article A is an ancestor of an article B if B refers to theorems in A, that is A transfers information to B. The direct ancestor A of an article B is the article which transfers the largest quantity of information into B. The tree below presents the direct ancestor relationship among Mizar articles.
The amount of information that an article A transfers to an article B is calculated as the sum of information transferred by all theorems from A which are referred to in B.
Let T be a theorem from A that is referred to in B. The amount of information, I, carried into B by T is calculated using the Shannon formula as:
I = a (-log2 n/N)where
Last modified: October 20, 2000