Talk:Mizar (software): Difference between revisions

From Citizendium
Jump to navigation Jump to search
imported>Dmitrii Kouznetsov
imported>Daniel Mietchen
({{subpages}})
Line 1: Line 1:
{{subpages}}
==Need more simple examples==
==Need more simple examples==
It would be good to add also examples that check simple relations, in particular,
It would be good to add also examples that check simple relations, in particular,

Revision as of 04:53, 29 January 2010

This article is developing and not approved.
 Main Article
 Discussion
Related Articles  [?]
Bibliography  [?]
External Links  [?]
Citable Version  [?]
 
To learn how to update the categories for this article, see here. To update categories, edit the metadata template.
 Definition:  A software package for automated verification of mathematical definitions and proofs. [d] [e]
Checklist and Archives
 Workgroup categories:  Computers and Mathematics [Categories OK]
 Talk Archive:  none  English language variant:  British English

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

Retrieved from "https://citizendium.org/wiki/index.php?title=Talk:Mizar_(software)&oldid=720427"