בינה מלאכותית

אסטרטגיות רזולוציה

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

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

גישות אפשריות:

1. BFS – ביצוע רזולוציה על כל הפסוקים האפשריים – יוצר רמה שניה של פסוקים. אז נבצע רזולוציה על כל הרמות הקודמות, וכו'.
2. אסטרטגית הסרה – פסוקית שאין לה משלים תיזרק. למשל, אם מופיע בפסוקית ואין אף פסוקית אחרת המכילה , אז אפשר לזרוק את הפסוקית ולהקטין את מרחב החיפוש.
   
   נכנה בשם ליטרל טהור ליטרל שאין לו משלים. בזמן הרזולוציה לא נוצרים ליטרלים טהורים. לכן רק בתחילת התהליך נזרוק פסוקיות בעלות ליטרלים טהורים.
3. הסרת טאוטולוגיות – מכיוון שטאוטולוגיה לעולם לא תביא לסתירה, הרי שהיא מיותרת.
4. רזולוציית יחידה – תמיד עדיף לבצע רזולוציה כאשר אחד מהביטויים באורך 1.
   
   למשל, רזולוציה של פסוקית מאורך 4 ופסוקית מאורך 5 ייתן פסוקית באורך 7. במקרה זה הארכנו את גודל הפסוקית. לעומת זאת אם נבצע רזולוציה בין פסוקית באורך לפסוקית באורך 1 נקבל פסוקית באורך .
   
   דגש: רזולוציית יחידה אינה שלמה – יש פעמים שהיא לא מוצאת הוכחה.
   
   רזולוציית יחידה שלמה עבור קבוצת פסוקיות הורן – שבהן יש ליטרל חיובי אחד לכל היותר (ליטרל חיובי = ליטרל ללא סימן ).
5. אסטרטגית קבוצת תמיכה (Set of support) –
   
   הרעיון של האסטרטגיה: בתהליך הרזולוציה אנחנו מנסים להראות שהנחת השלילה גורמת לסתירה (ולכן אינה ספיקה). סתירה חייבת לערב את שלילת המשפט, מכיוון שאנחנו מניחים שהאקסיומות עקביות. לפיכך בכל שלב נרצה להשתמש בפסוקית של המשפט, או צאצאית של פסוקית כזו, בנוסף לפסוקית מחוץ למשפט.
   
   הגדרה: קבוצת פסוקיות A מהווה קבוצת תמיכה עבור קבוצת פסוקיות B אם B-A ספיקה.
   
   אסטרטגית קבוצת התמיכה מחייבת שלפחות אחת משתי הפסוקיות עליהן מופעל כלל הרזולוציה תהיה מתוך קבוצת התמיכה, או צאצאית של קבוצת התמיכה. נבחר בהתחלה את קבוצת התמיכה להיות שלילת המשפט אותו אנו רוצים להוכיח.

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