Talk:Mizar (software)

Need more simple examples

It would be good to add also examples that check simple relations, in particular,

2>1
x^2=x*x

Explain this to me on a simple example; the difficult example I will be able to do on my own - Israel Gelfand, 1994, http://israelmgelfand.com/edu_work.html

The guide for choice of the libraries seems to be absent. It could be just a script that adds and removes libraries one by one, checking, weather the number of non-accepted lines increases or reduces. But I cannot find such a script at their homepage. What should be a keyword for such a search?

Dmitrii Kouznetsov 05:23, 29 January 2010 (UTC)
P.S. the { {subpages} } is not accepted...

I add more example, but I could construct nothing workable about operations ^, sin, exp. According the manual, they should be supported at the including of the name SIN_COS into the headers, but this does not seem to work... If anybody can add the correct examples to check 1^1=1, sin(0)=0, 2<exp(1), this would be good! Dmitrii Kouznetsov 08:42, 4 February 2010 (UTC)

Disambig?

Mizar is also the name of a star, ζ Ursae Majoris. Peter Jackson 14:28, 29 January 2010 (UTC)

Yes, now is better. Thank you! Dmitrii Kouznetsov 04:31, 31 January 2010 (UTC)

An unclear sentence

I am not sure what this means: "the readers of the already existing programs could be used". That all existing libraries are loaded? --Peter Schmitt 11:00, 2 February 2010 (UTC)

Hello, Peter. I like that you divide the "examples" into subsections. I add one subsection more with some algebra.

I do not think that it is a good idea to load all the existing libraries.

First, there are too many, and it will take long time to copypast them all into the code, and even longer to mizf them. Second, I suspect, various libraries may use a little bit different notations, and this will cause problems. (Although I hope, the staff check the new programs for the compatibility of the notations). Perhaps, it is the "bottle neck" of the whole Mizar system, the lack of the service that searches for the appropriate library that reduces the number of the error messages at the processing.

Dmitrii Kouznetsov 02:35, 3 February 2010 (UTC)

Did you realize your names are the same? Peter Jackson 10:24, 4 February 2010 (UTC)