Hilbert II-prosjektet er desentralisert tilgang til verifisert og lesbar matematisk kunnskap. Som det navnet allerede antyder, er dette prosjektet i tradisjonen av Hilbert 's program.
Hilbert II ønsker å bli fri, world wide matematisk kunnskapsbase som inneholder matematiske teoremer og bevis i en formell riktig form. Alle som tilhører dokumentene er utgitt under GNU Free Documentation License.
Vi tar sikte på å tilpasse den felles matematisk argumentasjon til en formell syntaks. Det betyr, når i matematikk en viss form for argumentasjon brukes ofte vi ser frem til å integrere den i den formelle språket i Hilbert II. Denne formspråk kalles qedeq format.
Hilbert II gir et program suite som gjør at en matematiker til å sette teoremer og bevis til at kunnskapsbase. Disse bevisene blir automatisk verifisert av et bevis kontrolløren. Også tekster i "vanlig matematisk språk" kan integreres.
De matematiske aksiomer, definisjoner og påstander er kombinert til såkalte qedeq moduler. Slik modul kan bli sett på som en matematisk lærebok som inkluderer formelle korrekte bevis. Fordi dette systemet ikke er sentralt administrert og referanser til hvilket som helst sted på internett er mulig, kan en verdensomspennende matematisk kunnskapsbase være build.
Enhver bevis for et teorem i denne "matematisk web" kunne bli boret ned til svært elementære regler og aksiomer. Tenk på et utrolig antall matematiske lærebøker med hyperkoblinger og hver av sine bevis kan bli verifisert av Hilbert II. For hver teorem avhengigheten av andre teoremer, definisjoner og aksiomer kan være lett avledet
Det grunnleggende konseptet med dette prosjektet er publisert som PDF-dokument.: Grunnleggende konseptet. Dette dokumentet er allerede generert ut fra følgende XML-filen: qedeq_basic_concept.xml. Hovedprosjektet er i første develompment fase, se under utvikling.
Det finnes en fungerende prototype kalt Principia Mathematica II. Det er fullt i stand til første ordens predikatlogikk og viser de viktigste funksjonene og funksjonaliteten til Hilbert II. Det kan verifisere (prototype) qedeq modul filer plassert hvor som helst på internett.
Prototypen har en GUI og kan overføre qedeq moduler til HTML og LaTeX-filer. Du kan opprette og redigere din egen ny qedeq modul og publisere det på internett. I web allerede eksisterende qedeq moduler kan brukes bare ved å referere til dem
Hva er nytt i denne versjonen:.
Kommentarer ikke funnet