Talk:Mizar (software): Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Dmitrii Kouznetsov
(New page: ==Need more simple examples== It would be good to add also examples that check simple relations, for example, 2>1 x^2=x*x ''Explain this to me on a simple example; the difficult exampl...)
 
imported>Dmitrii Kouznetsov
Line 10: Line 10:
It could be just a script that add and remove 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?
It could be just a script that add and remove 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?


[[User:Dmitrii Kouznetsov|Dmitrii Kouznetsov]] 05:23, 29 January 2010 (UTC)
[[User:Dmitrii Kouznetsov|Dmitrii Kouznetsov]] 05:23, 29 January 2010 (UTC)<br>
P.S. the { {subpages} } is not accepted...

Revision as of 23:27, 28 January 2010

Need more simple examples

It would be good to add also examples that check simple relations, for example,

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 http://israelmgelfand.com/edu_work.html

The guide for choice of the libraries seems to be absent. It could be just a script that add and remove 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...