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

ספר אלקטרוני מאת: ניר אדר

6.1.4. רזולוציה עם משתנים

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

לדוגמא, ניתן להפוך את הליטרלים father(avraham, yzhak) ו-father(X, Y) לזהים על ידי ההצבה X/avraham, Y/yzhak, אולם אין הצבה שתהפוך את הליטרלים father(avraham, yzhak) ואת father(X, X) לזהים.

לתהליך המוצא הצבה שהופכת שני פסוקים לזהים קוראים האחדה (unification).

אלגוריתם הרזולוציה:

נתונות אוסף הנחות (נוסחאות בנויות כהלכה, אותן נכנה אקסיומות) $plot:\[{A_1},...,{A_n}\]$ ונתון משפט $plot:\[T\]$ אותו נרצה להוכיח.

הפוך את הנוסחה $plot:\[{A_1} \wedge ... \wedge {A_n} \wedge \neg T\]$ לאוסף של פסוקיות $plot:\[\left\{ {{C_1},...,{C_m}} \right\}\]$ (בצורת CNF).
התחל עם אוסף הפסוקיות $plot:\[P = \left\{ {{C_1},...,{C_m}} \right\}\]$ .
בצע את הלולאה הבאה:

בחר 2 פסוקיות $plot:\[{C_h} = \left\{ {{L_1},...,{L_h}} \right\},{C_l} = \left\{ {{D_1},...,{D_k}} \right\}\]$ כך שקיימים $plot:\[{D_j} = \varphi ,{L_i} = \neg \psi \]$ כאשר $plot:\[\psi ,\varphi \]$ ניתנים להאחדה עם הצבה $plot:\[\Theta \]$ .
תהי $plot:\[{C_{new}} = \left[ {{C_h} \cup {C_k} - \left\{ {{L_i},{D_j}} \right\}} \right]\Theta \]$ .
החלף את שמות המשתנים ב- $plot:\[{C_{new}}\]$ לשמות חדשים שלא מופיעים ב- $plot:\[P\]$ .
$plot:\[P \leftarrow P \cup \left\{ {{C_{new}}} \right\}\]$ .