IsaMorph הוא תקליטור הפצה של Linux Live (המבוסס על Morphix) המציג את prover המשפט האינטראקטיבי איזבל.
משמעות הדבר היא, שאתה יכול לבצע אתחול מהתקליטור ולקבל סביבה מבצעית מלא "הוכחת משפט" מבלי להתקין גנו / לינוקס או איזבל. רק הכנס את התקליטור במחשב שלך ויש לי חמש דקות מאוחר יותר המשפט הראשון שלך מוכח.
כל התוכניות מופצות בIsaMorph הן תוכנה חופשית. משמעות דבר היא שמערכת ההפעלה והיישומים הכלולים בתקליטור זה יכול להיות מועתקת באופן חופשי, שונה והפיצו. אז אל תהסס לתת עותקים לחברים או העמיתים לעבודה שלך.
הכנס את התקליטור לכונן תקליטורים במחשב אישי או נייד תואמים אינטל. עכשיו לאתחל את המחשב. ודא שהתקן האתחול הראשון הוא CD. לשם כך, ייתכן שתצטרך לשנות את הגדרות ה- BIOS של המחשב שלך.
אם אתה לא מכיר אותו, לקבל עזרה ממנהל המערכת או מישהו שיודע איך לעשות את זה שלך. כמחשב מתחיל אתחול, זה יהיה לחפש את תקליטור בכונן. תפריט יופיע לאחר זמן מה.
פשוט לחץ על מקש Enter או לחכות לכמה זמן. המחשב ימשיך אתחול מהתקליטור ו, בתקווה, ייתן לך מסך גרפי דומה למה שאתה מכיר. אתה יכול ללחוץ על התפריט בפינה השמאלית העליונה ולהפעיל יישומים.
IsaMorph מכיל סביבת איזבל עובד באופן מלא תמיכה בדור הוכחה ומסמך, זה כולל:
איזבל (גרסה 2005)
Prover המשפט האינטראקטיבי איזבל 2005 עם לפחות ההיגיון הבא נערך ב: HOL, HOL-Complex, ZF, תחשיב היחסים, וטהור. לפיכך, לאחר אתחול IsaMorph אתה יכול להוכיח באופן מיידי בכל משפטים של הגיונות אלה. התקליטור כולל גרסה מקוונת של הדרכות של איזבל ותיעוד התאוריה.
HOL-TestGen (גרסה 1.1.1)
מקרה מבחן גנרטור לבדיקת יחידת מפרט מבוסס. היא בנויה על גבי הסביבה מוכיחה specfication ומשפט איזבל / HOL.
כללי הוכחה (3.6pre גרסה)
ממשק משתמש רב עוצמה לאיזבל.
SML של ניו ג'רזי (גרסה 110.56)
תקן ML איכות הסביבה המשמשת לעריכה והוצאה לפועל איזבל.
GNU Emacs (גרסה 22.0.50)
עורך GNU Emacs אשר בונה יחד עם גנרל הוכחת ממשק המשתמש העיקרי של איזבל.
teTeX (גרסה 2.0.2)
סביבת LaTeX מלאה המשמשת לייצור מסמכי הוכחה.
יישומים אחרים
בנוסף, CD מכיל גם מגוון רחב של יישומים לשימוש נפוץ. הוא כולל שולחן עבודה ידידותי למשתמש (Gnome) דפדפן אינטרנט (Mozilla), וכן הלאה. רק תסתכל על התפריט כדי לגלות עוד רב. ניסיתי לצמצם את המספר של תוכנה ספציפית שאינו איזבל כדי למזער את גודל ההורדה.
מה חדש במהדורה זו:
תגובות לא נמצא