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