Hilbert II-project is gedecentraliseerd toegang tot geverifieerde en leesbaar wiskundige kennis. Zoals de naam al doet vermoeden, is dit project is in de traditie van het Programma van Hilbert.
Hilbert II wil een gratis, wereldwijd wiskundige kennis die wiskundige stellingen en bewijzen in een formele juiste vorm bevat geworden. Alle behorende documenten worden gepubliceerd onder de GNU Free Documentation License.
Wij streven ernaar om de wiskundige argumentatie aan te passen aan een formele syntax. Dat betekent dat, wanneer in de wiskunde een bepaald soort argumentatie wordt vaak gebruikt zullen we uitkijken naar het in de formele taal van Hilbert II integreren. Deze formele taal heet de qedeq formaat.
Hilbert II biedt een programma suite die een wiskundige in staat stelt om stellingen en bewijzen in die kennisbasis te zetten. Deze bewijzen worden automatisch gecontroleerd door een bewijs checker. Ook teksten in "wiskundige taal" kan worden geïntegreerd.
De wiskundige axioma's, definities en stellingen worden gecombineerd om zogenaamde qedeq modules. Een dergelijke module kan worden beschouwd als een mathematische tekstboek formeel correct bewijzen omvat. Omdat dit systeem is niet centraal beheerd en verwijzingen naar elke locatie op het internet mogelijk zijn, zou een wereldwijde wiskundige kennis op te bouwen zijn.
Elke bewijs van een stelling in deze "wiskundige web" kon worden geboord tot in de elementaire regels en axioma's. Denk aan een ongelooflijk aantal wiskundige schoolboeken met hyperlinks en elk van haar bewijzen konden worden geverifieerd door Hilbert II. Voor elke stelling van de afhankelijkheid van andere stellingen, definities en axioma's gemakkelijk kunnen worden afgeleid
Het basisconcept van dit project is gepubliceerd als PDF-document:. Basisconcept. Dit document is al gegenereerd uit de volgende XML-bestand: qedeq_basic_concept.xml. Het belangrijkste project is in de eerste develompment fase, zie in ontwikkeling.
Er bestaat een werkend prototype genaamd Principia Mathematica II. Het is volledig in staat van eerste orde predikatenlogica en toont de belangrijkste functies en functionaliteit van Hilbert II. Het kan controleren (prototype) qedeq module bestanden overal gevestigd in het internet.
Het prototype heeft een GUI en kan qedeq modules omzetten in HTML en LaTeX-bestanden. U kunt maken en je eigen nieuwe qedeq module bewerken en te publiceren op het internet. In het web kon reeds bestaande qedeq modules enkel gebruikt worden door te verwijzen naar hen
Wat is nieuw in deze release:.
Reacties niet gevonden