לוגיקה למדעי המחשב

תשפ״ג

• אוסף מבחנים ופתרונות ←

  אוסף מבחנים ופתרונות של אלכסנדר רבינוביץ׳

תשע״ז

• תרגול 1 ←

  דיון לא פורמלי על השפה הפורמלית
  הצרנה
  נוסחאות חוקיות

• הרצאה 1 ←

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

• תרגול 2 ←

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

• הרצאה 2 ←

  משפט כריעות יחידה
  הצבה בנוסחה
  מושגים סמנטיים בסיסיים

• תרגול 3 ←

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

• הרצאה 3 ←

  תחביר
  תורת ההוכחות
  תחשיב הילברט לתורת הפסוקים

• תרגול 4 ←

  שלמות פונקציונאלית
  צורות נורמליות CNF,DNF
  מערכת הוכחה בסגנון הילברט (לא סיימנו)

• הרצאה 4 ←

  הוכחות בHPC
  משפטים על הוכחות

• תרגול 5 ←

  תרגול בנושא HPC נאותות ושלמות
  נביעה לוגית ויכיחות

• הרצאה 5 ←

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

• תרגול 6 ←

  המשך שלמות ונאותות
  השפה הפורמלית

• הרצאה 6 ←

  סמנטיקה
  משפט sanity test
  שקילויות

• תרגול 7 ←

  מושגים במשתנים
  פירוש לסימונים
  הגדרות -  ספיקות, נכונות, תקפות

• תרגול 8 ←

  שיקלות בין נוסחאות
  t-נביעה ו v-נביעה

• תרגול 9 ←

  PNF
  אלגוריתם סקולהם
  מבנה הרברנד וground instances

• תרגול 10 ←

  תרגילים על הרברנד וסקולהם

• תרגול 11 ←

  קומפקטיות
  הרחבה אלמנטרית

• תרגול 12 ←

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

תשע״ו

• הרצאה 1 ←

  נושאים מנהליים
  מה זה לוגיקה?
  XB,F : יחידות ומינימליות
  משפט ההוכחה באינדוקציה

• תרגול 1 ←

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

• הרצאה 2 ←

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

• תרגול 2 ←

  תחשיב הפסוקים - Well-Formed Formats (WFF)
  עוד תכונות של WFF
  הסמנטיקה של תחשיב הפסוקים
  תרגילים

• הרצאה 3 ←

  מושגים סמנטיים עבור קבוצות פסוקים
  תכונות של גרירה לוגית
  צורות נורמליות:
  
  Negation Normal Form
  Conjuctive Normal Form
  Disjunctive Normal Form
  
  סמנטיקה של תחשיב הפסוקים כמשחק

• תרגול 3 ←

  תזכורת: משפט התלות הסופית
  קבוצות קשרים שלמות
  תרגילים בטאוטולוגיות, סתירות וגרירות לוגיות

• הרצאה 4 ←

  מערכת ההוכחה HPC
  אקסיומות וכללי היסק
  תכונות של מערכת הוכחה
  משפט הדדוקציה
  משפט הדיכוטומיה
  הוכחת נאותות של HPC, התחלה של הוכחת שלמות

• תרגול 4 ←

  דוגמאות על כללי היסק
  דוגמאות על קבוצות עקביות
  מסקנות ממשפט הנאותות

• תרגול 5 ←

  (לא היתה הרצאה בשבוע 5)
  
  תזכורת של מערכת ההוכחה HPC
  תרגילים על מערכות הוכחה

• הרצאה 5 ←

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

• תרגול 6 ←

  משפט הקומפקטיות
  משפט Erdos-DeBnjin על צביעה של גרף
  תרגילים סביב משפט הקומפקטיות

• הרצאה 6 ←

  הלמה של Kunig
  גדירות
  גדירות באופן סופי
  לוגיקה מסדר ראשון - תחביר

• תרגול 7 ←

  תרגילים על גדירות

• הרצאה 7 ←

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

• תרגול 8 ←

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

• הרצאה 8 ←

  T-נביעה מול V-נביעה
  הצבות מותרות
  החלפת שמות למשתנים
  צורה נורמלית PNF
  משפט הרברנד
  משפט סקולם

• תרגול 9 ←

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

• הרצאה 9 ←

  משפט סקולם
  בדיקת ספיקות של נוסחא
  הגדרת Ground Instance
  משפט הרברנד- שקילות בין תנאים
  דוגמא לשימוש במשפט הקומפקטיות לתחישב היחסים (בלי הוכחה)

• תרגול 10 ←

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

• הרצאה 10 ←

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

• תרגול 11 ←

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

• הרצאה 11 ←

  גדירות במבנים סופיים
  משחקי EF

• תרגול 12 ←

  משחקי Ehrenfeucht–Fraïssé
  משפט טרכטנברוט

• הרצאה 12 ←

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

• תרגול 13 ←

  תרגילי חזרה

• הרצאה 13 - הרצאת השלמה ←

  הוכחת משפט הדיכוטומיה עבור HC
  משפט השלמות עבור HC
  העשרה - משפט אי השלמות של גדל
  
  תודה לרותם בראונשטיין על הסיכום של שיעור ההשלמה!