proof co-occurrence graph
Josef Urban <[email protected]> Wed, 4 Sep 2013 15:36:12 +0200
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAFP4q17Vgp_RtKsNmOZV652ekW6RHFCUBK8YDKQX3D=PpZtb-g@mail.gmail.com> |
Hi, at http://mizar.cs.ualberta.ca/~mptp/mml4.181.1147/html/00clustering-max-20.out3.html is a listing of 5072 clusters (maximum size 20) of theorems and definitions from MML version 4.181.1147, based on their co-occurrence in MML proofs. The clustering was done by Twan van Laarhoven with his graph clustering software: https://github.com/twanvl/graph-cluster . Josef