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

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

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

7.3. מערכת ההוכחה H*

כל האקסיומות וכללי ההיסק נשארים כמו ב-H למעט כלל REP, בהחלפת סוגריים מסולסלים בסוגריים משולשים. כלל REP החדש:

plot:\[\frac{{\left( {p\left( {\bar x,n} \right) \wedge n > 0} \right) \to B &  & \,\,\,\left\langle {p\left( {\bar x,n} \right) \wedge \left( {n > 0} \right)} \right\rangle S\left\langle {p\left( {\bar x,n - 1} \right)} \right\rangle  &  & \,\,\,p\left( {\bar x,0} \right) \to \neg B}}{{\left\langle {\exists n,p\left( {\bar x,n} \right)} \right\rangle \,\,{\text{while}}\,\,B\,\,{\text{do}}\,\,S\,\,{\text{od}}\,\,\left\langle {p\left( {\bar x,0} \right)} \right\rangle }}\]

תגיות המסמך:

לפרק הקודם7.2. מערכת ההוכחה H
לפרק הבא7.4. לוגיקות טמפורליות
אין תגובות!
שיתוף:
| עוד