Re: [mizar] Another factor...

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Freek:

> But I wonder what the factor is for the whole "waybel/yellow"
> translation up to now.  Does anyone have some data about
> this?  Order of magnitude is fine for me.  Also a description
> of which articles correspond to what part of the book would
> be okay (I can count the propositions in the book myself.)

At

	http://www.cs.ualberta.ca/~piotr/02JAR/

there is a paper that G. Bancerek and I submitted to JAR recently.  A
preliminary version of this paper is at

	http://www.cs.ualberta.ca/~piotr/02JAR/old/

which in an appendix contains the information you need.  This paper
contains other statistics of interest (and some qhich are totally
useless). 

Grzegorz's Japanese web page

	http://megrez.mizar.org/ccl/state.html#report

provides the information about the current state of things (it seems
nothing new has been done with ccl for quite a while).

The measure which you are suggesting may be misleading I am afraid if taken
at the face value as in principle it was possible to have such translation
almost at the 1-1 level.

Best,

-- 
Piotr Rudnicki              CompSci, University of Alberta, Edmonton, Canada
email: piotr@cs.ualberta.ca                 http://web.cs.ualberta.ca/~piotr