Principia Mathematica II ist ein Projekt, dem es darum geht, eine Art riesiges Mathematikbuch zu schaffen, in dem die ganzen Beweise in einer speziellen Formalen Sprachen formuliert sein sollen.
pmii will be a huge free mathematical online textbook collection. In the first phase we start collecting basic articles about axiomatic set theory, number theory and algebra. These articles will be presented under http://www.qedeq.org. The result of this phase should be a free collection of mathematical articles that cover the foundation of mathematics. In the next step these articles will be edited, cross linked, reorganized and transferred into a formal language. After that the articles will be also online published in PDF and HTML format.
Die eingegebenen Sätze und Axiome in dieser Sprache sollen dann die Basis für ein System zum automatischen Beweisen sein.
In the famous "Principia Mathematica" A.N. Whitehead and B. Russell tried to present mathematics in a fully formalized form. Goal of Principia Mathematica II (the title is a little bit arrogant.. ;-) is the creation of a system that enables a working mathematician to put theorems and proofs (in a formal language) into it. These proofs are automatically verified by a proof checker. Because this system is not centrally administrated and enables references to any location in the internet, a world wide mathematical knowledge base could be build. Any proof of a theorem in this "mathematical web" could be drilled down to the very elementary rules and axioms. To make it more than a huge number of correct formulas, it should also contain information in "common mathematical language". Think of an incredible number of mathematical textbooks with hyperlinks and each of its proofs could be verified by pmii. For each theorem the dependency of other theorems, definitions and axioms could be easily derived.
pmii will be a huge free mathematical online textbook collection. In the first phase we start collecting basic articles about axiomatic set theory, number theory and algebra. These articles will be presented under http://www.qedeq.org. The result of this phase should be a free collection of mathematical articles that cover the foundation of mathematics. In the next step these articles will be edited, cross linked, reorganized and transferred into a formal language. After that the articles will be also online published in PDF and HTML format.
Die eingegebenen Sätze und Axiome in dieser Sprache sollen dann die Basis für ein System zum automatischen Beweisen sein.
In the famous "Principia Mathematica" A.N. Whitehead and B. Russell tried to present mathematics in a fully formalized form. Goal of Principia Mathematica II (the title is a little bit arrogant.. ;-) is the creation of a system that enables a working mathematician to put theorems and proofs (in a formal language) into it. These proofs are automatically verified by a proof checker. Because this system is not centrally administrated and enables references to any location in the internet, a world wide mathematical knowledge base could be build. Any proof of a theorem in this "mathematical web" could be drilled down to the very elementary rules and axioms. To make it more than a huge number of correct formulas, it should also contain information in "common mathematical language". Think of an incredible number of mathematical textbooks with hyperlinks and each of its proofs could be verified by pmii. For each theorem the dependency of other theorems, definitions and axioms could be easily derived.
integrator - am Donnerstag, 27. Februar 2003, 13:30 - Rubrik: Matheseiten
m31 meinte am 21. Dez, 12:36:
Namensänderung auf "Hilbert II"
Der Projektname hat sich geändert, er lautet nun *Hilbert II*.Ziel des Projekts ist der dezentrale Zugang zu verifiziertem und lesbarem mathematischem Wissen. Dieses Projekt steht, wie der Name schon andeutet, in der Tradition von Hilberts Programm.
In *Hilbert II* werden mathematische Axiome, Definitionen und Sätze in sogenannten QEDEQ-Modulen zusammengefasst. Ein solches Modul kann auch als mathematisches Textbuch aufgefasst werden, das formal korrekte Beweise enthält. Durch die Verweismöglichkeit auf andere QEDEQ-Module kann im Internet ein riesiges mathematisches Wissensnetz aufgebaut werden.
