Re: Other systems

[Grzegorz Bancerek <bancerek@cs.shinshu-u.ac.jp>]

Hi,

David wrote:
> 
> Hi!  Does anybody know if there is any other deduction software with a nice big
> library of theorems and proofs?  Like Mizar?

There is an opinion that Mizar is the system with the largest library.
John McCarthy on the page
 http://www-formal.stanford.edu/jmc/future/objectivity.html
expresses such opinion.

>  I've been able to find other
> deduction software, except that none of them feature a big library of proven
> theorems like Mizar has (20 thousand theorems according to the homepage).

The numbers are following:
articles - 703;
theorems - 34944; definitions - 6244; schemes - 623; definientia - 2315;
functors - 4672; modes - 381; predicates - 624; attributes - 1360;
existential registrations - 1238;
conditional registrations - 922;
term adjective registrations - 2472; 

> And thanks everybody for the pointers on where to start learning mizar!

Try
 http://www.cs.kun.nl/~freek/mizar/
But, the best place to start is Bialystok (or Nagano).

Grzegorz