[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] "Formalized Mathematics"

On Fri, Jul 11, 2008 at 01:51:32PM -0700, Jesse Alama wrote:
> Roman Matuszewski <romat@mizar.org> writes:
> 
> > Additionaly, please observe that 5 articles published
> > in "Formalized Mathematics" are in the first 20 most
> > cited computer science articles in the CiteSeerX:
> > http://citeseerx.ist.psu.edu/stats/articles;jsessionid=D28942507FE29084C3D690F0B650872A
> 
> These five articles ("Tarski-Grothendieck set theory", "Properties of
> subsets", "Functions and their basic properties", "Relations and their
> basic properties", "Functions from a set to a set") are in the top 20
> for a simple reason: the articles in the citeseer database that cite
> them are also FM articles, and virtually all the MML depends on TARSKI.
> 
> The citation structure of FM articles is rather different from that of
> other journals.  In mizar everything -- everything! -- that is logically
> required for your article gets cited.  

Not always. sometimes newer notions replace old notions and as a result
someone's substantial contribution may not cited at all.  E.g. AMI_3 and
SCM_1 were meant to be an interface to AMI_1 and AMI_2.  
At least AMI_2 is hardly ever referenced.

I think that the most frequently referenced Mizar articles should be
imported by deafault and then the Mizar presence at CiteSeer would become
somewhat more realistic.

> If other journals required
> citations like that, then the citeseer top 20 would probably look very
> different.  (What might be at the top of the pile?  Feller's probability
> books?  Spivak's Calculus?  Halmos's Naive Set Theory?)
> 
> Jesse

The citations measure something but it is far from clear what.  Until
now, my little note "An Overview of the MIZAR Project" in Proceedings of
1992 Workshop on Types and Proofs for Programs, pages 311--332, June
1992 is being cited although there are much newer (and IMHO better) overviews
of Mizar.  I think that authors simply copy references from one paper
to another.

Cheers,

-- 
Piotr Rudnicki                                http://web.cs.ualberta.ca/~piotr