Wikipedia - Benutzerbeiträge [de]

Mizar-System

2012-07-24T17:08:22Z

Rschwieb: spelling

{{for|the star system|Mizar (star)}}
The '''Mizar system''' consists of a [[formal language]] for writing mathematical definitions and proofs, a [[proof assistant]] which is able to [[Automated proof checking|mechanically check]] proofs written in this language, and a library of [[mathematical formalization|formalized mathematics]] which can be used in the proof of new theorems.<ref name="A Brief Overview of Mizar">{{cite journal|last=Naumowicz|first=Adam|coauthors=Artur Korniłowicz|title=A Brief Overview of Mizar|journal=Theorem Proving in Higher Order Logics|year=2009|volume=5674|pages=67–72|series=Lecture Notes in Computer Science|url=http://www.springerlink.com/content/08138878w5n05278/}}</ref> The [[#Mizar Mathematical Library|Mizar Mathematical Library]] is the largest coherent body of strictly formalized mathematics in exsistence.<ref name="Arrow">{{cite journal|last=Wiedijk|first=Freek|title=Formalizing Arrow’s theorem|journal=Sadhana|year=2009|volume=34|pages=193–220|issue=1|url=http://www.springerlink.com/content/3607101377774154/}}</ref> The system is maintained and developed by the '''Mizar Project'''<ref name="The Mizar Project website">[http://www.mizar.org/ The Mizar Project website]</ref> under the direction of its founder [[Andrzej Trybulec]].

==Mizar Project==
The Mizar Project started around 1973 by [[Andrzej Trybulec]] as an attempt to reconstruct mathematical [[vernacular]] so it can be checked by a computer.<ref>{{cite journal|last=Matuszewski|first=Roman|coauthors=Piotr Rudnicki|title=Mizar: the first 30 years|journal=Mechanized Mathematics and Its Applications|year=2005|volume=4|url=http://markun.cs.shinshu-u.ac.jp/mizar/mma.dir/}}</ref> Its current goal, apart from the continual development of the Mizar System, is the collaborative creation of a large library of formally verified proofs, covering most of the core of modern mathematics. This is in-line with the influential [[QED manifesto]].<ref>{{cite web|last=Wiedijk|first=Freek|title=Mizar|url=http://www.cs.ru.nl/~freek/mizar/|accessdate=July 2012}}</ref>

Currently the project is developed and maintained by research groups at [[Białystok University]], Poland, the [[University of Alberta]], Canada, and [[Shinshu University]], Japan. While the Mizar proof checker remains proprietary,<ref name="not-open-source">[http://old.nabble.com/TPHOLs-becomes-ITP-%28fwd%29-td19435554.html#a19493250 Mailing list discussion] referring to the close-sourcing of Mizar.</ref> the sizable body of formalized mathematics that it verified, the [[#Mizar Mathematical Library|Mizar Mathematical Library]], is licensed open-source.<ref name="library-open-source">[http://mizar.uwb.edu.pl/forum/archive/1104/msg00000.html Mailing list announcement] referring to the open-sourcing of MML.</ref>

Papers related to the Mizar system regularly appear in the peer-reviewed journals of the formal mathematics academic community. These include ''[[Studies in Logic, Grammar and Rhetoric]]'', ''[[Intelligent Computer Mathematics]]'', ''[[Interactive Theorem Proving]]'' and the ''[[Journal of Formalized Reasoning]]''.

==Mizar Language==
The distinctive feature of the '''Mizar Language''' is its readability. As is common in mathematical text, it relies on [[classical logic]] and a [[declarative programming|declarative style]].<ref>{{cite journal|last=Geuvers|first=H.|title=Proof assistants: History, ideas and future|journal=Sadhana|year=2009|volume=34|issue=1|url=http://www.springerlink.com/content/u7tn18130148t65m/}}</ref> Mizar articles are written in ordinary [[ASCII]], but the language was designed to be close enough to the mathematical vernacular that most mathematicians could read and understand Mizar articles without special training.<ref name="A Brief Overview of Mizar"/> Yet, the language enables the increased level of formality necessary for [[automated proof checking]].

For a proof to be admitted, all steps have to be justified either by elementary logical arguments or by citing previously verified proofs.<ref>{{cite journal|last=Wiedijk|first=Freek|title=Formal Proof--Getting Started|journal=AMS Special Issue on Formal Proof|year=2008|url=http://www.ams.org/notices/200811/index.html}}</ref> This results in a higher level of rigor and detail than customary in mathematical text-books and publications. Thus, a typical Mizar article is about four times as long as an equivalent paper written in ordinary style.<ref>{{cite web|last=Wiedijk.|first=Freek|title=The "de Bruijn factor"|url=http://www.cs.ru.nl/~freek/factor/index.html|accessdate=July 2012}}</ref>

Formalization is relatively labor intensive, but not impossibly difficult. Once one is versed in the system, it takes about one week of full time work to have a text-book page formally verified. This suggests that its benefits are now in the reach of applied fields such as [[probability theory]] and [[economics]].<ref name="Arrow"/>

==Mizar Mathematical Library==
The '''Mizar Mathematical Library''' ('''MML''') includes all theorems which can be referred in newly written articles. Once approved by the proof checker they are further evaluated in a process of [[peer-review]] for appropriate contribution and style. If accepted they are published in the associated ''Journal of Formalized Mathematics''<ref name="Journal of Formalized Mathematics">[http://fm.mizar.org/ Journal of Formalized Mathematics]</ref> and added to the MML.

===Breadth===
As of July 2012, the MML included 1150 articles written by 241 authors.<ref name="MML Query">[http://mmlquery.mizar.org The MML Query search engine]</ref> In aggregate, these contain more than 10,000 formal definitions of mathematical objects and about 52,000 theorems proved on these objects. More than 180 named mathematical facts have so benefited from formal codification.<ref name="MML facts">{{cite web|title=A list of named theorems in the MML|url=http://mmlquery.mizar.org/mmlquery/fillin.php?filledfilename=mml-facts.mqt&argument=number+102|accessdate=July 2012}}</ref> Some examples are the [[Hahn–Banach theorem]], [[König's lemma]], [[Brouwer fixed point theorem]], [[Gödel's completeness theorem]] and [[Jordan curve theorem]].

This breath of coverage has led some<ref>{{cite journal|last=Wiedijk|first=Freek|title=The QED Manifesto Revisited|journal=From Insight to Proof: Festschrift in Honour of Andrzej Trybulec|year=2007|volume=10|series=Studies in Logic Grammar and Rhetoric|issue=23|url=http://logika.uwb.edu.pl/studies/vol23.html}}</ref> to suggest Mizar as one of the leading approximations to the [[QED manifesto|QED utopia]] of encoding all core mathematics in computer verifiable form.

===Availability===
All MML articles are available in [[PDF]] form as the papers of the ''Journal of Formalized Mathematics''.<ref name="Journal of Formalized Mathematics"/> The full text of the MML is distributed with the Mizar checker and can be freely downloaded from the Mizar website.<ref name="The Mizar Project website" /> In an on-going recent project<ref>[http://foundations.cs.ru.nl/fndswiki/Research/MathWiki The MathWiki project homepage]</ref> the library was also made available in an experimental [[wiki]] form<ref name="MML wiki">[http://mws.cs.ru.nl/mwiki/ The MML in wiki form]</ref> that only admits edits when they are approved by the Mizar checker.<ref>{{cite journal|last=Alama|first=Jesse|coauthors=Kasper Brink, Lionel Mamane and Josef Urban|title=Large Formal Wikis: Issues and Solutions|journal=Intelligent Computer Mathematics|year=2011|volume=6824|series=Lecture Notes in Computer Science|pages=133–148|url=http://www.springerlink.com/content/qm3203471p33w271/}}</ref>

The '''MML Query''' website<ref name="MML Query"/> implements a powerful search engine for the contents of the MML. Among other abilities, it can retrieve all MML theorems proved about any particular type or operator.<ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(symbol+to_power+|+notation+|+constructor+|+occur+|+th)+ordered+by+number+of+ref An example of an MML query], yielding all theorems proved on the [[exponent]] operator, by the number of times they are cited in subsequent theorems.</ref><ref>[http://mmlquery.mizar.org/cgi-bin/mmlquery/emacs_search?input=(atleast+*+(+PROB_1:modenot+3+ref)+{{!}}+th)+ordered+by+number+of+ref Another example of an MML query], yielding all theorems proved on [[sigma field|sigma-fields]].</ref>

===Logical structure===
The MML is built on the axioms of the [[Tarski-Grothendieck set theory]]. Even though semantically [[implementation of mathematics in set theory|all objects are sets]], the language allows one to define and use [[weak typing|syntactical weak types]]. For example, a set may be declared to be of type '''Nat''' only when its internal structure conforms with a particular list of requirements. In turn, this list serves as the definition of the [[natural numbers]] and the set of all the sets that conform to this list is denoted as '''NAT'''.<ref>{{cite journal|last=Grabowski|first=Adam|coauthors=Artur Kornilowicz, Adam Naumowicz|title=Mizar in a Nutshell|journal=Journal of Formalized Reasoning|year=2010|volume=3|issue=2|pages=152–245|url=http://jfr.unibo.it/article/view/1980}}</ref> This implementation of types seeks to reflect the way most mathematicians formally think of symbols<ref>{{cite book|last=Taylor|first=Paul|title=Practical Foundations of Mathematics|year=1999|publisher=Cambridge University Press|isbn=9780521631075|url=http://www.cs.man.ac.uk/~pt/Practical-Foundations/html/}}</ref> and so streamline codification.

==Mizar Proof Checker==
Distributions of the '''Mizar Proof Checker''' for all major operating systems are freely available for downloaded at the Mizar Project website.<ref name="The Mizar Project website" /> Use of the proof checker is free for all non-commercial purposes. It is written in [[Free Pascal]] and the source code is available to all members of the Association of Mizar Users.<ref name="The Association of Mizar Users website">[http://mizar.uwb.edu.pl/sum/ The Association of Mizar Users website]</ref>

== See also ==
* [[Automated proof checking]]
* [[Proof assistant]]
* [[QED manifesto]]

==References==
{{reflist|2}}

==External links==
*{{official|http://www.mizar.org/}}

[[Category:Large-scale mathematical formalization projects]]
[[Category:Proof assistants]]
[[Category:Dependently typed languages]]
[[Category:Educational math software]]
[[Category:Mathematical societies]]

[[it:Sistema Mizar]]
[[ja:Mizar]]
[[pl:System Mizar]]

Mizar-System

2012-07-24T17:08:22Z

Rschwieb: spelling

Eulerkraft

2012-04-05T20:10:14Z

Rschwieb: /* Euler Force Example */ ce

In [[classical mechanics]], the '''Euler acceleration''' (named for [[Leonhard Euler]]), also known as '''azimuthal acceleration'''<ref name=Morin>{{cite book |author=David Morin |url=http://books.google.com/books?id=Ni6CD7K2X4MC&pg=PA469&dq=acceleration+azimuthal+inauthor:Morin&lr=&as_brr=0 |title=Introduction to classical mechanics: with problems and solutions |page= 469 |isbn= 0521876222 |year=2008 |publisher=Cambridge University Press}}</ref> or '''transverse acceleration'''<ref name=Fowles>{{cite book |author=Grant R. Fowles and George L. Cassiday|title=Analytical Mechanics, 6th ed.|page=178|year=1999|publisher=Harcourt College Publishers}}</ref> it is the [[Fictitious force|fictitious]] tangential force that is felt as a result of any radial acceleration. In other words, is an [[acceleration]] that appears when a non-uniformly [[rotating reference frame]] is used for analysis of motion and there is variation in the [[angular velocity]] of the [[frame of reference|reference frame]]'s axes. This article is restricted to a frame of reference that rotates about a fixed axis.

The '''Euler force''' is a [[fictitious force]] on a body that is related to the Euler acceleration by ''' ''F'' ''' = ''m'' ''' ''a'' ''', where ''' ''a'' ''' is the Euler acceleration and ''m'' is the mass of the body.<ref name=Battin>{{cite book |title=An introduction to the mathematics and methods of astrodynamics |page=102 |author= Richard H Battin |url=http://books.google.com/books?id=OjH7aVhiGdcC&pg=PA102&vq=Euler&dq=%22Euler+acceleration%22&lr=&as_brr=0&source=gbs_search_s&sig=ACfU3U0__alj4q5o16OHM8vGvArm0rqMdg
|isbn=1563473429 |year=1999 |publisher=American Institute of Aeronautics and Astronautics |location=Reston, VA }}</ref><ref>{{cite book |title=Introduction to Mechanics and Symmetry: A Basic Exposition of Classical Mechanical Systems |author=Jerrold E. Marsden, Tudor S. Ratiu |isbn=038798643X |year=1999 |publisher=Springer |page=251 |url=http://books.google.com/books?id=I2gH9ZIs-3AC&pg=PP1&dq=isbn:038798643X&sig=tDWUiGpvGVpbRCCQcGK0Bx5Yk3g#PPA251,M1}}</ref>

==Euler Force Example==
{{Main|Rotating reference frame}}
For person on a merry-go-round, as the ride starts, the Euler force will be the apparent force pushing the person to the back of the horse, and as the ride comes to a stop, it will be the apparent force pushing the person towards the front of the horse. The Euler force is perpendicular to the [[Centrifugal force (fictitious)|centrifugal force]] and is in the plane of rotation.

==Euler acceleration==
{{Main|Rotating reference frame}}
The direction and magnitude of the Euler acceleration is given by:
:<math>
\boldsymbol{a}_\mathrm{Euler} =
- \frac{d\boldsymbol\omega}{dt} \times \mathbf{r}
</math>

where:
:'''''ω''''' is the angular velocity of rotation of the reference frame;
:'''''r''''' is the vector position of the point where the acceleration is measured relative to the axis of the rotation.

==Euler force==
Using the above acceleration, the Euler force is:
:<math>
\boldsymbol{F}_\mathrm{Euler} =
m \boldsymbol{a}_\mathrm{Euler} =
- m \frac{d\boldsymbol\omega}{dt} \times \mathbf{r} \ ,
</math>

where:
:''m'' is the [[mass]] of the object upon which this [[fictitious force]] is exerted.

==See also==
*[[Fictitious force]]
*[[Coriolis effect]]
*[[Centrifugal force]]
*[[Rotating reference frame]]
*[[Angular acceleration]]

==Notes and references==
<references/>

[[Category:Fictitious forces]]
[[Category:Rotation]]

{{classicalmechanics-stub}}

[[ar:قوة أويلر]]
[[cs:Eulerova síla]]
[[da:Vinkelaccelerationskraft]]
[[es:Fuerza de Euler]]
[[pl:Transwersalna siła bezwładności]]
[[pt:Força de Euler]]
[[zh:欧拉力]]