| 词条 | QED manifesto |
| 释义 |
The QED manifesto was a proposal for a computer-based database of all mathematical knowledge, strictly formalized and with all proofs having been checked automatically. (Q.E.D. means {{lang|la|quod erat demonstrandum}} in Latin, meaning "which was to be demonstrated.") OverviewThe idea for the project arose in 1993, mainly under the impetus of Robert Boyer. The goals of the project, tentatively named QED project or project QED, were outlined in the QED manifesto, a document first published in 1994, with input from several researchers.[1] Explicit authorship was deliberately avoided. A dedicated mailing list was created, and two scientific conferences on QED took place, the first one in 1994 at Argonne National Laboratories and the second in 1995 in Warsaw organized by the Mizar group.[2] The project seems to have died in 1996, never having produced more than discussions and plans. In a 2007 paper, Freek Wiedijk identifies two reasons for the failure of the project.[3] In order of importance:
Nonetheless, QED-style projects are regularly proposed, and the Mizar library has successfully formalized a large portion of undergraduate mathematics. {{As of|2007}} it is the largest such library.[4] Another such project is the Metamath proof database. In 2014 the Twenty years of the QED Manifesto[5] workshop was organized as part of the Vienna Summer of Logic. See also
References1. ^The QED Manifesto in Automated Deduction - CADE 12, Springer-Verlag, Lecture Notes in Artificial Intelligence, Vol. 814, pp. 238-251, 1994. HTML version 2. ^The QED Workshop II report 3. ^Freek Wiedijk, The QED Manifesto Revisited, 2007 4. ^Fairouz Kamareddine, Manuel Maarek, Krzysztof Retel, and J. B. Wells, Gradual Computerisation/Formalisation of Mathematical Texts into Mizar 5. ^Twenty years of the QED Manifesto workshop Further reading
External links
4 : Educational projects|Formal methods|Mathematics literature|Proof assistants |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。