5.1.4.3. משפט הנאותות של Hמשפט: אם ההוכחה תהיה באינדוקציה על מבנה ההוכחה ב-H. נראה שכל אחת מהאקסיומות תמיד נכונה. נראה כי לכל כלל היסק, אם מתקיים החלק העליון שבכלל, אזי מתקיים גם החלק התחתון. בסיס אם החישוב התחיל במצב לפי למת החישובים, החישוב היחיד שיש להשמה הוא החישוב הבא: צריך להוכיח כי כעת נבדוק עבור נשתמש שוב בלמת החישובים, ונראה כי צריך
להוכיח: הוכחת כללי ההיסק הרכבה סדרתית (SEQ): נתון: צ"ל: נשאל את עצמנו איזה סוג חישובים יש
להרכבה סידרתית לפי למת החישובים. ישנם חישובים מתבדרים וישנם חישובים עוצרים. המקרה
בו אנו מתעניינים עבור נכונות חלקית הוא מקרה שבו גם החלק עפ"י הנתון:
מ- לולאה (REP): נתון: צ"ל: למת החישובים: מעניין אותנו לבדוק חישובים שעוצרים, כי עבור חישובים שלא עוצרים הטענה נכונה באופן טריויאלי.
באינדוקציה על מספר ביצועי החוג, נראה
כי לכל בסיס: צ"ל כי צעד: נניח כי על פי עבור כלל CONS: נתון: צריך להוכיח: יהי על סמך נתון 2: על סמך נתון 3: על סמך טרנזיטיביות הגזירה נקבל: כלל COND: הכלל מוכח באופן דומה ל-SEQ. ההוכחה לא תוצג במסמך זה.
אין תגובות!
|
תוכן העניינים:
קישורים רלוונטיים:שיתוף: |