The Dependence Tree of Mizar Articles
based on quantitative information transfer

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 (-log₂ n/N)

• a - the number of references to T in B,
• n - the number of references to T in all articles at the time when B was the last article accepted into MML,
• N - number of all references to theorems in the MML at that time.