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

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

Pronex Normal Form

שלב 1: הגדרת נוסחאות חסרות כמתים מעל מילון $plot:\[\tau \]$ - מסומן $plot:\[QF\left( \tau \right)\]$ .

בסיס: נוסחאות אטומיות. סגור: קשרים.

שלב 2: הגדרת $plot:\[PNF\left( \tau \right)\]$ : בסיס: $plot:\[QF\left( \tau \right)\]$ . סגור: כמתים.

משפט ה-PNF

לכל נוסחה $plot:\[\alpha \]$ קיימת נוסחה $plot:\[\alpha '\]$ מצורת PNF כך ש- $plot:\[\alpha ' \equiv \alpha \]$ .

ההוכחה באינדוקציית מבנה על מבנה הנוסחה.

בסיס: $plot:\[\alpha \]$ נוסחה אטומית $plot:\[\alpha \Leftarrow \]$ מצורת PNF.

סגור: נניח של- $plot:\[\alpha ,\beta \]$ קיימים שקולים $plot:\[\alpha ',\beta '\]$ מצורת PNF.

כמתים: $plot:\[\forall {v_i}\alpha \]$ , נמצא נוסחה: $plot:\[\forall {v_i}\alpha '\]$ וכך גם ל- $plot:\[\exists \]$ .

קשרים: נניח $plot:\[\left( {\alpha \to \beta } \right)\]$ , ואז:

$plot:\[\left( {\alpha ' \to \beta '} \right)\]$

מתרגמים ל- $plot:\[\left\{ {\neg , \wedge , \vee } \right\}\]$ : $plot:\[\left( {\neg \alpha ' \vee \beta '} \right)\]$

עושים renaming למשתנים הקשורים ב- $plot:\[\alpha '\]$ כך שלא יופיע ב- $plot:\[\beta '\]$ ולהיפך.

משתמשים בשקילויות הבאות:

$plot:\[\neg \forall {v_i}\varphi \equiv \exists {v_i}\neg \varphi \]$
$plot:\[\neg \exists {v_i}\varphi \equiv \forall {v_i}\neg \varphi \]$
$plot:\[\forall {v_i}\left( {\varphi \wedge \psi } \right) \equiv \forall {v_i}\varphi \wedge \forall {v_i}\psi \]$
$plot:\[\exists {v_i}\left( {\varphi \vee \psi } \right) \equiv \exists {v_i}\varphi \vee \exists {v_i}\psi \]$
אם $plot:\[{v_i}\]$ לא חופשי ב- $plot:\[\psi \]$ אז: $plot:\[\left( {\forall {v_i}\varphi \vee \psi } \right) \equiv \forall {v_i}\left( {\varphi \vee \psi } \right)\]$
אם $plot:\[{v_i}\]$ לא חופשי ב- $plot:\[\psi \]$ אז: $plot:\[\left( {\forall {v_i}\varphi \wedge \psi } \right) \equiv \forall {v_i}\left( {\varphi \wedge \psi } \right)\]$
אם $plot:\[{v_i}\]$ לא חופשי ב- $plot:\[\psi \]$ אז: $plot:\[\left( {\exists {v_i}\varphi \vee \psi } \right) \equiv \exists {v_i}\left( {\varphi \vee \psi } \right)\]$

לפרק הקודםRenaming של משתנים קשורים

לפרק הבאגדירות של יחסים במבנה

תגובות:

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

מאת: bentz

22/5/2020 16:37

תיקון

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

מאת: משה ב

16/3/2017 20:01

שיתוף:

| עוד

יש לראות בכל האמור באתר underwar.co.il מידע כללי בלבד. כל פעולה שנעשית על פי המידע והפרטים האמורים באתר underwar.co.il הינה על אחריות הגולש בלבד. בשום מקרה אתר underwar.co.il ו/או ניר אדר ו/או צוות מנהלי פורום underwar.co.il ו/או שאר חברי הפורום אינם אחראיים בשום צורה ואופן לתוצאות השימוש במידע המובא באתר זה. עשיית שימוש במידע המובא באתר underwar.co.il, הינה על אחריותו של הגולש בלבד.

פרוייקט UnderWarrior - מדריכים, מאמרים, סיכומים וחומרי לימוד בתחומי תכנות, מתמטיקה, אבטחת מידע ועוד
1997-2025 © כל הזכויות שמורות לניר אדר

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

Pronex Normal Form

תגיות המסמך:

תגובות:

תיקון

סמנטיקה

תוכן העניינים:

קישורים רלוונטיים:

שיתוף: