IsaMorph

IsaMorph er en Linux-distribution live cd (baseret på Morphix) byder den interaktive teorem prover Isabelle.
Det betyder, du kan starte fra cd'en og få et fuldt operationelt "bevisførelse" miljø uden at installere GNU / Linux eller Isabelle. Bare indsæt cd'en i din pc og har fem minutter senere din første sætning bevist.
Alle programmer fordelt inden IsaMorph er fri software. Det betyder, at operativsystemet og de programmer, der er indeholdt i denne cd kan frit kopieres, ændres og distribueres. Så er du velkommen til at give kopier til dine venner eller kollegaer.
Indsæt cd'en i cd-drevet på en Intel kompatibel pc eller laptop. Nu genstarte computeren. Sørg for, at den første startenhed er cd. Til dette, kan du nødt til at ændre BIOS-indstillingerne på din computer.
Hvis du ikke er fortrolig med det, få hjælp fra systemadministratoren eller nogen, der ved hvordan man gør det. Da computeren starter opstart, vil det søge efter en CD i drevet. En menu vises efter et stykke tid.
Bare tryk på Enter-tasten eller vente et stykke tid. Computeren vil fortsat starte fra cd og forhåbentlig give dig en grafisk skærm, der ligner det, du er fortrolig med. Du kan klikke på menuen øverst til venstre, og start programmer.
IsaMorph indeholder et fuldt fungerende Isabelle miljø understøtter bevise og dokumentere generation, dette inkluderer:
Isabelle (version 2005)
Den interaktive teorem prover Isabelle 2005 mindst følgende logikker udarbejdet i: HOL, HOL-Complex, ZF, FOL, og Pure. Således efter opstart IsaMorph kan du straks bevise teoremer i nogen af ​​disse logikker. Cd'en indeholder en offline version af Isabelle s tutorials og teori dokumentation.
HOL-TestGen (version 1.1.1)
En prøvesag generator til specifikation baseret test af enheder. Den er bygget på toppen af ​​specfication og teorem beviser miljø Isabelle / HOL.
Proof General (version 3.6pre)
En kraftfuld brugergrænseflade til Isabelle.
SMG of New Jersey (version 110,56)
Standard ML Miljø anvendes til at samle og udføre Isabelle.
GNU Emacs (version 22.0.50)
GNU Emacs editor, der bygger sammen med Proof General de vigtigste brugergrænseflade Isabelle.
teTeX (version 2.0.2)
En komplet LaTeX miljø anvendes til generering af bevis dokumenter.
Andre programmer
Derudover cd'en indeholder også en række applikationer til en fælles brug. Det omfatter en brugervenlig desktop (Gnome) en Internet browser (Mozilla), og så videre. Bare tag et kig på menuen for at finde ud mange flere. Jeg forsøgte at minimere antallet af ikke Isabelle specifik software for at minimere download størrelse.
Hvad er nyt i denne version: