IsaMorph

IsaMorph είναι μια διανομή Linux Live CD (με βάση Morphix) που χαρακτηρίζει τη διαδραστική θεώρημα prover Isabelle.
Αυτό σημαίνει ότι, μπορείτε να εκκινήσετε από το CD και να πάρετε μια πλήρως λειτουργική "απόδειξης θεωρήματος" περιβάλλον χωρίς να εγκαταστήσετε το GNU / Linux ή Isabelle. Απλά τοποθετήστε το CD στον υπολογιστή σας και να έχετε πέντε λεπτά αργότερα το πρώτο θεώρημα σας αποδεδειγμένη.
Όλα τα προγράμματα που διανέμονται εντός IsaMorph είναι ελεύθερο λογισμικό. Αυτό σημαίνει ότι το λειτουργικό σύστημα και τις εφαρμογές που περιέχονται σε αυτό το CD μπορεί να αντιγραφεί ελεύθερα, να τροποποιηθεί και να διανεμηθεί. Επομένως, σας παρακαλώ αισθανθείτε ελεύθερος να δώσει αντίγραφα σε φίλους ή τους συναδέλφους σας.
Τοποθετήστε το CD στη μονάδα CD σε ένα συμβατό υπολογιστή ή το laptop της Intel. Τώρα κάντε επανεκκίνηση του υπολογιστή. Βεβαιωθείτε ότι η πρώτη συσκευή εκκίνησης είναι το CD. Γι 'αυτό, ίσως χρειαστεί να αλλάξετε τις ρυθμίσεις του BIOS του υπολογιστή σας.
Εάν δεν είστε εξοικειωμένοι με αυτό, ζητήστε βοήθεια από το διαχειριστή του συστήματος ή κάποιον που ξέρει πώς να το κάνουμε σας. Καθώς ξεκινά ο υπολογιστής εκκίνηση, θα ψάξει για ένα CD στη μονάδα. Ένα μενού θα εμφανιστεί μετά από κάποιο χρονικό διάστημα.
Απλά πατήστε το πλήκτρο Enter ή περιμένετε για κάποιο χρονικό διάστημα. Ο υπολογιστής θα συνεχίσει να εκκινήσετε από το CD και, ελπίζω, να σας δώσω μια γραφική οθόνη παρόμοια με αυτό που είστε εξοικειωμένοι με. Μπορείτε να κάνετε κλικ στο μενού στο πάνω αριστερά και αρχίστε εφαρμογές.
IsaMorph περιέχει ένα Isabelle περιβάλλον πλήρως λειτουργική υποστήριξη που αποδεικνύει και το έγγραφο γενιά, αυτό περιλαμβάνει:
Isabelle (έκδοση 2005)
Το διαδραστικό θεώρημα prover Isabelle 2005 με τουλάχιστον τις ακόλουθες λογικές καταρτίζονται: HOL, HOL-Complex, ZF, FOL, και καθαρό. Έτσι, μετά την εκκίνηση IsaMorph μπορείτε να αποδείξετε αμέσως θεωρήματα σε οποιαδήποτε από αυτές τις λογικές. Το CD περιλαμβάνει μια offline έκδοση των tutorials Isabelle και την τεκμηρίωση της θεωρίας.
HOL-TestGen (έκδοση 1.1.1)
Μια γεννήτρια δοκιμή για τις προδιαγραφές με βάση τις δοκιμές μονάδα. Είναι χτισμένο στην κορυφή του specfication και θεώρημα αποδεικνύει περιβάλλον Isabelle / HOL.
Απόδειξη Γενικά (έκδοση 3.6pre)
Ένα ισχυρό περιβάλλον εργασίας χρήστη για Isabelle.
ΟΕΙΜ του New Jersey (έκδοση 110.56)
Το Πρότυπο ML Περιβάλλοντος χρησιμοποιείται για την κατάρτιση και την εκτέλεση Isabelle.
GNU Emacs (έκδοση 22.0.50)
Ο συντάκτης GNU Emacs που χτίζει μαζί με την απόδειξη Γενικά η κύρια διεπαφή χρήστη της Ισαβέλλας.
teTeX (έκδοση 2.0.2)
Ένα πλήρες περιβάλλον LaTeX χρησιμοποιείται για την παραγωγή των εγγράφων απόδειξης.
Άλλες Εφαρμογές
Επιπλέον, το CD περιέχει επίσης μια ποικιλία εφαρμογών για την από κοινού χρήση. Περιλαμβάνει μια φιλική προς το χρήστη επιφάνεια εργασίας (Gnome) ένα πρόγραμμα περιήγησης στο Internet (Mozilla), και ούτω καθεξής. Απλά ρίξτε μια ματιά στο μενού για να μάθετε πολλά περισσότερα. Προσπάθησα να ελαχιστοποιηθεί ο αριθμός των μη Isabelle ειδικό λογισμικό για να ελαχιστοποιηθεί το μέγεθος λήψης.
Τι νέο υπάρχει σε αυτήν την έκδοση: