Enclosed is the MML theorem subsumption information computed by MoMM. Out of the initial number of 58760 clauses generated from Mizar theorems, 1307 are subsumed. This file was essentially produced by grep "pos.*pos" all.ths.cb > subsumed.ths invoked on the file all.ths.cb from the MoMM distro, followed by some simple postprocessing. The recommended way to look at the results, is to force mizar-mode (M-x mizar-mode) on the file, split the screen into 3 windows, and proceed by Shift-left clicking on the pairs of references. Though this can be used to remove many redundancies, I would like to warn against using this unselectively. The exported theorems are not the only treasure in MML, the proofs are equally valuable (or even more, from the point of data mining). Removing a theorem with different proof just because it is subsumed, is a loss from this point of view, also from the theory development point of view and its possible use for education. My opinion is that we should think of syntax additions that could take care of such features, and e.g. allow for multiple proofs for one theorem. Josef
Attachment:
subsumed.ths.gz
Description: GNU Zip compressed data