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

לוגיקה - סיכום נקודות

סיכום מאת: ניר אדר

מערכת הוכחה לתחשיב הפסוקים

אקסיומות:

כל פסוק plot:$\delta $ עבורו קיימים פסוקים plot:$\alpha ,\beta ,\gamma $ כך ש-plot:$\delta $ הוא אחד מהתבניות הבאות, הוא אקסיומה:

  1. plot:$\left( {\alpha  \to \left( {\beta  \to \alpha } \right)} \right)$
  2. plot:$\left( {\left( {\alpha  \to \left( {\beta  \to \gamma } \right)} \right) \to \left( {\left( {\alpha  \to \beta } \right) \to \left( {\alpha  \to \gamma } \right)} \right)} \right)$
  3. plot:$\left( {\left( {\left( {\alpha  \to F} \right) \to F} \right) \to \alpha } \right)$

דוגמא: plot:$\left( {\left( {{p_0} \to F} \right) \to \left( {F \to \left( {{p_0} \to F} \right)} \right)} \right)$ - אקסיומה מסוג 1, כאשר plot:$\alpha  = \left( {{p_0} \to F} \right),\beta  = F$.

כלל היסק: MP: plot:$\frac{{\alpha ,\alpha  \to \beta }}{\beta }$.

הסבר: אם א' גורר את ב', וגם א' מתקיים, הרי שב' מתקיים. MP נקרא גם כלל הניתוק.

הערה: בדיון במערכת ההוכחה בתחשיב הפסוקים נשתמש רק בקשרים plot:$\left\{ { \to ,F} \right\}$ (כאמור קשרים אלו מהווים מערכת שלמה).

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

סדרת ההוכחה היא סדרה סופית שבה כל פסוק הוא אקסיומה או מתקבל על ידי הפעלת MP מהפסוקים הקודמים.

טענה: plot:$ \vdash \left( {\alpha  \to \alpha } \right)$.

תגיות המסמך:

לפרק הקודםמערכות הוכחה פורמלית
לפרק הבאפסוקים מצורת DNF
מאת: bentz

תיקון

מציעה להחליף את
(a¬)
ב
a¬
שכן (a¬) אינו פסוק
מאת: משה ב

סמנטיקה
שיתוף:
| עוד