הועלה לאתר:   10.2.2004
מספר עמודים: 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

תגובות:

שם:(התחברות)
נושא:
תוכן:
 אין לשלוח תגובות הכוללות מידע המפר את תנאי השימוש של אתר UnderWarrior לרבות דברי הסתה, דיבה וסגנון החורג מהטעם הטוב.
 אימות:
מאת: bentz

תיקון

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

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