סוכנים מבוססי ידע, תחשיב הפסוקים ונביעה לוגית
כיצד סוכן אוטונומי בונה מודל פנימי של העולם, מתעדכן בתחושות חושיות (TELL), גוזר עובדות נסתרות (ASK), ומקבל החלטות מוכחות מתמטית בסביבות מוסתרות חלקית כגון עולם הוומפוס.
ברוכים הבאים לעולם הלוגיקה
שלום חברים! בפרקים הקודמים חיפשנו פתרונות באמצעות אלגוריתמים כמו $A^*$ ו-CSP. אבל מה קורה כשהסוכן אינו יודע את כל מצב העולם מראש? בסביבה מוסתרת חלקית (Partially Observable), סוכן רפלקס פשוט או עץ החלטות קשיח יקרוס מיד. כאן נכנסת לתמונה הבינה המבוססת על ידע (Knowledge-Based Intelligence): הסוכן שומר בסיס ידע ($KB$) של טענות פורמליות, ומפעיל היסק לוגי (Inference) כדי לחשוף מה נכון בוודאות מבלי לנחש. בפרק זה נתחיל בתחשיב הפסוקים הפשוט והאלגנטי ונבין את המושג החשוב ביותר: נביעה לוגית ($KB \models \alpha$). בואו נצלול!
1. ארכיטקטורת סוכן מבוסס ידע (Knowledge-Based Agents)
הרכיב המרכזי בארכיטקטורה של סוכן לוגי הוא בסיס הידע (Knowledge Base - KB). ה-$KB$ הוא אוסף פסוקים (sentences) בשפה לוגית פורמלית, כאשר כל פסוק מייצג טענה כלשהי לגבי מצב העולם.
הסוכן מקבל תפיסה חושית (Percept) או לומד חוק טבע חדש, ומזין אותו ישירות לבסיס הידע: $\text{TELL}(KB, \text{sentence})$. בסיס הידע מתרחב ומתעדכן.
לפני שהסוכן בוחר פעולה, הוא שואל את ה-$KB$: $\text{ASK}(KB, \alpha)$. מנוע ההיסק בודק האם השאילתה $\alpha$ (למשל: "האם המשבצת הבאה בטוחה?") נובעת בהכרח ממה שכבר נאמר לו קודם לכן.
🏹 סביבת הבנצ'מרק: "עולם הוומפוס" (The Wumpus World)
עולם הוומפוס הוא מערה המחולקת לרשת $4 \times 4$. הסוכן מתחיל תמיד במשבצת $[1,1]$ במטרה למצוא זהב ולצאת חי. במערה מסתתרת מפלצת הוומפוס ובורות עמוקים (Pits). הסוכן אינו רואה מעבר למשבצת שבה הוא עומד, אך מצויד בחיישנים עקיפים:
- רוח (Breeze): מורגשת בכל משבצת הסמוכה ישירות (מעלה, מטה, ימין, שמאל) לבור.
- סירחון (Stench): מורגש בכל משבצת הסמוכה ישירות לוומפוס.
- נצנוץ (Glitter): נראה אך ורק במשבצת שבה מונח הזהב עצמו.
2. תחשיב הפסוקים: תחביר, סמנטיקה ומודלים
א. התחביר (Syntax)
מגדיר את המבנה הפורמלי של הפסוקים החוקיים בשפה:
- פסוק אטומי (Atomic Sentence): סימבול לוגי בודד המייצג עובדה, כגון $P, Q, W_{1,3}, B_{2,1}$.
- ליטרל (Literal): פסוק אטומי חיובי ($P$) או שלילה שלו ($\neg P$).
- פסוק מורכב (Complex Sentence): נבנה באמצעות סוגריים ו-5 הקשרים הלוגיים המרכזיים.
ב. הסמנטיקה והמודלים (Semantics & Models)
הסמנטיקה מגדירה את ערך האמת של כל פסוק ביחס לעולם:
- מודל (Model $m$): עולם מובנה פורמלית המהווה השמה של ערכי אמת ושקר (True/False) לכל אחד מהסימבולים.
- מרחב המודלים: עבור $n$ סימבולים אטומיים בלתי תלויים, קיימים בדיוק $2^n$ מודלים אפשריים.
- קבוצת המודלים $M(\alpha)$: קבוצת כל העולמות שבהם הפסוק $\alpha$ מקבל ערך אמת (מסופק).
טבלת האמת של חמשת הקשרים הלוגיים:
| P | Q | ¬P | P ∧ Q | P ∨ Q | P ⇒ Q | P ⇔ Q |
|---|---|---|---|---|---|---|
| F | F | T | F | F | T | T |
| F | T | T | F | T | T | F |
| T | F | F | F | T | F | F |
| T | T | F | T | T | T | T |
שימו לב להדגשה: גרירה ($P \Rightarrow Q$) היא שקרית אך ורק במקרה שבו התנאי $P$ אמיתי והתוצאה $Q$ שקרית! בכל שאר המקרים (כולל כאשר $P$ שקרי), הגרירה אמיתית בהגדרה.
3. נביעה לוגית (Entailment): לב ליבה של ההסקה
המשמעות: בסיס הידע $KB$ גורר לוגית את הפסוק $\alpha$ אם ורק אם בכל מודל שבו $KB$ כולו אמיתי, גם $\alpha$ אמיתי בהכרח. אם נצייר את מרחב המודלים כדיאגרמת ון, עיגול העולמות המספקים את ה-$KB$ מוכל לחלוטין בתוך עיגול העולמות המספקים את $\alpha$.
אלגוריתם היסק נקרא נאות אם הוא גוזר אך ורק פסוקים שנובעים באמת מבסיס הידע: אם $\text{Infers}(KB, \alpha)$ אזי $KB \models \alpha$. אלגוריתם נאות לעולם אינו מייצר שקרים מתוך אמת!
אלגוריתם היסק נקרא שלם אם הוא מסוגל למצוא הוכחה לכל פסוק שנובע לוגית מבסיס הידע: אם $KB \models \alpha$, האלגוריתם מובטח להחזיר תשובה חיובית.
נביעה לוגית שקולה לכך שמשפט הגרירה הוא טאוטולוגיה (Valid) – אמיתי בכל עולם אפשרי ביקום.
כדי להוכיח ש-$\alpha$ נובע, נוסיף את שלילתו $\neg\alpha$ ל-$KB$ ונראה שקבוצת המודלים המשותפת היא ריקה (סתירה מוחלטת). זהו עקרון היסוד של רזולוציה!
4. חוקי השקילות הלוגית המרכזיים
שני פסוקים $\alpha$ ו-$\beta$ הם שקילים לוגית ($\alpha \equiv \beta$) אם ורק אם הם מקבלים בדיוק את אותו ערך אמת בכל המודלים ($M(\alpha) = M(\beta)$). חוקים אלו הם ארגז הכלים לאלגברה לוגית ולהמרת פסוקים לצורת CNF:
5. סימולציה אינטראקטיבית 6.1: מעבדת מרחב המודלים ועולם הוומפוס
אלגוריתם הרזולוציה, המרה ל-CNF ושרשור בפסוקיות הורן
ממעבר על כל שורות טבלת האמת ועד לגזירה ישירה: הוכחה בשלילה באמצעות רזולוציה, וכיצד הגבלת הידע לפסוקיות הורן מאפשרת היסק מובטח בזמן ריצה לינארי.
לקפוץ מעל מחסום הסיבוכיות
בדיקת טבלאות אמת היא תהליך נאיבי שדורש $2^n$ שורות. בעולם האמיתי עם 100 משתנים, $2^{100}$ הוא מספר הגדול ממספר האטומים ביקום! לכן חוקרי AI פיתחו שתי דרכים מבריקות לעקוף את המחסום: אלגוריתם הרזולוציה שמבטל ליטרלים משלימים ומחפש סתירה ישירה, ופסוקיות הורן שמאפשרות שרשור קדימה ואחורה בזמן לינארי לחלוטין ($O(n)$). בואו נלמד כיצד להמיר כל נוסחה ל-CNF ואיך להפעיל את האלגוריתמים הללו שלב אחר שלב.
1. אלגוריתם הרזולוציה בתחשיב הפסוקים (PL-Resolution)
רזולוציה היא כלל היסק חזק ושלם (Refutation Complete). הכלל פועל על ידי מציאת זוג ליטרלים משלימים (Complementary Literals) בין שתי פסוקיות דיסיונקטיביות, קיזוזם ההדדי, ומיזוג שאר הליטרלים לפסוקית חדשה המכונה Resolvent:
כאשר מתקיים $l_i \equiv \neg m_j$ (לדוגמה $P$ ו-$\neg P$). במקרה הפשוט של שני ליטרלים: \[\frac{A \vee B, \quad \neg A \vee C}{B \vee C} \quad \Longleftrightarrow \quad \frac{\neg A \Rightarrow B, \quad B \Rightarrow C}{\neg A \Rightarrow C}\]
🎯 הוכחה על דרך השלילה (Proof by Contradiction / Refutation)
כדי להוכיח שהשאילתה $\alpha$ נובעת מ-$KB$ ($KB \models \alpha$), אנו מזינים לאלגוריתם הרזולוציה את הקבוצה המורחבת $KB \wedge \neg\alpha$. האלגוריתם מבצע קיזוזים חוזרים ונשנים:
- אם נוצרת הפסוקית הריקה ($\square$ / Empty Clause): נחשפה סתירה לוגית בלתי ניתנת ליישוב! המסקנה היא שההנחה $\neg\alpha$ בלתי אפשרית, ולכן $\alpha$ נובעת בהכרח ($KB \models \alpha$).
- אם לא נוצרות פסוקיות חדשות והפסוקית הריקה לא הושגה: אין נביעה ($KB \not\models \alpha$).
2. ארבעת שלבי ההמרה לצורה נורמלית קוניונקטיבית (CNF Conversion)
אלגוריתם הרזולוציה דורש שכל הפסוקים יוזנו בצורת CNF (Conjunctive Normal Form): קוניונקציה ("וגם") של פסוקיות (Clauses), כאשר כל פסוקית היא דיסיונקציה ("או") של ליטרלים בלבד. להלן 4 שלבי ההמרה כפי שנלמדו בכיתה עבור הפסוק של משבצת הוומפוס $B_{1,1} \Leftrightarrow (P_{1,2} \vee P_{2,1})$:
החלפת $\alpha \Leftrightarrow \beta$ ב-$(\alpha \Rightarrow \beta) \wedge (\beta \Rightarrow \alpha)$.
החלפת $\alpha \Rightarrow \beta$ ב-$\neg\alpha \vee \beta$.
החלפת $\neg(P_{1,2} \vee P_{2,1})$ ב-$(\neg P_{1,2} \wedge \neg P_{2,1})$ וביטול שלילה כפולה.
הפעלת פילוג מעל הדיסיונקציה: קיבלנו 3 פסוקיות CNF עצמאיות ומוכנות להזנה לרזולוציה!
3. חמש אסטרטגיות רזולוציה מתקדמות (Advanced Resolution Strategies)
אסטרטגיות רזולוציה מתקדמות & שאלות מבחןהפעלת רזולוציה נאיבית מובילה לפיצוץ קומבינטורי של פסוקיות חדשות. כדי לנווט ביעילות במרחב החיפוש ולהגיע לפסוקית הריקה ($\square$) במינימום צעדים, פותחו 5 אסטרטגיות בקרה מובנות בעלות תכונות מתמטיות קריטיות:
מתחילים מקבוצת הפסוקיות ההתחלתית $S_0$. בכל שלב גוזרים את כל הרזולבנטות האפשריות מכל זוגות הפסוקיות ברמה הנוכחית ומצרפים אותן ל-$S_1, S_2, \dots$ לפני מעבר לרמה הבאה.
• פיצוץ קומבינטורי: מספר הפסוקיות גדל מעריכית עם העומק, וגורם לצריכת זיכרון וזמן עצומים.
ליטרל נקרא טהור (Pure) אם הוא מופיע באותו מופע בלבד (רק חיובי, או רק שלילי) בכל הפסוקיות ב-$KB$, ואין לו ליטרל משלים נגדי באף פסוקית.
פסוקית המכילה ליטרל ואת שלילתו בעת ובעונה אחת ($P \vee \neg P \vee \dots$) היא טאוטולוגיה, שכן ערך האמת שלה הוא תמיד $True$ בכל מודל אפשרי.
בכל צעד רזולוציה, לפחות אחת משתי הפסוקיות הנבחרות חייבת להיות פסוקית יחידה (Unit Clause) – כלומר פסוקית המורכבת מליטרל בודד (אורך 1).
• עבור פסוקיות הורן (Horn Clauses): רזולוציית יחידה שלמה תמיד ומוצאת סתירה בזמן פולינומיאלי/לינארי!
מחלקים את קבוצת הפסוקיות לשתי קבוצות זרות: קבוצת האקסיומות וההנחות ($A$) המייצגת את עובדות העולם, וקבוצת התמיכה ($B$) המתחילה משלילת השאילתה אותה אנו מבקשים להוכיח ($\neg Q$).
4. פסוקיות הורן (Horn Clauses) והיסק בזמן לינארי
כאשר בסיס הידע מכיל פסוקים כלליים, הרזולוציה עלולה לקחת זמן אקספוננציאלי. אולם, מרבית הידע האנושי והמערכות המומחיות מנוסח ככללי תנאי ותוצאה (If-Then). מבנה מיוחד זה נקרא פסוקיות הורן:
פסוקית CNF המכילה בדיוק ליטרל חיובי אחד (המכונה ה"ראש" או המסקנה), ושאר הליטרלים שליליים (ה"גוף" או ההנחות).
פסוקית CNF המכילה לכל היותר ליטרל חיובי אחד (מאפשרת גם 0 ליטרלים חיוביים, המייצגים אילוץ שלילה או סתירה).
השוואה מעמיקה: שרשור קדימה (FC) מול שרשור לאחור (BC)
| מאפיין השוואה | שרשור קדימה (Forward Chaining - FC) | שרשור לאחור (Backward Chaining - BC) |
|---|---|---|
| מוטיבציה מרכזית | מונחה-נתונים (Data-driven) | מונחה-מטרה (Goal-driven) |
| נקודת ההתחלה | מתחיל מן העובדות הידועות ב-$KB$ וממשיך הלאה. | מתחיל מהשאילתה המבוקשת $q$ ומחפש מאיפה להוכיח. |
| סיבוכיות זמן ריצה | O(n) - לינארי ביחס לגודל ה-KB | הרבה פחות מ-O(n) - רק ענפים רלוונטיים |
| מנגנון מניעת חישוב מיותר | מערך מונים count[c] שמנוכה ב-1 לכל עובדה. |
סורק אך ורק כללים שבראשם מופיעה מטרת המשנה. |
| הקבלה קוגניטיבית | עיבוד תחושתי לא-מודע (זיהוי קול, ראייה ממוחשבת). | פתרון בעיות מודע (תכנון מסלול, הוכחת משפט). |
5. סימולציה אינטראקטיבית 6.2: מעבדת הרזולוציה ומפלי השרשור
אלגוריתמים מתקדמים לבדיקת מודלים: DPLL מול WalkSAT
הכרעת ספיקות במרחבי ענק: כיצד אלגוריתם DPLL מנצל הפצת יחידה וסימבולים טהורים לחיפוש עץ שלם, וכיצד WalkSAT פורץ את גבולות המיליונים באמצעות חיפוש מקומי הוריסטי.
קרב הענקים של מדעי המחשב
בעיית הספיקות הבוליאנית (SAT Problem) היא הבעיה ה-NP-שלמה הראשונה שהוכחה בהיסטוריה (משפט קוק-לוין). ובכל זאת, מערכות תעשייתיות כמו אימות שבבי מעבדים באינטל ומערכות תכנון משימות בנאס"א פותרות פסוקים בעלי מיליוני משתנים מדי יום! כיצד זה ייתכן? בזכות שני אלגוריתמים גאוניים: DPLL – שמבצע חיפוש עץ שלם אך גוזם 99.9% ממנו בעזרת "הפצת יחידה", ו-WalkSAT – שמטפס על גבעת הפתרונות בעזרת מינימום סתירות ואקראיות מבוקרת. בואו נבין את הקרב ביניהם לעומק!
1. אלגוריתם DPLL: חיפוש עץ לעומק עם שלוש יוריסטיקות מנצחות
אלגוריתם DPLL (Davis-Putnam-Logemann-Loveland) מקבל כקלט פסוק בצורת CNF ומבצע חיפוש עץ רקורסיבי לעומק (DFS) עם נסיגה לאחור (Backtracking). הוא משפר את בדיקת טבלאות האמת באופן דרמטי באמצעות שלושה מנגנונים:
פסוקית היא אמיתית ברגע שלפחות ליטרל אחד בה נקבע כ-True. מנגד, הפסוק כולו נכשל מיד ברגע שפסוקית בודדת הפכה לשקרית לחלוטין. אין צורך להמשיך להציב בשאר המשתנים – נסוגים מיד לאחור (Backtrack)!
סימבול נקרא "טהור" אם הוא מופיע באותו סימן בדיוק (רק חיובי $P$ או רק שלילה $\neg P$) בכל הפסוקיות שטרם סופקו. קובעים לו מיד ערך שמספק אותו. זוהי השמה בטוחה שאינה דורשת פיצול ענפים!
פסוקית שבה כל הליטרלים למעט אחד כבר הוצבו כ-False. כדי למנוע את הכשלת המערכת, חובה דטרמיניסטית להציב לליטרל הנותר True. פעולה זו גוררת שרשרת השמות כפויה המכונה Unit Propagation.
function DPLL-SATISFIABLE?(s) returns true or false
clauses ← set of clauses in CNF representation of s
symbols ← list of proposition symbols in s
return DPLL(clauses, symbols, {})
function DPLL(clauses, symbols, model) returns true or false
if every clause in clauses is true in model then return true
if some clause in clauses is false in model then return false
P, val ← FIND-PURE-SYMBOL(symbols, clauses, model)
if P is non-null then return DPLL(clauses, symbols - P, model ∪ {P: val})
P, val ← FIND-UNIT-CLAUSE(clauses, model)
if P is non-null then return DPLL(clauses, symbols - P, model ∪ {P: val})
P ← FIRST(symbols); rest ← REST(symbols)
return DPLL(clauses, rest, model ∪ {P: true}) or
DPLL(clauses, rest, model ∪ {P: false})
2. אלגוריתם WalkSAT: חיפוש מקומי הוריסטי מבוסס Min-Conflicts
בניגוד ל-DPLL שהוא אלגוריתם חיפוש מלא ושלם, WalkSAT הוא אלגוריתם חיפוש מקומי (בדומה לטיפוס גבעות ולהתקררות מדומה). הוא מתחיל מהשמה אקראית לחלוטין, ובכל צעד מנסה לשפר את המודל על ידי היפוך (Flip) ערכו של משתנה בודד.
🎲 מנגנון הבחירה ההסתברותי של WalkSAT (פרמטר p)
בכל איטרציה, האלגוריתם בוחר באקראי פסוקית אחת שאינה מסופקת במודל הנוכחי, ומחליט איזה משתנה מתוכה להפוך:
3. טבלת השוואה ישירה: DPLL מול WalkSAT
| מאפיין אלגוריתמי | DPLL | WalkSAT |
|---|---|---|
| אסטרטגיית חיפוש | חיפוש עץ לעומק עם נסיגה (Backtracking Search) | חיפוש מקומי הוריסטי (Local Search / Hill-Climbing) |
| תכונת השלמות (Completeness) | שלם (Complete) – תמיד יכריע ספיקות או יוכיח חוסר ספיקות | אינו שלם (Incomplete) – עלול להיכשל גם כשיש פתרון |
| תכונת הנאותות (Soundness) | נאות (Sound) | נאות (Sound) – אם מצא מודל, המודל חוקי בוודאות |
| צריכת זיכרון | O(n) - לינארי בעומק העץ | O(n + m) - שמירת ההשמה ומספר הפסוקיות |
| שימוש אופטימלי בתעשייה | אימות חומרה (Verification) שבו חובה לדעת אם קיימת סתירה | תכנון ושיבוץ בעיות ענק (Scheduling) הידועות כספיקות |
4. סימולציה אינטראקטיבית 6.3: מעבדת DPLL ו-WalkSAT
לוגיקה מסדר ראשון (First-Order Logic): אונטולוגיה וכמתים
מדוע תחשיב הפסוקים קורס מול מורכבות העולם האמיתי, כיצד אובייקטים, יחסים ופונקציות מרכיבים שפת ידע עוצמתית, ומדוע סדר הכמתים משנה את המציאות מקצה לקצה.
המעבר לפילוסופיה של אובייקטים
תארו לעצמכם שהייתם רוצים לומר: "כל הסטודנטים בקורס בינה מלאכותית הם אנשים חכמים". בתחשיב הפסוקים, הייתם צריכים לכתוב פסוק נפרד עבור כל סטודנט בכיתה: $S_1 \Rightarrow H_1$, $S_2 \Rightarrow H_2$ וכן הלאה למיליארדי אנשים! זהו חוסר כוח ביטוי (Expressive Power) משווע. לוגיקה מסדר ראשון (FOL) פותרת זאת על ידי חיקוי החשיבה האנושית: ישנם עצמים, ישנן תכונות ויחסים, וישנם כמתים ($\forall, \exists$) שמאפשרים לקבוע טענות גלובליות בשורה אחת. בואו נלמד כיצד להשתמש בהם בצורה מדויקת וללא טעויות נפוצות!
1. האונטולוגיה של לוגיקה מסדר ראשון (FOL)
בעוד שתחשיב הפסוקים מניח עולם שטוח המורכב מעובדות בוליאניות פשוטות, FOL מאמצת אונטולוגיה עשירה המורכבת משלושה יסודות מרכזיים:
ישויות פיזיות או מופשטות בעולם: $\text{KingJohn}, \text{Richard}, 2, \text{NUS}$. מיוצגים בתחביר על ידי שמות קבועים.
תכונות של עצמים או קשרים ביניהם המחזירים אמת או שקר: $\text{Brother}(\text{John}, \text{Richard})$, $\text{King}(\text{John})$, $\text{OnHead}(\text{Crown}_1, \text{John})$.
מיפוי מאובייקט לאובייקט יחיד אחר בעולם (אינן מחזירות אמת/שקר!): $\text{LeftLegOf}(\text{John})$, $\text{Father}(\text{Richard})$, $\sqrt{9} \to 3$.
📐 מושג המודל ב-FOL: תחום ופונקציית פירוש (Interpretation)
מודל ב-FOL אינו עוד רשימה של ערכי True/False, אלא מבנה מתמטי תורת-קבוצתי:
- התחום (Domain): קבוצת העצמים הממשיים הקיימים בעולם.
- פונקציית הפירוש (Interpretation): קושרת כל קבוע לאובייקט ספציפי בתחום, כל פרדיקט לקבוצת $n$-יות של אובייקטים שעבורם היחס מתקיים, וכל פונקציה להתאמה בין איברי התחום.
2. כמתים (Quantifiers) ושתי מלכודות המבחן הקלאסיות
∀ כמת כולל (Universal Quantifier)
"לכל x"מצהיר כי הטענה נכונה עבור כל אובייקט בתחום של המודל.
משמעות המשפט השגוי: "כל דבר ביקום נמצא ב-NUS וכל דבר ביקום חכם" (כולל סלעים, שולחנות וכוכבים!). לכן כמת כולל דורש תמיד גרירה ($\Rightarrow$).
∃ כמת קיומי (Existential Quantifier)
"קיים x"מצהיר כי קיים לפחות אובייקט אחד בתחום המקיים את התנאי.
משמעות המשפט השגוי: הפסוק יהפוך לאמת ריקה (Vacuously True) ברגע שקיים עצם כלשהו שאינו ב-NUS (כי גרירה עם שקר ברישא מחזירה אמת!). לכן כמת קיומי דורש תמיד וגם ($\wedge$).
3. סדר כמתים מקוננים ודואליות הכמתים (חוקי דה-מורגן)
סדר כמתים שונים משנה באופן קריטי!
דואליות הכמתים (חוקי דה-מורגן לכמתים):
כל כמת ניתן לביטוי באמצעות שלילתו של הכמת האחר:
4. סימולציה אינטראקטיבית 6.4: מעבדת האונטולוגיה והכמתים
היסק מתקדם ב-FOL: האחדה (MGU), סקולמיזציה ורזולוציה מלאה
כיצד אלגוריתם ההאחדה מגשר על פער המשתנים, משפט ארברנד וחידת חצי-הכריעות, 6 שלבי ההמרה ל-CNF, ועץ ההוכחה המפורסם של Criminal(West).
השיא האלגוריתמי של הקורס
הגענו לפסגת הלוגיקה בבינה מלאכותית! כאן נפגשים כל החוטים: כיצד מחשב יכול להוכיח משפטים מתמטיים מורכבים מבלי "להציב את כל האפשרויות בעולם"? הסוד טמון בהאחדה (Unification): התאמה חכמה כמו מנעול ומפתח בין שתי נוסחאות המכילות משתנים. נלמד מהי פונקציית סקולם, מדוע אסור לשכוח את ה-Occurs Check, ואיך להרכיב עץ רזולוציה שלם שמפיל את הטענות בזו אחר זו עד לפסוקית הריקה $\square$. בואו נתחיל!
1. כללי הצבה, משפט ארברנד ובעיית חצי-הכריעות (Semi-Decidability)
מאפשר להחליף את המשתנה $v$ בכל מונח קרקעי $g$ (קבוע מוכר). למשל, מתוך $\forall x \text{ King}(x) \Rightarrow \text{Evil}(x)$, בהצבה $\{x/\text{John}\}$ נקבל: $\text{King}(\text{John}) \Rightarrow \text{Evil}(\text{John})$.
מחליפים את $v$ בקבוע סקולם חדש ($k$) שאינו מופיע באף מקום אחר ב-$KB$ (זהות דמה זמנית). מבוצע פעם אחת בלבד.
🌌 משפט ארברנד (Herbrand's Theorem), משפט צ'רץ'-טיורינג ואי-כריעות למחצה (Semi-Decidability)
יסודות החישוביות בלוגיקהכאשר בסיס הידע ב-FOL מכיל פונקציות (למשל $\text{Father}(x)$ או $s(x)$), יקום המונחים (Herbrand Universe) הופך לאינסופי בן-מנייה: $\{\text{John}, \text{Father}(\text{John}), \text{Father}(\text{Father}(\text{John})), \dots\}$. כיצד מחשב סופי יכול להוכיח נביעה לוגית מעל יקום אינסופי?
אם קבוצת פסוקיות ב-FOL אינה ספיקה (כלומר מכילה סתירה), אזי קיימת תת-קבוצה סופית של מונחי קרקע (Ground Terms) מתוך יקום ארברנד שהשמתם בפסוקיות יוצרת סתירה בתחשיב הפסוקים!
לוגיקה מסדר ראשון היא חצי-כריעה (Semi-Decidable) בלבד (ואינה כריעה באופן מלא - Undecidable). הוכחת המשפט מתבססת על רדוקציה מלאה מבעיית העצירה של טיורינג (Halting Problem) לבעיית הנביעה הלוגית ב-FOL.
| ענף לוגי | סטטוס כריעות | התנהגות כאשר $KB \models \alpha$ | התנהגות כאשר $KB \not\models \alpha$ |
|---|---|---|---|
| תחשיב הפסוקים (PL) | כריע לחלוטין (Decidable) | מוצא הוכחה ועוצר (סופי, $2^n$ שורות) | קובע אי-נביעה ועוצר בהכרח |
| FOL מונו-אדי (Monadic FOL - ללא פונקציות) | כריע (Decidable) | מוצא הוכחה ועוצר | קובע אי-נביעה ועוצר (מרחב מודלים חסום) |
| FOL כללי (כולל יחסים וסמלי פונקציות) | חצי-כריע בלבד (Semi-Decidable) | מובטח למצוא הוכחה ולעצור! (שלמות גדל) | עלול לרוץ לנצח בלולאה אינסופית! |
2. אלגוריתם ההאחדה (Unification) ומבחן ה-Occurs Check
במקום לפרוס את כל ההצבות האפשריות, אלגוריתם ההאחדה מוצא הצבה $\theta$ (Substitution) שהופכת שני ביטויים שונים לזהים לחלוטין: $\text{Unify}(\alpha, \beta) = \theta \iff \text{SUBST}(\theta, \alpha) = \text{SUBST}(\theta, \beta)$. האלגוריתם מחזיר תמיד את המאחד הכללי ביותר (MGU - Most General Unifier), ששומר על משתנים חופשיים ככל הניתן.
💻 הפסאודוקוד הפורמלי של אלגוריתם ההאחדה (UNIFY Algorithm)
Russell & Norvig / Nir Adar
הפונקציה OCCURS_CHECK(var, x) סורקת את הביטוי $x$ ובודקת האם המשתנה $var$ מוכל בתוכו.
אם ננסה לאחד את המשתנה $x$ עם הביטוי $f(x)$, ללא Occurs Check תיווצר ההצבה $\{x / f(x)\}$.
הצבה זו מובילה למבנה אינסופי מעגלי בלתי אפשרי: $x = f(f(f(\dots)))$!
| ביטוי ראשון (p) | ביטוי שני (q) | תוצאת ההאחדה (θ) | הסבר |
|---|---|---|---|
| Knows(John, x) | Knows(John, Jane) | { x / Jane } | הצבה ישירה של קבוע למשתנה. |
| Knows(John, x) | Knows(y, OJ) | { y / John, x / OJ } | הצבה צולבת של שני משתנים לשני קבועים. |
| Knows(John, x) | Knows(y, Mother(y)) | { y / John, x / Mother(John) } | הצבת פונקציה מקוננת לאחר שיערוך y. |
| Knows(John, x) | Knows(x, OJ) | FAIL (קריסה) | המשתנה x לא יכול להיות גם John וגם OJ. |
| P(x) | P(Father(x)) | FAIL (Occurs Check) | המשתנה x מופיע בתוך הביטוי שאליו הוא מוצב! |
⚡ מודוס פוננס המורחב (Generalized Modus Ponens - GMP)
מאפשר להסיק מסקנה ישירה בלוגיקה מסדר ראשון במכה אחת: \[\frac{p_1', p_2', \dots, p_n', \quad (p_1 \wedge p_2 \wedge \dots \wedge p_n \Rightarrow q)}{\text{SUBST}(\theta, q)} \quad \text{where } \text{Unify}(p_i', p_i) = \theta \text{ for all } i\]
3. ששת שלבי ההמרה ל-CNF בלוגיקה מסדר ראשון (FOL CNF Conversion)
ב-FOL, ההמרה ל-CNF מורכבת יותר ודורשת טיפול ייחודי בכמתים ובשמות משתנים:
4. הוכחת רזולוציה מלאה: פרשת "Criminal(West)"
זוהי דוגמת הדגל הקלאסית בספרות הבינה המלאכותית (Russell & Norvig). נתונה השאילתה: להוכיח כי האמריקאי קולונל ווסט שמכר טילים למדינת Nono העוינת הוא פושע ($\text{Criminal}(\text{West})$).
- רזולוציה בין $\neg\text{Criminal}(\text{West})$ לחוק $C_1$ $\to$ הצבה $\{x/\text{West}\}$ ומחיקת $\text{Criminal}$.
- רזולוציה מול העובדה $C_2$ ($\text{American}(\text{West})$) $\to$ מחיקת $\neg\text{American}$.
- רזולוציה מול $C_4$ ו-$C_3$ (טיל $M_1$ הוא נשק) $\to$ הצבה $\{y/M_1\}$ ומחיקת $\neg\text{Weapon}$.
- רזולוציה מול $C_5$ (מכירה ל-Nono) $\to$ הצבה $\{z/\text{Nono}\}$ ומחיקת $\neg\text{Sells}$. נותר: $\neg\text{Hostile}(\text{Nono})$.
- רזולוציה מול $C_6$ ו-$C_7$ ($Nono$ היא אויב לכן עוינת) $\to$ מחיקת $\neg\text{Hostile}$ וגזירת הפסוקית הריקה $\square$!
🧭 אסטרטגיות רזולוציה מתקדמות (Resolution Strategies)
מחייבת שכל צעד ישלב לפחות פסוקית אחת שניגזרה משלילת השאילתה. מונעת התפזרות להוכחת עובדות לא קשורות ושומרת על שלמות!
מחייבת שאחת הפסוקיות תהיה בעלת ליטרל יחיד. מקטינה גודל פסוקיות אך אינה שלמה ל-FOL מלא.
מוחקת פסוקיות חלשות שמוכלות כבר על ידי פסוקיות כלליות יותר (למשל מחיקת $P(a) \vee Q(b)$ אם קיים $P(x)$).
5. סימולציה אינטראקטיבית 6.5: מעבדת ההאחדה ועץ הרזולוציה
צ'יט-שיט מאסטר: מפת הדרכים הלוגית וגשר לפרק 7
סיכום מקיף של כל שיטות הייצוג וההיסק, מטריצת השוואה כוללת של כל אלגוריתמי הפרק, עשרת כללי הברזל למבחן, והכנה לחקר תכנון וסוכני פעולה בזמן (Planning).
לקשור את כל הקצוות יחד
השלמתם בהצלחה את פרק 6 – אחד הפרקים המאתגרים והיפים ביותר בקורס! ביחידה זו ריכזתי עבורכם את מטריצת האלגוריתמים המלאה, את עשרת כללי הברזל שיצילו אתכם מכל מלכודת בבחינה, וכרטיסיות של כל החוקים. שמרו דף זה פתוח כשתפתרו תרגילים ושאלות העמקה!
1. מטריצת ההשוואה הכוללת: כל אלגוריתמי ההיסק של פרק 6
| אלגוריתם | שפת קלט | סיבוכיות זמן (גרוע) | סיבוכיות מקום | שלמות (Complete) | נאותות (Sound) | שימוש מרכזי |
|---|---|---|---|---|---|---|
| סריקת טבלאות אמת (TT) | פסוקים כלליים | O(2ⁿ) | O(n) | כן ✓ | כן ✓ | הבנה תיאורטית בסיסית בלבד |
| אלגוריתם DPLL | CNF בוליאני | O(2ⁿ) (בפועל מהיר בהרבה) | O(n) | כן ✓ | כן ✓ | אימות חומרה (Verification) |
| אלגוריתם WalkSAT | CNF בוליאני | O(MaxFlips) | O(n + m) | לא ✕ | כן ✓ | בעיות ענק שידוע כי הן ספיקות |
| שרשור קדימה (FC) | פסוקיות הורן | O(n) - לינארי! | O(n) | כן (להורן) | כן ✓ | עיבוד נתונים תחושתי מתמשך |
| שרשור לאחור (BC) | פסוקיות הורן | < O(n) (תלוי יעד) | O(עומק עץ) | כן (להורן) | כן ✓ | מנועי פרולוג (Prolog) ושאילתות יעד |
| רזולוציה מלאה (PL/FOL) | CNF / FOL-CNF | חצי-כריע ב-FOL | תלוי עץ | כן (Refutation) | כן ✓ | מנועי הוכחת משפטים אוטומטיים (ATP) |
2. עשרת כללי הברזל למבחן בבינה מלאכותית
$\models$ הוא יחס סמנטי (Meta-relation) בין עולמות: $KB \models \alpha$. לעומתו $\Rightarrow$ הוא קשר לוגי פנימי בתוך פסוק. הקשר ביניהם: $KB \models \alpha \iff (KB \Rightarrow \alpha)$ הוא טאוטולוגיה.
החלפה אוטומטית שחייבת לזרום לכם בעיניים: $\alpha \Rightarrow \beta \equiv \neg\alpha \vee \beta$. זכרו ש-$\neg(\neg\alpha) \equiv \alpha$.
$\forall x \text{ P}(x) \Rightarrow \text{Q}(x)$ ולא עם $\wedge$! שימוש ב-$\wedge$ יכפה שכל דבר ביקום (כולל סלעים) מקיים את הטענה.
$\exists x \text{ P}(x) \wedge \text{Q}(x)$ ולא עם $\Rightarrow$! שימוש בגרירה הופך את הפסוק לאמיתי ריקית ברגע שקיים עצם כלשהו שאינו מקיים את הרישא.
מתוך $\forall x \exists y \text{ Loves}(x,y)$, אסור להציב קבוע $C_1$! חובה להציב פונקציית סקולם $F(x)$, שכן ה-$y$ תלוי ב-$x$.
ברזולוציה הוכחנו סתירה! המשמעות היא ששלילת השאילתה אינה ספיקה, ולכן השאילתה תקפה ונובעת מה-$KB$.
זכרו את מנגנון המונה `count[c]` של PL-FC-Entails שמתנכה ומונע סריקה חוזרת של כללים.
באלגוריתם ההאחדה, אסור להציב משתנה במונח המכיל את עצמו ($x / f(x)$). הדבר יגרום ללולאה אינסופית.
אם הוא החזיר מודל – המודל אמיתי בהכרח. אך אם נעצר ללא פתרון, לא ניתן לדעת האם הפסוק בלתי ספיק או שפשוט לא חיפשנו מספיק.
לפי משפט ארברנד: הוכחה תמיד תימצא בזמן סופי אם היא קיימת. אך אם אין נביעה, האלגוריתם עלול לרוץ לנצח.
הגשר הפדגוגי לפרק 7: מתחשיב פסוקים לתכנון פעולות (Planning)
לאורך פרק 6 ראינו כיצד סוכן מייצג את מצב העולם הסטטי בעזרת לוגיקה. אולם בעולם האמיתי, סוכן חייב לבצע פעולות המשנות את המצב לאורך זמן! אם ננסה לייצג כל פעולה בלוגיקה רגילה, ניתקל ב"בעיית המסגרת" (Frame Problem): איך מצהירים שמה שלא השתנה – נשאר כפי שהיה מבלי לכתוב מיליוני פסוקי שימור? בפרק 7 נלמד על שפות תכנון קלאסיות כמו STRIPS ו-PDDL, נבין כיצד פעולות מוגדרות על ידי תנאים מוקדמים (Preconditions) ותוצאות (Effects), ונראה כיצד אלגוריתמי חיפוש ותכנון גרפים (GraphPlan) יוצרים תוכניות פעולה מורכבות שמגיעות למטרות עתידיות. נתראה בפרק 7!