תרגול 1 - 3.3.09

• פרטים טכניים
• מה זה לוגיקה?
• השפה הפורמלית של תחשיב הפסוקים הקלאסי
• הצרנה
• דוגמא לכיצד מוכיחים שמשהו הוא נוסחה או לא נוסחה

שיעור 1 - 8.3.09

• פרטים טכניים, קצת היסטוריה והכלים שהקורס אמור לתת לנו
• הרכיבים העיקריים של מערכת לוגית (שפה פורמלית ויחס נביעה)
• הצרנה
• תחשיב הפסוקיפ הקלאסי: השפה שלו, יחס הנביעה שלו.
• דוגמא להוכחת טענה (בשתי צורות) [נמצא בין השפה ליחס הנביעה של תחשיב הפסוקים הקלאסי]

שיעור 2 - 15.3.09

• בילבולים אפשריים מהשיעור הקודם
• טענות על תחשיב הפסוקים הקלאסי
• משפט ההצבה
• הוכחת נביעה על ידי רדוקציה לטאוטולוגיה
• משפט הדדוקציה הסמנטי
• הוכחת נביעה על ידי רדוקציה לספיקות
• משפט הקומפקטיות - הצגת שתי הגדרות שקולות (והוכחת אחת על ידי השניה)
• כמה מילים על כריעות של בעיה הנביעה

תרגול 2 - 17.3.09

• הגדרה שונה מהשיעור להשמה והוכחת שקילות
• מושגים סמנטיים חשובים (מודל, יחס נביעה, ספיקות, טאוטולוגיה, סתירה, שקילות לוגית)
• איך בודקים טאוטולוגיה, ספיקות, נביעה
• טענה המקשרת בין נביעה לספיקות (והוכחתה)
• הצגת משפט הדדוקציה ועוד טענה דומה
• תרגילי הוכח / הפרך
• תרגיל שמלמד על סוג של בניה של השמה

שיעור 3 - 22.3.09
השיעור הכרנו מערכות הוכחה.

• הגדרת HPC (ודוגמא להוכחה בו)
• משפט התקפות של HPC (כיוון אחד של שקילות יחסי הנביעה של CPL ו-HPC) והוכחתו
• משפט הדדוקציה של HPC והוכחתו
  • הכללה
• הגדרת HPI
• הצגת משפט השלמות של HPC (כיוון שני של שקילות יחסי הנביעה של CPL ו-HPC)

תרגול 3 - 24.3.09

• הגדרת: HPC, הוכחה, ומשפט
• תכונות של הוכחות במערכת HPC
• יכיחות מתורה גדולה יותר
• משפט הדדוקציה ודוגמא לשימוש בו
• תרגיל שקילות בין מערכות
• הצבה שומרת יכיחות

שיעור 4 - 29.3.09

• הוכחת משפט השלמות
  • הסבר אינטואיבי להוכחה
  • הגדרת Ti ו- 3 עובדות ברורות עליהן
  • הגדרת *T ו- 4 תכונות שלה
  • למה עיקרית (פי ב-*T <==> פי יכיח מ- *T) והוכחתה
  • סיום הוכחת המשפט
• רווחים מהוכחת המשפט
• הגדרת קונסיסטנטיות
  • שקילות לאי-טריוויאליות
• התחלת דיבור על מערכות מתקדמות יותר

תרגול 4 - 31.3.09

• הגדרת תחשיב חדש F והוכחה באינדוקציה שמשפטיו הן נוסחאות של *HPC
• תרגיל ממבחן: אם כל תת-גרף סופי הוא k-צביע, הגרף כולו הוא k-צביע (ע"י שימוש במשפט הקומפקטיות)

שיעור 5 - 19.4.09

• סיום הפתיחה משיעור שעבר ובעקבותה הצגת מערכת NDC
• הגדרת סקוונט
• האקסיומה וכללי ההיסק של מערכת NDC ו- NDI
• הגדרת נביעה ב- NDC
• משפט התקפות של NDC
• צורות הוכחה ב- NDC ודוגמאות
• הוכחה בשלילה (ההבדל בין NDC ל- NDI)

תרגול 5 - 21.4.09

• הגדרת מערכת NDC
• משפט התקפות של NDC
• תרגילים הוכחה ב- NDC
• תרגיל: הוכחת שקילות בין מערכת NDC ל- 'NDC

שיעור 6 - 26.4.09

• הוכחת שיוויון יחסי הנביעה של NDC ו-HPC
• שקילות לוגית
  • הגדרה
  • טענה: הצבת נוסחאות שקולות בנוסחא שומרת שקילות
  • הוכחת הטענה גם עבור HPI
• שקילויות חשובות
• צורות נורמליות (nnf, CNF, DNF) של נוסחאות
  • ניתן להציג כל נוסחא בצורה נורמלית
• אוניברסליות הקשרים שלנו

תרגול 6 - 30.4.09

• ‫משפט הצבת אקוויוולנטים‬
• ‫שקילויות חשובות‬
• CNF, DNF ומה שביניהם
  • חידון הנוסחאות הגדול
  • כל פונ' ניתן להביע באמצעות נוסחת CNF ונוסחת DNF
• ‫שלמות פונקציונלית‬
  • הוכחת שלמות פונקציונלית
  • הוכחת אי-שלמות פונקציונלית

שיעור 7 - 3.5.09

• לוגיקה רב ערכית
  • הגדרת שלושה סוגי חישובים (להוט, עצל, ועצל מקבילי) וטבלאות אמת מתאימות
  • הגדרה של לוגיקה רב ערכית
  • שימוש של לוגיקה רב ערכית: הוכחה כי חוק פירס לא יכיח ב- HPI
  • כמה מילים על לוגיקה עמומה
• ‫תחשיב הפרדיקטים - לוגיקה מסדר ראשון‬
  • א"ב של השפה (המשותף לכל השפות והסיגנטורה)
  • השפה המושרית על ידי סיגנטורה - שמות העצם והנוסחאות בה.
  • הגדרת מבנה

תרגול 7 - 5.5.09

• ‫לוגיקה רב ערכית
  • הגדרת לוגיקה רב ערכית והשמה בה
  • דוגמא: הלוגיקה הרב ערכית של גדל
  • אי נביעת N2 ב-HPC בלוגיקה של גדל
• ‫לוגיקה מסדר ראשון‬
  • מוטיבציה
  • הגדרת הא"ב של השפה
  • הגדרת שמות העצם והנוסחאות בשפה
  • הצרנות

שיעור 8 - 10.5.09

• הבנת המושג "נכון" (זהות מול משוואה)
• הגדרות בסיסיות
  • מבנה
  • השמה
• יחסים
  • יחס הנכונות
  • יחס התקפות
• משתנה חופשי וקשור
  • הגדרה
  • למה: המשתנים החופשיים הם היחידים שמשפיעים על סיפוק הנוסחא (ניסוח לא פורמלי)

תרגול 8 - 12.5.09

• ‫סמנטיקה של FOL
  • הגדרת מבנה
  • הגדרת השמה
  • הגדרת x-וריאנט
  • הגדרת יחס הסיפוק
  • הגדרת ספיקות, תקפות במבנה ותקפות לוגית
• קבוצת המשתנים החופשיים
  • הגדרת הקבוצה
  • הגדרת שם עצם סגור
  • הגדרת פסוק
• תרגילי תקפות לוגית

שיעור 9 - 17.5.09

• אזהרה לגבי מושג הספיקות ב- FOL מול המושג בתחשיב הפסוקים
• הגדרת יחסי הנביעה ב- FOL
  • איזה יחס מבין שניהם יותר חזק?
  • רדוקציות ביניהם
  • תכוניות יחודיות לכל יחס
    • v-נביעה: כלל הכללה, נביעה בכלל ההצבה
    • t-נביעה: משפט הדדקוציה

תרגול 9 - 19.5.09

• חזרה על הגדרות ספיקות ונביעה
• הבחנה בין יחסי הנביעה (מי גורר את מי)
• תרגילים
  • v-ספיקות גוררת t_ספיקות אבל לא להיפך
  • הקשר בין v-נביעה לאי-ספיקות
  • כלל הדדקוציה נכון ב- t-נביעה אך לא ב- v-נביעה
• הצבה של שם עצם במקום משתנה חופשי
  • משפט ההחלפה עבור שמות עצם

שיעור 10 - 24.5.09

• משפט ההצבה והוכחתו
• כריעות - תקפות מול אי-תקפות
• תחשיבים עבור FOL
  • דדקוציה טבעית - עבור t-נביעה
    • סכימת הוכחה לדוגמא
  • הילברט - עבור v-נביעה
    • סכימת הוכחת משפט התקפות עבורו

תרגול 10 - 26.5.09

• הצבות לא חוקיות - התייחסות קלה
• NDFOL
  • הצגה
  • 2 תרגילי הוכחה "פשוטים"
  • הוכחת תרגיל "אמיתי"
• HFOL
  • הצגה
  • תרגיל הוכחת שקילות מערכות

שיעור 11 - 31.5.09

• משפט הדדוקציה של HFOL (עם דיון מקדים)
• שקילות הנביעה הלוגית של HFOL ו- NDFOL
• תחילת הוכחת משפט השלמות של HFOL
  • מרחב הרברנד
  • מבנה הרברנד
  • 5 טענות על מבנה הרברנד

תרגול 11 - 2.6.09

• למה להעברת משפטים של HPC ל- HFOL
• תרגילי הוכחה ב- HFOL
• הסגור ותרגיל עליו
• תרגיל על הרחבת שפה
• PNF - צורה פרנקסית נורמלית

שיעור 12 - 7.6.09

• סריקת ההוכחה של משפט השלמות של HFOL
• מסקנות ואפליקציות מהמשפט
  • משפט הקומפקטיות עבור HFOL

    אי יחידות המודל עבור אקסיומות של תורת המספרים

  • משפט סקולם לוונהיים
  • משפט הרברנד

תרגול 12 - 9.6.09

• תרגילים על מבנה הרברנד
• תרגיל על שימוש במשפט הרברנד (ומשפט סקולם)
• תרגיל על משפט הקומפקטיות

שיעור 13 - 12.6.09

• משפט החלפת אקוויולנטים
• משפט סקולם
• לוגיקה מסדר ראשון עם שוויון
  • הגדרה
  • שקילות בינה לבין לוגיקה מסדר ראשון

שיעור 14 - 14.6.09
סיכום השיעור על ידי מיכל

תרגול 13 - 16.6.09

• כמה מילים על המבחן
• לוגיקה מסדר ראשון עם שוויון
  • הגדרה
  • תרגיל לגבי מבנים נורמליים
  • דדוקציה טבעית עם שוויון
  • משפט לבנהיים סקולם
• שפה רב סוגית
  • הגדרה
  • דוגמא לשימוש

תרגול 14 - 24.6.09

• 6 תרגילי מבחן

נמצא כאן סיכום מאוד מאוד נקודתי של החומר.
סיכום התרגול