הועלה לאתר:  
מספר עמודים: 120
הורדת המסמך בגרסה להדפסהלהורדת המסמך בשלמותו

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

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

2.2. תזכורת – מונחים מעולם הלוגיקה

נוסחה plot:$\alpha $ הינה אמת לוגית אם לכל מבנה plot:$m$ ולכל השמה plot:$S$ מתקיים: plot:$m,S \vDash \alpha $.

סימון: plot:\[ \vDash \alpha \]. לדוגמה: plot:$\forall x\left( {R\left( {x,y} \right) \vee \neg R\left( {x,y} \right)} \right)$

מערכת הוכחה: אוסף של כללים ליצירת טענות.

אם ניתן ליצור את plot:$\alpha $ על ידי מערכת הוכחה plot:$D$ אז נאמר ש plot:$\alpha $ יכיחה במערכת plot:$D$ ונסמן: plot:${ \vdash _D}\alpha $.

אם לא ניתן ליצור את plot:$\alpha $מהמערכת plot:$D$ נאמר כיplot:$\alpha $ איננה יכיחה ב plot:$D$ ונסמן: plot:${\not  \vdash _D}\alpha $.

מערכת הוכחה נאותה היא מערכת בה כל טענה יכיחה הינה ספיקה. plot:${ \vdash _D}\alpha  \to  \vDash \alpha $

מערכת הוכחה שלמה היא מערכת בה ניתן להוכיח כל טענה נכונה. plot:$ \vDash \alpha  \to { \vdash _D}\alpha $

תגיות המסמך:

לפרק הקודם2.1. תזכורת – תחשיב היחסים
לפרק הבא3. הוכחת נכונות של תוכניות
אין תגובות!
שיתוף:
| עוד