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

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

6.1.3. אלגוריתם הרזולוציה: (ללא משתנים)

נתונה קבוצה אקסיומות A, נוסחה P אותה אנחנו רוצים להוכיח.

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

האלגוריתם:

הפוך את $plot:\[A \wedge \neg P\]$ לקבוצת פסוקיות $plot:\[E\]$ .
אתחל: $plot:\[D \leftarrow E\]$ .
המשך עד אשר לפחות מהתנאים הבאים מתקיים:

- נמצאה סתירה.

- לא ניתן להמשיך.

- המשאבים שהוקצו להוכחה נצרכו.

בחר שתי פסוקיות ב- $plot:\[D\]$ מהצורה: $plot:\[A = \left\{ {{A_1},...,{A_n},L} \right\},B = \left\{ {{B_1},...,{B_m},\neg L} \right\}\]$ .
$plot:\[D \leftarrow D \cup \left\{ {\left\{ {{A_1},...,{A_n},{B_1},...,{B_m}} \right\}} \right\}\]$ .

בסיום:

אם הפרוצדורה עצרה בגלל סתירה, החזר "כן". (P נובעת מ-A).
אם הפרוצדורה עצרה מחוסר אפשרות להמשיך, החזר "לא".
אם הפרוצדורה עצרה מחוסר משאבי חיפוש, החזר "לא ידוע".

תכונות תהליך הרזולוציה:

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