"Formalized Mathematics"

[Roman Matuszewski]

Dear All,

I would like to inform you that from May 2008
our journal "Formalized Mathematics" is published at the
MetaPress platform:
http://versita.metapress.com/content/121073/
Every article has a DOI number and all articles will soon
be indexed by most Abstracting Services.

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

Best regards,

Roman Matuszewski, Editor

-------
dr Roman Matuszewski, University of Bialystok, Poland
http://mizar.org/people/romat/

[Jesse Alama]

Roman Matuszewski <romat@...> 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.  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

--
Jesse Alama (alama@...)

[Piotr Rudnicki]

On Fri, Jul 11, 2008 at 01:51:32PM -0700, Jesse Alama wrote:

> Roman Matuszewski <romat@...> 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

[trybulec]

Piotr Rudnicki wrote:

>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.
>
>  
>
What do you mean by this?

It is not a critisism, just interested.

Andrzej

[Piotr Rudnicki]

I meant that paying attention to CiteSeer statistics for basic MML articles
is essentially meaningless.  If something is cited everywhere it is like cited
by default, i.e. not cited at all.

PR


On Thu, Jul 17, 2008 at 05:56:17PM +0200, trybulec wrote:

> Piotr Rudnicki wrote:
>
> >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.
> >
> >
> >
> What do you mean by this?
>
> It is not a critisism, just interested.
>
> Andrzej

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

[trybulec]

Jesse Alama wrote:

>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.  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?)
>
>  
>

Roman agreed to suppress all citation to TARSKI in next issues of FM.
So, it will be not so often cited, in FM not at all.

You are not quite right about the citation structure of FM. The articles
are cited only when the notation introduced in them is used. So, TARSKI
is so often cited because of the singleton , the unordered pair, the
ordered pair,, and the inclusion are defined in it.

And we would cite, if not Euclid or Newton, then Cantor or Peano rather
than Halmos or others.

There are not citation to the Encyclopedia articles (these with the name
starting with 'X') nor even for addenda like VALUED_0. When an
Encyclopedia file XRELA_0 for binary relations is eventually ready, that
the citation to RELAT_1 will vanish.

The TARSKI is an exception, it cannot be overridden by an Encyclopedia
article, and it is axiomatics. So, probably it should be not cited.

Regards,
Andrzej