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


Text version
Java not supported
All remarks concerning this page please send to:
[ Home | Project | Language | System | People | MML | FM | SUM ]

Last modified: October 20, 2000