תחשיב הפסוקים: בדיקת תקינות, המרת CNF והוכחת רזולוציה
הוכחה פורמלית של תקפות (Validity) וטאוטולוגיה דרך שתי פרדיגמות יסוד: בדיקת השמות מיצתית (Model Enumeration) מול שיטת ההפרכה (Refutation) באמצעות אלגוריתם הרזולוציה. ניתוח מלא ומעמיק של התרגיל.
דברי המורה הפרטי: לפרק לוגיקה לגורמים ולהבין את הרזולוציה שמאחורי הקלעים
שלום חברים! ברוכים הבאים לפרק 7. תחשיב הפסוקים נראה במבט ראשון כמו אלגברה בוליאנית פשוטה, אבל בעולם ה-AI הוא משמש כמנוע היסק חיוני לקבלת החלטות פורמלית. המטרה כאן אינה רק למלא טבלת אמת ידנית של 8 או 16 שורות, אלא להבין איך מחשב יכול להוכיח טענות מורכבות ללא צורך בסריקה אקספוננציאלית. נלמד כיצד המרת CNF פועלת בדיוק כמו פירוק לגורמים באלגברה, וכיצד רזולוציית הפרכה (Refutation Resolution) מאפשרת לסוכן להניח את שלילת היעד ולהגיע לסתירה (פסוקית ריקה $\square$) ביעילות מפתיעה.
💡 אינטואיציה בגובה העיניים: אנלוגיית חקירת הבלש בבית המשפט
תארו לעצמכם חוקר משטרה המציג שתי עדויות: "או שהחשוד היה בבנק, או שהוא היה ברכבת". העד השני מוכיח מעל לכל ספק: "החשוד לא היה ברכבת". כלל הרזולוציה "מבטל" את האפשרות של הרכבת ומותיר מסקנה ודאית בלתי ניתנת לערעור: החשוד היה בבנק! רזולוציית הפרכה פועלת בדיוק כך: מניחים את ההפך ממה שרוצים להוכיח, ואם כל הדרכים מובילות לסתירה מוחלטת – הטענה המקורית נכונה בוודאות מתמטית.
1. הצגת התרגיל והניתוח הסמנטי
נתבונן במשפט הלוגי המורכב הבא בתחשיב הפסוקים:
"נוכחות של אוכל מספיקה כדי שתהיה מסיבה, או שנוכחות של משקאות מספיקה כדי שתהיה מסיבה". די באחד התנאים כדי לקיים את המסקנה.
"אם יש גם אוכל וגם משקאות יחד, הרי שבהכרח תהיה מסיבה". אינטואיטיבית, אם אחד מהם הספיק לבדו, קל וחומר ששניהם יחד יגררו מסיבה.
2. סעיף א': קביעת תקינות (Validity) ושקילות לוגית
כדי להוכיח שהמשפט הוא **טאוטולוגיה** (תקף בכל מודל אפשרי), נוכיח תחילה כי שני האגפים שקילים לוגית לחלוטין זה לזה:
שני האגפים מניבים בדיוק את אותה פסוקית דיסיונקטיבית: $\neg Food \lor \neg Drinks \lor Party$. לכן המשפט כולו הוא מהתבנית $P \Rightarrow P$. פסוק מהצורה "אם P אז P" הוא **תקף תמיד (Tautology)** לכל השמה של ערכי אמת בעולם!
3. סעיף ב': המרת שלילת המשפט לצורת CNF מלאה
כדי להוכיח את המשפט ברזולוציה, אנו מיישמים את מתודולוגיית ה**הפרכה (Proof by Refutation)**: שוללים את הפסוק כולו, ממירים ל-CNF, ומחפשים סתירה שתוביל לגזירת הפסוקית הריקה $\square$:
| מספר פסוקית | מבנה הפסוקית (Clause) | מקור הגזירה | סוג פסוקית |
|---|---|---|---|
| (1) | ¬Food ∨ Party ∨ ¬Drinks | אגף שמאל המקורי | פסוקית רגילה (3 ליטרלים) |
| (2) | Food | שלילת אגף ימין | Unit Clause (ליטרל יחיד) |
| (3) | Drinks | שלילת אגף ימין | Unit Clause (ליטרל יחיד) |
| (4) | ¬Party | שלילת אגף ימין | Unit Clause (ליטרל יחיד) |
4. סעיף ג': הוכחה שלמה ברזולוציה עד לסתירה (□)
נפעיל את כלל הרזולוציה בין זוגות פסוקיות המכילות ליטרל והיפוכו:
(2) Food
(3) Drinks
(4) ¬Party
5. סימולציה אינטראקטיבית 7.1: מעבדת CNF ועץ רזולוציה מונחה
מידול עולמות וסוכנים לוגיים: חידת המתקן הגרעיני והעדפות המרק
הפיכת תפיסות חיישנים (Percepts) לטענות לוגיות, מידול עולמות סריג, סיפוק אילוצים (CSP/SAT), והתמודדות עם בעיית המסגרת (Frame Problem) באמצעות תחשיב המצבים (Situation Calculus).
דברי המורה הפרטי: מנועי SAT מודרניים – מתיאוריה שלמות לביצועי שיא
שלום חברים! בעיית SAT היא בעיית ה-NP-Complete הראשונה שהוכחה בהיסטוריה, אך באופן מדהים, פותרי SAT מודרניים פותרים היום בעיות תעשייתיות עם מיליוני משתנים! איך זה ייתכן? בזכות שלושה עקרונות פשוטים שהופכים את החיפוש העיוור למדויק: סיום מוקדם, ליטרלים טהורים (Pure Symbols) ופסוקיות יחידה (Unit Clauses) באלגוריתם DPLL. בנוסף, נכיר את WalkSAT – גישת חיפוש מקומי מבריקה שמוותרת על ודאות של 100% תמורת מהירות שיא, ואת עולם פסוקיות הורן שבו הכל נפתר בזמן ליניארי מוחלט.
💡 אינטואיציה בגובה העיניים: אנלוגיית מילוי לוח סודוקו
פתרון נוסחת CNF בעזרת DPLL דומה להפליא לפתרון סודוקו: כשרואים שורה שבה חסר רק מספר יחיד (פסוקית יחידה), לא מנחשים – משבצים אותו מיד! אם יש מספר שאין לגביו שום הגבלה סותרת (Pure Symbol), מציבים אותו מיד. רק כאשר אין ברירה, מנחשים השמה ובודקים. זו הסיבה ש-DPLL יעיל באלפי מונים מטבלאות אמת.
1. חידת הסוכן והמתקן הגרעיני (Nuclear Agent Puzzle)
סוכן של הסוכנות הבינלאומית לאנרגיה גרעינית אמור לוודא שאין אורניום במתקן המכיל 4 חדרים המסודרים בריבוע $2 \times 2$. הסוכן מוצב בחדר השמאלי התחתון ואינו רואה קירות זוהרים. חוק הטבע בסביבה קובע: אם יש אורניום בחדר כלשהו, קירות החדר הזה זוהרים משני צדדיהם (מבפנים ומבחוץ).
| משתנה לוגי | משמעות סמנטית בעולם הפיזיקלי | ערך אמת ידוע לסוכן |
|---|---|---|
| X | יש אורניום בחדר הימני התחתון [1,0] | נעלם (טענה להוכחה: ¬X) |
| A | הקיר המפריד בין חדר שמאלי-תחתון לשמאלי-עליון זוהר | שקרי (¬A) - החיישן קובע |
| B | הקיר המפריד בין חדר שמאלי-תחתון לימני-תחתון זוהר | שקרי (¬B) - החיישן קובע |
| C | הקיר המפריד בין חדר ימני-תחתון לימני-עליון זוהר | לא נצפה ישירות ע"י הסוכן |
⚡ היסק לוגי צעד-אחר-צעד (Modus Tollens)
הוכחה פורמליתהסוכן מוצב בחדר [0,0] ואינו מזהה שום זוהר בקירות:
"אם יש אורניום בחדר כלשהו, קירותיו זוהרים משני צדדיהם". עבור חדר X המוקף בקירות B ו-C:
נפעיל רזולוציה בין פסוקית החוק הפיזיקלי לבין תצפית החיישן על הליטרל B:
2. בסיס הידע (KB) והמרתו ל-CNF
3. הוכחה ברזולוציה שאין אורניום בחדר הימני התחתון (¬X)
כדי להוכיח את הטענה $KB \models \neg X$, אנו מוסיפים את שלילת הטענה לבסיס הידע: $$\neg(\neg X) \equiv X$$ ונגדיר אותה כפסוקית יחידה מספר (5) X:
(3) ¬X ∨ B
רזולוציה על הליטרל X מניבה את הפסוקית הנגזרת:
(2) ¬B
רזולוציה על הליטרלים הסותרים B מול ¬B מניבה:
4. מידול אילוצי מרק (CSP/SAT) ותחשיב המצבים (Situation Calculus)
מידול העדפות סועדים באמצעות תחשיב הפסוקים:
- הילה: רוצה אטריות רק אם יש כופתאות: $N \Rightarrow D \equiv \neg N \lor D$
- דן: רוצה כופתאות או ירקות: $D \lor V$
- תמר: לא רוצה גם כופתאות וגם ירקות: $\neg(D \land V) \equiv \neg D \lor \neg V$
מנוע הסקה מוצא את המודל היחיד המספק את כל האילוצים: מרק עם אטריות וכופתאות בלבד, ללא ירקות ($N=T, D=T, V=F$).
כאשר סוכן נע בין חדרים, עובדות רבות אינן משתנות (קירות נשארים באותו מקום).
פתרון אלגנטי זה פותר את בעיית המסגרת (Frame Problem) בכך שהוא מגדיר בדיוק מתי עובדה הופכת לאמת או נשארת אמת!
5. סימולציה אינטראקטיבית 7.2: עולם הסוכן הגרעיני וחידת המרק
פתרון תעלומות מורכבות: תעלומת הרצח של דן ויוריסטיקות רזולוציה
הצרנת עדויות בשפה טבעית, אילוצי רוצח יחיד שרק הוא משקר, המרה ל-9 פסוקיות CNF, והוכחה ממוקדת באמצעות רזולוציה לינארית (Linear Resolution), רזולוציית יחידה (Unit Resolution), וקבוצת תמיכה (Set of Support).
דברי המורה הפרטי: קופצים מדרגה לתחשיב היחסים מסדר ראשון (FOL)
שלום חברים! תחשיב הפסוקים סובל ממגבלה קריטית: הוא רואה את העולם כאוסף עובדות מנותקות (P, Q, R) ואינו מסוגל לדבר על אובייקטים, יחסים ותכונות משותפות. בתחשיב היחסים (FOL) אנחנו מקבלים כוח ביטוי עצום: קבועים, פונקציות, פרדיקטים וכמתים ($\forall, \exists$). כאן מסתתרות מלכודות המבחן הקלאסיות ביותר של הקורס – למשל מדוע $\forall$ תמיד הולך יד ביד עם גרירה ($\Rightarrow$), ומדוע שימוש ב-$\land$ עם כמת כולל הוא אסון סמנטי שגורם לקריסת הטענה.
💡 אינטואיציה בגובה העיניים: שאילתת SQL במסד נתונים
תחשבו על כמת כולל $\forall x [Student(x) \Rightarrow Smart(x)]$ כמו שאילתת סינון: "לכל שורה בטבלה, אם העמודה היא סטודנט, אז הוא חכם". אם נחליף את הגרירה ב-AND, נקבל טענה מגוחכת: "כל דבר ביקום הוא גם סטודנט וגם חכם" (כולל השולחן, החתול והטוסטר!).
1. תיאור תעלומת הרצח של דן והנחות היסוד
ארבעה חשודים ברצח של דן: צחי, גיא, דודי ועופר.
- עדות גיא: "אני לא רצחתי. דודי היה חבר של דן. עופר שנא את דן."
- עדות דודי: "הייתי מחוץ לעיר ביום הרצח (לא הייתי עם דן). אני אפילו לא מכיר את דן!"
- עדות עופר: "אני זכאי! ראיתי במו עיניי את גיא ואת דודי יחד עם דן ממש לפני הרצח."
- בדיוק אדם אחד ביצע את הרצח.
- רק הרוצח עצמו עלול לשקר – כל שאר האנשים דוברים אמת צרופה!
2. הגדרת הפרדיקטים והמרת בסיס הידע ל-9 פסוקיות CNF
| # | פסוקית CNF (Clause) | מקור ההצרנה |
|---|---|---|
| (1) | Killer(Guy) ∨ Friend(Dudi, Dan) | עדות גיא: ¬Killer(Guy) ⇒ Friend(Dudi, Dan) |
| (2) | Killer(Guy) ∨ ¬Friend(Ofer, Dan) | עדות גיא: ¬Killer(Guy) ⇒ ¬Friend(Ofer, Dan) |
| (3) | Killer(Dudi) ∨ ¬Friend(Dudi, Dan) | עדות דודי: ¬Killer(Dudi) ⇒ ¬Friend(Dudi, Dan) |
| (4) | Killer(Dudi) ∨ ¬With(Dudi) | עדות דודי: ¬Killer(Dudi) ⇒ ¬With(Dudi) |
| (5) | Killer(Ofer) ∨ With(Dudi) | עדות עופר: ¬Killer(Ofer) ⇒ With(Dudi) |
| (6) | Killer(Ofer) ∨ With(Guy) | עדות עופר: ¬Killer(Ofer) ⇒ With(Guy) |
| (7) | ¬Killer(Guy) ∨ ¬Killer(Dudi) | אילוץ רוצח יחיד (לא ייתכן ששניהם רצחו) |
| (8) | ¬Killer(Guy) ∨ ¬Killer(Ofer) | אילוץ רוצח יחיד (לא ייתכן ששניהם רצחו) |
| (9) | ¬Killer(Dudi) ∨ ¬Killer(Ofer) | אילוץ רוצח יחיד (לא ייתכן ששניהם רצחו) |
3. הוכחה ברזולוציה שדודי הוא הרוצח (Killer(Dudi))
נניח בשלילה שדודי אינו הרוצח, ונוסיף לבסיס הידע את שלילת השאילתה: (10) ¬Killer(Dudi). נבצע שרשרת צעדים לינארית:
4. יוריסטיקות רזולוציה וסולברי SAT מודרניים (CDCL)
מתחילה בפסוקית השאילתה (שלילת המטרה), ובכל צעד מצליבה את התוצאה האחרונה שנגזרה עם פסוקית מבסיס הידע המקורי. חוסכת זיכרון ומבטיחה עץ הוכחה ישר.
לפחות אחת משתי הפסוקיות המשתתפות היא פסוקית יחיד (Unit Clause). צעד זה מקטין מידית את מספר הליטרלים בפסוקית השנייה ומבטיח התכנסות מהירה.
מתירה רזולוציה אך ורק כאשר אחת הפסוקיות נגזרת משלילת המטרה. מונעת חיבורים עקרים בין עובדות רקע ומבטיחה שלמות (Completeness) אם בסיס הידע המקורי ספיק.
אלגוריתמי CDCL מנתחים את גרף ההשלכות בעת סתירה, לומדים פסוקית חדשה (Conflict Clause) ומוסיפים אותה ל-KB, ומבצעים Backjumping (קפיצה לאחור) כדי לעקוף ענפים עקרים.
5. סימולציה אינטראקטיבית 7.3: חדר החקירות של תעלומת הרצח
לוגיקה מסדר ראשון (FOL): כמתים, תרגום שפה וחידת האנשים בחדר
אונטולוגיה של אובייקטים ויחסים, חוקי ברזל בתרגום משפה טבעית, פרדוקס הספר של ראסל, והוכחה מלאה ברזולוציה מסדר ראשון של חידת הנשואים והרווקים (Case Analysis מובנה).
דברי המורה הפרטי: אמנות ההאחדה (Unification) ושרשור כללים
שלום חברים! כדי לחבר בין כללים מופשטים לעובדות קונקרטיות בעולם, אנו זקוקים למנגנון שמוצא את ה"מכנה המשותף" בין ביטויים עם משתנים. מנגנון זה נקרא האחדה (Unification), ותוצאתו היא ה-MGU (Most General Unifier) – ההצבה המינימלית הכללית ביותר שהופכת שני ביטויים לזהים. נלמד ליישם אותו בשרשור קדימה (Forward Chaining) המונחה על ידי עובדות קיימות, ובשרשור אחורה (Backward Chaining) המונחה על ידי שאלות ויעדים.
💡 אינטואיציה בגובה העיניים: התאמת מפתח למנעול
אם יש לכם כלל: "כל מי שאוכל תפוח הוא בריא", ונתון ש"דני אוכל תפוח", ההאחדה היא המנגנון שמזהה שניתן להציב $x = \text{Danny}$. ה-Occur Check מוודא שלא ננסה להציב מפתח בתוך עצמו ($x = f(x)$), מה שהיה גורם ללולאה אינסופית בייצור ביטויים.
1. חידת האנשים בחדר (Married and Unmarried Puzzle)
בחדר נמצאים שלושה אנשים: $A, B, C$. נתון כי:
• $A$ נשוי ($married(A)$).
• $C$ אינו נשוי ($\neg married(C)$).
• $A$ מסתכל על $B$ ($looks\_at(A, B)$).
• $B$ מסתכל על $C$ ($looks\_at(B, C)$).
השאילתה: האם בהכרח קיים בחדר אדם נשוי שמביט על אדם שאינו נשוי?
2. פיצול מקרים (Case Analysis) מול הוכחה ברזולוציה
סטטוס הנישואים של $B$ אינו ידוע. נבחן את שני המקרים האפשריים ביקום:
- מקרה 1: $B$ נשוי. אז $B$ (נשוי) מביט על $C$ (לא נשוי) -> מתקיים!
- מקרה 2: $B$ אינו נשוי. אז $A$ (נשוי) מביט על $B$ (לא נשוי) -> מתקיים!
רזולוציה אינה זקוקה לניחוש אנושי של פיצול מקרים. בעת שלילת השאילתה, הליטרלים של $married(B)$ מתבטלים אוטומטית כתוצאה מפעולת ההאחדה (Unification), ומניבים את הפסוקית הריקה $\square$ ללא תלות בסטטוס של $B$!
3. חוקי ברזל בתרגום שפה טבעית ל-FOL
"כל סטודנט עובר" = \forall x (Student(x) \Rightarrow Pass(x))
אם x אינו סטודנט (למשל כיסא), האגף השמאלי שקרי, והגרירה נכונה באופן ריק (Vacuously True).
"ישנו סטודנט שעובר" = \exists x (Student(x) \land Pass(x))
טוען שקיים עצם ספציפי x שמקיים בו-זמנית את שתי התכונות. שימוש שגוי ב-$\Rightarrow$ היה נכון עבור כל אובייקט שאינו סטודנט!
3. מקרה בוחן 4.2: פרד הקולי וסם בעליו (Fred & Sam) – הוכחה מלאה ב-Set of Support
תרגיל מבחן קלאסי המדגים רזולוציה מסדר ראשון (FOL) עם קבוצת הנחות עשירה ושימוש באסטרטגיית Set of Support (SOS). מטרתנו: להוכיח מתוך 10 הנחות עולם האם הכלב פרד נרטב בגשם או נשאר יבש בבית.
| # | ניסוח בשפה טבעית | הצרנה ב-FOL | פסוקית CNF |
|---|---|---|---|
| 1 | פרד הוא כלב מסוג קולי. | Collie(Fred) | Collie(Fred) |
| 2 | סם הוא בעליו החוקיים של פרד. | Master(Fred, Sam) | Master(Fred, Sam) |
| 3 | היום הוא יום שבת. | Day(Saturday) | Day(Saturday) |
| 4 | מזג האוויר בחוץ קר. | Weather(Cold) | Weather(Cold) |
| 5 | יורד גשם. | Weather(Rain) | Weather(Rain) |
| 6 | כל קולי הוא כלב. | ∀x (Collie(x) ⇒ Dog(x)) | ¬Collie(x) ∨ Dog(x) |
| 7 | כל כלב פוחד מרעמים כשיורד גשם. | ∀x (Dog(x) ∧ Weather(Rain) ⇒ Scared(x)) | ¬Dog(x) ∨ ¬Weather(Rain) ∨ Scared(x) |
| 8 | אם הבעלים שוהה בבית, הכלב שוהה עמו בבית. | ∀x∀y (Dog(x) ∧ Master(x, y) ∧ In(y, House) ⇒ In(x, House)) | ¬Dog(x) ∨ ¬Master(x, y) ∨ ¬In(y, House) ∨ In(x, House) |
| 9 | בימי שבת כשיורד גשם או כשקר, אנשים שוהים בביתם. | ∀y (Day(Saturday) ∧ Weather(Cold) ⇒ In(y, House)) | ¬Day(Saturday) ∨ ¬Weather(Cold) ∨ In(y, House) |
| 10 | כלב ששוהה בבית אינו נרטב. | ∀x (Dog(x) ∧ In(x, House) ⇒ ¬Wet(x)) | ¬Dog(x) ∨ ¬In(x, House) ∨ ¬Wet(x) |
קבוצת האקסיומות $A = \{1, 2, 3, 4, 5, 6, 7, 8, 9, 10\}$ ספיקה ועקבית בפני עצמה. קבוצת התמיכה הראשונית היא שלילת השאילתה: $B = \{11\}$. חוק ברזל: כל צעד רזולוציה יערב לפחות פסוקית אחת מקבוצת התמיכה $B$, והרזולבנטה החדשה תתווסף ל-$B$.
| פסוקית חדשה | פסוקיות אב ברזולוציה | האחדה (MGU θ) | רזולבנטה מופקת (Resolvent) |
|---|---|---|---|
| 12 | 11, 10 | {x / Fred} | ¬Dog(Fred) ∨ ¬In(Fred, House) |
| 13 | 12, 6 | {x / Fred} | ¬Collie(Fred) ∨ ¬In(Fred, House) |
| 14 | 13, 1 | ∅ | ¬In(Fred, House) (פרד אינו בבית!) |
| 15 | 14, 8 | {x / Fred} | ¬Dog(Fred) ∨ ¬Master(Fred, y) ∨ ¬In(y, House) |
| 16 | 15, 6 | {x / Fred} | ¬Collie(Fred) ∨ ¬Master(Fred, y) ∨ ¬In(y, House) |
| 17 | 16, 1, 2 | {y / Sam} | ¬In(Sam, House) (סם אינו בבית!) |
| 18 | 17, 9 | {y / Sam} | ¬Day(Saturday) ∨ ¬Weather(Cold) |
| 19 | 18, 3 | ∅ | ¬Weather(Cold) |
| 20 | 19, 4 | ∅ | □ (הפסוקית הריקה - סתירה הושגה!) |
5. סימולציה אינטראקטיבית 7.4: מעבדת כמתים וחידת האנשים בחדר
רזולוציה מתקדמת ב-FOL: סקולמיזציה, אלגוריתם האחדה (MGU) ומקרי בוחן שלמים
תורת הסקולמיזציה ושקילות ספיקות, אלגוריתם מרטלי-מונטנרי ובקרת מופעים (Occur Check), פתרון מלא של תרגיל הסטודנטים והבניינים בקמפוס (12 צעדים) והוכחת חידת הדר המאושרת (11 צעדים).
דברי המורה הפרטי: הפסגה הלוגית – 8 צעדי ההמרה ל-CNF וסקולמיזציה
שלום חברים! הגענו לנושא הנחשב למאתגר ביותר בפרק 7 – רזולוציה בתחשיב היחסים. כדי להפעיל רזולוציה על משפטי FOL, עלינו לעבור תהליך המרה קפדני בן 8 שלבים: מסילוק גרירות, דרך דחיפת שלילות פנימה, סטנדרטיזציה של שמות משתנים, סקולמיזציה (Skolemization) מדויקת – קבועים מול פונקציות סקולם לפי הכמתים הקודמים להם – השמטת כמתים כוללים, ופילוגים. נתרגל שלב אחר שלב עד להבנה עיוורת של כל שלב.
💡 אינטואיציה בגובה העיניים: קבוע סקולם מול פונקציית סקולם
אם נאמר: "לכל אדם יש לב" ($\forall x \exists y Heart(y, x)$), האם לכולם יש את אותו לב משותף? ברור שלא! הלב תלוי באדם הספציפי, ולכן מחליפים את $y$ בפונקציית סקולם $f(x)$. לעומת זאת, אם הטענה היא "קיים מישהו שהוא נשיא" ($\exists x President(x)$), ה-$x$ אינו תלוי באף משתנה אחר, ולכן הוא מוחלף בקבוע סקולם $C_1$.
1. תהליך הסקולמיזציה (Skolemization) ושקילות ספיקות
אלגוריתם הרזולוציה בלוגיקה מסדר ראשון פועל אך ורק על פסוקיות בעלות כמתים כוללים מרומזים. לא ניתן לבצע רזולוציה בנוכחות כמתים קיומיים ($\exists$). לשם כך פותח תהליך ה**סקולמיזציה** (על שם תורלף סקולם):
\exists x Rich(x) \implies Rich(S_0)
כאשר הכמת הקיומי אינו נמצא בתוך תחום של כמת כולל, ממציאים קבוע חדש לגמרי $S_0$ שטרם הופיע בשפה, המייצג את אותה ישות שקיומה מובטח.
\forall x \exists y Heart(y, x) \implies \forall x Heart(F(x), x)
כאשר הכמת הישי תלוי במשתנה כולל $x$ ("לכל אדם יש לב"), לא ניתן להציב קבוע בודד! חובה להגדיר פונקציה $F(x)$ הממפה כל $x$ ללב הייחודי שלו.
סקולמיזציה אינה שומרת על שקילות לוגית, משום שהשפה הורחבה בסמלי פונקציות וקבועים חדשים. עם זאת, היא שומרת במדויק על שקילות ספיקות: $$KB \text{ is satisfiable } \iff Skolem(KB) \text{ is satisfiable}$$ כיוון שרזולוציה מחפשת סתירה (חוסר ספיקות), שקילות ספיקות מספיקה ומבטיחה את נאותות ושלמות ההוכחה!
2. אלגוריתם ההאחדה (Unification) ובקרת מופעים (Occur Check)
האחדה מוצאת את ההצבה הכללית ביותר (Most General Unifier - MGU) $\theta$ ההופכת שני מונחים לזהים. אלגוריתם מרטלי-מונטנרי פועל באמצעות סט משוואות $E$:
| כלל אלגוריתמי | תנאי הפעלה וטרנספורמציה | דוגמה מספרית |
|---|---|---|
| פירוק פונקציות (Decomposition) | f(s_1, ..., s_n) = f(t_1, ..., t_n) מחולף ב-s_1=t_1, ..., s_n=t_n | f(x, a) = f(g(y), a) ⇒ x=g(y), a=a |
| מחיקת זהות (Delete) | t = t נמחק מהמערכת (טריוויאלי) | a = a נמחק |
| התנגשות (Clash Failure) | f(...) = g(...) או a = b עבור קבועים שונים מביא לעצירה מיידית בכישלון | f(a) = g(b) ⇒ FAIL! |
| בקרת מופעים (Occur Check) | x = t כאשר x מופיע בתוך t (לולאה אינסופית) מביא לכישלון מיידי | x = f(x) ⇒ FAIL! |
| הצבת משתנה (Variable Elimination) | x = t כאשר x אינו בתוך t: מציבים t במקום x בכל שאר המשוואות | x = a מחליף את x בכל ה-KB |
3. תרגיל 5: חידת הסטודנטים, הקורסים והבניינים בקמפוס
ניתוח מלא של 5 המשפטים המורכבים והוכחה שלמה בת 12 צעדים המוכיחה כי כל סטודנט ביקר בכל בניין בקמפוס:
(4a) ¬Student(x) ∨ ¬Building(y) ∨ Room(S_3(x, y), y)
(4b) ¬Student(x) ∨ ¬Building(y) ∨ Visited(x, S_3(x, y))
• (7) + (5) על Room בהצבה {z/S_3(x, y)} ⇒ (8) ¬Building(y) ∨ ¬Visited(x, S_3(x, y)) ∨ Visited(x, y)
• (8) + (6c) על Visited(x, y) ⇒ (9) ¬Building(y) ∨ ¬Visited(x, S_3(x, y))
• (9) + (4b) על Visited(x, S_3) ⇒ (10) ¬Building(y) ∨ ¬Student(x)
• (10) + (6a) ⇒ (11) ¬Building(y)
• (11) + (6b) ⇒ (12) □ (הפסוקית הריקה!)
4. תרגיל 6: חידת הדר המאושרת (Lucky Hadar)
- כל מי שעובר את הבחינות שלו במתמטיקה וזוכה בלוטו – מאושר.
- כל מי שלומד או שהינו בר-מזל, עובר את כל הבחינות שלו (כולל מתמטיקה).
- הדר לא למדה, אך הינה ברת-מזל.
- כל מי שהינו בר-מזל – זוכה בלוטו.
3. מקרה בוחן 5.3: אילן היוחסין המוזר (`gparent(I, I)`) – 16 צעדי רזולוציה מלאים
מבוסס על שיר העם המפורסם "I'm My Own Grandpa". נתון אילן יוחסין שבו בעקבות שרשרת נישואין, האדם $I$ הפך להורה של אמו $M$ ($Parent(I, M)$). מטרתנו: להוכיח פורמלית ברזולוציית FOL עם האחדה (MGU) האם האדם $I$ הוא סב של עצמו ($Gparent(I, I)$).
| # | הגדרה / עובדה בלוגיקה | פסוקית CNF |
|---|---|---|
| 1 | הגדרת סב: מי שהוא הורה של הורה ($∀x∀y (∃z (P(x,z) ∧ P(z,y)) ⇒ G(x,y))$) | ¬Parent(x, z) ∨ ¬Parent(z, y) ∨ Gparent(x, y) |
| 2 | אם היא הורה: $∀m∀c (Mother(m, c) ⇒ Parent(m, c))$ | ¬Mother(m, c) ∨ Parent(m, c) |
| 3 | אב הוא הורה: $∀f∀c (Father(f, c) ⇒ Parent(f, c))$ | ¬Father(f, c) ∨ Parent(f, c) |
| 4 | עובדה: $M$ היא אמו של $I$ | Mother(M, I) |
| 5 | עובדה: $F$ הוא אביו של $I$ | Father(F, I) |
| 6 | עובדת נישואין חריגה: $I$ הפך להורה של $M$ | Parent(I, M) |
| 7 | שלילת השאילתה (Negated Query): $¬Gparent(I, I)$ | ¬Gparent(I, I) |
| צעד | פסוקית ראשונה | פסוקית שנייה | מאחד כללי (MGU θ) | פסוקית מופקת (Resolvent) |
|---|---|---|---|---|
| צעד 1 (8) | 1 | 7 | {x / I, y / I} | ¬Parent(I, z) ∨ ¬Parent(z, I) |
| צעד 2 (9) | 8 | 6 | {z / M} | ¬Parent(M, I) |
| צעד 3 (10) | 9 | 2 | {m / M, c / I} | ¬Mother(M, I) |
| צעד 4 (11) | 10 | 4 | ∅ | □ (סתירה ראשית במסלול M!) |
| צעד 5 (12) | 2 | 4 | {m / M, c / I} | Parent(M, I) [עובדת הורות נגזרת] |
| צעד 6 (13) | 3 | 5 | {f / F, c / I} | Parent(F, I) |
| צעד 7 (14) | 1 | 6 | {x / I, z / M} | ¬Parent(M, y) ∨ Gparent(I, y) |
| צעד 8 (15) | 14 | 12 | {y / I} | Gparent(I, I) [גזירה ישירה!] |
| צעד 9 (16) | 15 | 7 | ∅ | □ (סתירה מול שלילת השאילתה!) |
4. סקולמיזציה מרובת משתנים ושאילתת אי-נביעה (Non-Provability Saturation)
🐶 חלק א': סקולמיזציה מרובת משתנים ("לכל כלב ובעליו...")
"לכל אדם ולכל כלב, אם האדם הוא בעליו של הכלב, אזי קיים מקום וקיים זמן שבהם הכלב נמצא עם בעליו."
הצרנה לוגית פורמלית:
שימו לב: שני הכמתים הקיומיים $\exists l$ (מקום) ו-$\exists t$ (זמן) נמצאים בתוך תחום ההשפעה של שני כמתים כוללים: $\forall x$ ו-$\forall y$.
לכן, לא ניתן להחליפם בקבועי סקולם, וגם לא בפונקציה של משתנה יחיד! חובה להגדיר שתי פונקציות סקולם דו-ממדיות:
🪐 חלק ב': שאילתת אי-נביעה ורוויה ללא סתירה ("האם יש מקום שכולם בו?")
נניח שבסיס הידע קובע ש"לכל אדם יש מקום שבו הוא נמצא": $$\forall x \exists y \text{ In}(x, y) \quad \xrightarrow{\text{Skolem}} \quad \text{In}(x, f(x)) \quad \text{[פסוקית 1]}$$ אנו מבקשים לדעת האם נובעת השאילתה: "האם קיים מקום מסוים שכל האנשים ביקום נמצאים בו?" $$Q: \exists y \forall x \text{ In}(x, y)$$
אנו מנסים לאחד את $\text{In}(x, f(x))$ עם $\text{In}(g(y), y)$:
1. מהארגומנט הראשון דורשים: $x = g(y)$.
2. מהארגומנט השני דורשים: $y = f(x)$.
3. בהצבת $x$ לתוך $y$, נקבל את המשוואה: $y = f(g(y))$!
💡 מסקנת המודל: לא נוצרות שום פסוקיות חדשות, ואלגוריתם הרזולוציה מגיע לרוויה (Saturation) מבלי למצוא סתירה ($\square$). מכאן הוכח סופית כי $KB \not\models Q$ – הטענה שקיים מקום שכולם נמצאים בו אינה נובעת מן ההנחות!
6. סימולציה אינטראקטיבית 7.5: מנוע האחדה ועץ רזולוציה ב-FOL
צ'יט-שיט מאסטר בלוגיקה ו-10 מלכודות נפוצות
מטריצת השוואה מקיפה בין מנועי ההסקה, עשר המלכודות הנפוצות ביותר בלוגיקה פורמלית, מילון מונחים מקצועי עברי-אנגלי, והרחבה לעולם התכנון הקלאסי (Planning).
דברי המורה הפרטי: צ'יט-שיט מאסטר וסיכום מקיף לקראת המבחן
שלום חברים! הגעתם ליחידת הסיכום והנעילה של פרק 7. כאן ריכזנו עבורכם את כל טבלאות ההשוואה המרכזיות: תחשיב הפסוקים מול FOL, אלגוריתמי הסקה וזמני ריצה, חוקי דה-מורגן וכמתים, רשימת מלכודות נפוצות במבחני OpenU, וטיפים מעשיים לפתרון תרגילי רזולוציה במינימום צעדים. השתמשו בטבלאות אלו כחזרה מהירה וממוקדת לפני פתרון מבחנים!
1. מטריצת השוואה כוללת בין מנועי הסקה (Inference Engines Matrix)
| אלגוריתם / גישה | פורמט ידע נדרש | שלמות (Completeness) | סיבוכיות זמן | יתרונות מרכזיים ומגבלות |
|---|---|---|---|---|
| טבלת אמת (Enumeration) | כל פסוק בוליאני | שלם ונאות | O(2^n) | אינטואיטיבי אך קורס בהתפוצצות קומבינטורית מעל 20 משתנים. |
| שרשור קדימה (Forward Chaining) | חוקי הורן בלבד (Horn) | שלם לחוקי הורן | O(n) ליניארי! | מהיר להפליא, אך אינו תומך בדיסיונקציות או בעמימות עובדות. |
| אלגוריתם DPLL | CNF מלא | שלם ונאות | NP-Complete | סריקת עץ חכמה עם Unit Propagation ו-Pure Symbols. |
| רזולוציה מלאה (Refutation) | CNF + סקולמיזציה | שלם להפרכה (Refutation Complete) | אקספוננציאלי במקרה גרוע | חזק ביותר בלוגיקה מסדר ראשון עם האחדה (MGU). |
| אלגוריתם CDCL | CNF תעשייתי | שלם ונאות | מעשי למיליוני משתנים | למידת פסוקיות קונפליקט מגרף השלכות וקפיצות לא-כרונולוגיות. |
| מנועי SMT (כגון Z3) | לוגיקה מסדר ראשון + תיאוריות (T) | שלם עבור תיאוריות כריעות | משתנה לפי תיאוריה | משלב SAT עם אריתמטיקה, מערכים ומצביעים. הסטנדרט באימות תוכנה. |
2. עשר מלכודות הבחינה הנפוצות ביותר בלוגיקה ורזולוציה
שגיאה: ביצוע רזולוציה בין $(A \lor B)$ לבין $(\neg A \lor \neg B)$ וקבלת $\square$ ישירות. חוק הברזל: רזולוציה מבטלת בדיוק ליטרל יחיד בכל צעד! התוצאה הנכונה היא טאוטולוגיה $A \lor \neg A$ או $B \lor \neg B$.
שגיאה: כתיבת $\forall x (Student(x) \land Pass(x))$ במקום $\Rightarrow$. פירושו שכל עצם ביקום (כולל שולחנות ומחשבים) הוא סטודנט שעובר מבחנים!
שגיאה: כתיבת $\exists x (Student(x) \Rightarrow Pass(x))$ במקום $\land$. משפט זה נכון באופן טריוויאלי וריק בכל עולם שבו קיים לפחות אובייקט אחד שאינו סטודנט!
שגיאה: החלפת $\forall x \exists y Loves(x, y)$ ב-$Loves(x, C)$. כיוון ש-$y$ מופיע בתחום של $x$, הוא חייב להיות פונקציית סקולם $F(x)$ ("לכל אדם יש מושא אהבה משלו").
חובה לוודא ששתי הפסוקיות הנבחרות לרזולוציה אינן חולקות את אותם שמות משתנים ($x, y$) לפני הפעלת האחדה, כדי למנוע הצבות שגויות.
ניסיון לאחד $x$ עם $f(x)$ גורר לולאה אינסופית $x = f(f(f(...)))$ ופוגע בנאותות (Soundness) של מערכת ההוכחה.
סקולמיזציה אינה שומרת על שקילות לוגית, אלא רק על Equisatisfiability. היא חוקית בהוכחות הפרכה ברזולוציה אך לא במעברי שקילות טהורים.
כדי להוכיח $KB \models \alpha$, חובה להוסיף את $\neg \alpha$ ל-KB ולחפש סתירה $\square$. הוספת $\alpha$ המקורית היא שגיאה מתודולוגית.
בלוגיקה קלאסית, עובדה שאינה כתובה ב-KB אינה נחשבת לשקרית! אין להסיק $\neg P$ רק כי $P$ אינו מופיע בבסיס הידע.
$\forall x \exists y$ אינו שקול ל-$\exists y \forall x$. הראשון מניח שלכל אחד יש מישהו, והשני מניח שיש מישהו יחיד המשותף לכולם.
3. שאלת מבחן תיאורטית: ניתוח זרות קבוצות ברזולוציה (משפט 7.1.6)
נניח שנתונה קבוצת אקסיומות עולם $P$, ואנו מעוניינים להוכיח בעזרת רזולוציה בשלילה כי המשפט $T$ נובע מ-$P$ ($P \models T$). לשם כך אנו מפעילים רזולוציה על הקבוצה המאוחדת $P \cup \{\neg T\}$ ומייצרים עץ גזירה של פסוקיות עד לקבלת הפסוקית הריקה ($\square$). נסמן ב-$A$ את קבוצת כל הפסוקיות שהשתתפו בפועל בעץ ההוכחה של הפסוקית הריקה.
כלומר, האם ייתכן שעץ הרזולוציה שמפיק סתירה ($\square$) אינו משתמש באף פסוקית משלילת המשפט $\neg T$, אלא רק בפסוקיות מתוך $P$?
כן, הדבר ייתכן! זה קורה אם ורק אם קבוצת האקסיומות $P$ בפני עצמה אינה עקבית (Inconsistent / בלתי ספיקה).
אם $P$ מכילה סתירה פנימית (למשל $\{Q, \neg Q\}$), אלגוריתם הרזולוציה יכול לגזור את הפסוקית הריקה $\square$ ישירות מתוך $P$ מבלי לגעת כלל בשאילתה $T$. לפי חוק Ex Falso Quodlibet ("מתוך שקר נובע כל דבר"), מבסיס ידע סותר נובע כל משפט שבעולם!
כלומר, האם ייתכן שעץ הרזולוציה שמפיק את הפסוקית הריקה ($\square$) אינו משתמש באף אקסיומה מתוך $P$, אלא נגזר כולו משלילת המשפט $\neg T$ בלבד?
כן, הדבר ייתכן! זה קורה אם ורק אם המשפט $T$ הוא טאוטולוגיה (אמת לוגית אוניברסלית / Valid Formula).
אם המשפט $T$ הוא טאוטולוגיה (למשל $P \lor \neg P$), אזי שלילתו $\neg T$ היא סתירה לוגית בפני עצמה (Unsatisfiable). במקרה זה, הרזולוציה על $\neg T$ לבדה מייצרת את הפסוקית הריקה $\square$ ללא שום צורך באקסיומות $P$ או בעובדות על העולם!
4. מילון מונחים מקצועי: לוגיקה והסקה אוטומטית (Glossary)
הגשר לפרק 8: מעבר מלוגיקה סטטית לתכנון פעולות (Classical Planning)
בפרקים 6 ו-7 למדנו כיצד סוכן מייצג ידע ומסיק מסקנות אודות המצב הנוכחי של העולם בעזרת לוגיקה פסוקית ו-FOL. אך סוכן אינטליגנטי אמיתי אינו מסתפק רק בלדעת מה מצב העולם – הוא נדרש לפעול כדי לשנות אותו ולהגיע למטרות מוגדרות!
ייצוג פעולות בעזרת תנאי קדם (Preconditions), תוצאות הוספה (Add List) ותוצאות מחיקה (Delete List).
שרשור קדימה מונחה יוריסטיקות (Forward State Search) מול רגרסיה לאחור ממצב המטרה (Goal Regression).
אלגוריתם פורץ דרך המשתמש בגרף רמות מתחלף ובקשרי שלילה הדדית (Mutex) לחילוץ תוכניות אופטימליות במהירות.