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

6. שימוש בלוגיקה לייצוג ידע

המטרה שלנו: לאפשר למחשב להוכיח משפטים.

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

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

כשנרצה להוכיח נוסחה P נבנה מאגר נוסחאות אותו נקבע כאקסיומות, וננסה להוכיח את הנוסחה.

פרוצדורת ההוכחה של נוסחה:

1. הכנס את קבוצת האקסיומות ל-S
2. אם הנוסחה המבוקשת נמצאת ב-S, החזר "כן".
3. אחרת הפעל את כללי ההיסק על נוסחאות ב-S.
4. הוסף את הנוסחאות החדשות ל-S.
5. חזור לשלב 2.