IsaMorph

IsaMorph är en Linux-distribution Live CD (baserat på Morphix) presenterar den interaktiva sats jäs Isabelle.
Detta innebär att du kan starta från CD och få en fullt fungerande "teorembevisning" miljö utan att installera GNU / Linux eller Isabelle. Sätt bara in CD-skivan i datorn och har fem minuter senare din första sats bevisats.
Alla program som distribueras inom IsaMorph är fri programvara. Detta innebär att operativsystemet och program som ingår i denna CD kan fritt kopieras, ändras och distribueras. Så är du välkommen att ge kopior till dina vänner eller kollegor.
Sätt i CD-skivan i cd-enheten på en Intel-kompatibel dator eller laptop. Nu starta om datorn. Se till att den första startenhet är CD. För detta kan du behöva ändra BIOS-inställningarna på din dator.
Om du inte är bekant med det, få hjälp från din systemadministratör eller någon som vet hur man gör det. När datorn startar uppstart, kommer det att söka efter en CD-skiva i enheten. En meny kommer att visas efter en viss tid.
Bara tryck på Enter eller vänta en tid. Datorn kommer att fortsätta att starta från cd och förhoppningsvis ge dig en grafisk skärm som liknar vad du är bekant med. Du kan klicka på menyn längst upp till vänster och starta program.
IsaMorph innehåller en fullt fungerande Isabelle miljö stödja bevis och dokumentgenerering, omfattar detta:
Isabelle (version 2005)
Den interaktiva sats jäs Isabelle 2005 åtminstone följande logik som sammanställts i: HOL, HOL-komplex, ZF, FOL och ren. Således, efter uppstart IsaMorph kan du genast bevisa satser i någon av dessa logiker. CD: n innehåller en offline version av Isabelles tutorials och teori dokumentation.
HOL-TestGen (version 1.1.1)
Ett testfall generator för specifikation baserad enhetstestning. Den är byggd på toppen av specfication och teorem bevisar miljö Isabelle / HOL.
Proof Allmänt (version 3.6pre)
En kraftfull användargränssnitt för Isabelle.
SML av New Jersey (version 110,56)
Standard ML miljö som används för att sammanställa och utföra Isabelle.
GNU Emacs (version 22.0.50)
GNU Emacs editor som bygger tillsammans med bevis generalhuvud användargränssnitt Isabelle.
teTeX (version 2.0.2)
En komplett Latex miljö som används för generering av korrektur dokument.
Andra applikationer
Dessutom CD innehåller också en mängd olika applikationer för en gemensam användning. Den innehåller ett användarvänligt skrivbordet (Gnome) en webbläsare (Mozilla), och så vidare. Ta bara en titt på menyn för att ta reda på många fler. Jag försökte minimera antalet icke Isabelle särskild programvara för att minimera hämtningsstorleken.
Vad är nytt i den här versionen: