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_{2} 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.

Text version

All remarks concerning this page please send to: arturk@math.uwb.edu.pl

[ Home | Project | Language | System | People | MML | FM | SUM ]

Last modified: October 20, 2000