|
גם בחיי היומיום איננו בונים טבלאות אמת כדי לבדוק תקפותם של היסקים שאנו שומעים ומשמיעים. כשאנו רוצים לשכנע בדבר מה, אנחנו משתדלים להציג הוכחה של הדבר מתוך קבוצת הנחות. אנחנו "בונים טיעון" שבו אם השומע יקבל את ההנחות שלנו ויעקוב אחר השלבים של ההוכחה, הוא ייאלץ לקבל את המסקנה. כל שלב בהוכחה צריך להיות משמר אמת על מנת שהמסקנה תתקבל כאמיתית.
הוכחת תקפות בנויה מסדרת היסקים תקפים. כל היסק תקף בהוכחה חייב להתבצע על פי כלל היסק מותר. כללי ההיסק המותרים הם:
- חזרה
p
p
- הוספת גימום
p
s
p ^ s
- מודוס פוננס (modus ponens)
p --> s
p
s
- הוספת איווי
p
p | s
s היא טענה כלשהי
שפת התכנות פרולוג עושה שימוש בכללי היסק.
בפרולוג, תכניות מייצגות אוסף הנחות. ניתן להציג שאילתות לאור ההנחות, ובזאת לבקש מפרולוג לבדוק האם הטענה המובעת בשאילתא נובעת מן ההנחות, כלומר האם ההנחות (התכנית) והשאילתא (המסקנה) מהוות יחד היסק תקף. פרולוג מנסה להוכיח את המסקנה מתוך ההנחות על פי כללי היסק של מנגנון ההוכחה שלו.
|
