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

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

העברת נוסחאות לצורת CNF

שלב 1: הסרת סימני הגרירה $plot:\[ \to \]$ .

כדי לבצע זאת, נשתמש בשקילות: $plot:\[A \to B \equiv \neg A \vee B\]$

דוגמא: $plot:\[\forall s\forall t\left[ {\forall x\left[ { \in \left( {x,s} \right) \to \in \left( {x,t} \right)} \right] \to \subseteq \left( {s,t} \right)} \right]\]$

יהפוך ל- $plot:\[\forall s\forall t\left[ {\neg \forall x\left[ {\neg \in \left( {x,s} \right) \vee \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right]\]$ .

שלב 2: הקטן את טווח השלילות לפסוקים אטומיים

כדי לעשות זאת, נשתמש בשקילויות הבאות:

$plot:\[\neg \left( {\neg A} \right) \equiv A\]$	$plot:\[\neg \left( {A \wedge B} \right) = \neg A \vee \neg B\]$	$plot:\[\neg \left( {A \vee B} \right) = \neg A \wedge \neg B\]$
$plot:\[\neg \exists X\left[ {P\left( X \right)} \right] \equiv \forall X\left[ {\neg P\left( X \right)} \right]\]$	$plot:\[\neg \forall X\left[ {P\left( X \right)} \right] \equiv \exists X\left[ {\neg P\left( X \right)} \right]\]$

דוגמא:

$plot:\[\begin{gathered} \forall s\forall t\left[ {\neg \forall x\left[ {\neg \in \left( {x,s} \right) \vee \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \Rightarrow \hfill \\ \forall s\forall t\left[ {\exists x\neg \left[ {\neg \in \left( {x,s} \right) \vee \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \Rightarrow \hfill \\ \forall s\forall t\left[ {\exists x\left[ {\neg \neg \in \left( {x,s} \right) \wedge \neg \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \Rightarrow \hfill \\ \forall s\forall t\left[ {\exists x\left[ { \in \left( {x,s} \right) \wedge \neg \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \hfill \\ \end{gathered} \]$

שלב 3: שנה את שמות המשתנים כך שלא יופיע אותו שם בשני כמתים

לדוגמא, הנוסחה $plot:\[\forall xP\left( x \right) \vee \forall xQ\left( x \right)\]$ תהפוך ל- $plot:\[\forall xP\left( x \right) \vee \forall yQ\left( y \right)\]$ .

שלב 4: העבר את כל הכמתים לתחילת הנוסחה תוך שמירה על סדר הופעתם

$plot:\[\begin{gathered} \forall s\forall t\left[ {\exists x\left[ { \in \left( {x,s} \right) \wedge \neg \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \Rightarrow \hfill \\ \forall s\forall t\exists x\left[ {\left[ { \in \left( {x,s} \right) \wedge \neg \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \hfill \\ \end{gathered} \]$

שלב 5: הסר את הכמתים הישיים בתהליך סקולומיזציה:

כמת ישי = $plot:\[\exists \]$ .

יהי $plot:\[n\]$ מספר הכמתים הכוללים משמאל לכמת הישי. הנוסחה עם הכמת הישי נמצאת בטווח $plot:\[n\]$ הכמתים. יהיו $plot:\[{x_1},...,{x_n}\]$ המשתנים של הכמתים הללו.
החלף את כל ההופעות של המשתנה של הכמת הישי בפונקציה חדשה בעלת שם כלשהו חדש (שאינו מופיע במקום אחר) בעלת $plot:\[n\]$ ארגומנטים $plot:\[{x_1},...,{x_n}\]$ . הפונקציה הזו נקראת פונקצית סקולם. לדוגמא, $plot:\[\forall {X_1}...\forall {X_n}\exists Y\left[ {p\left( {Y,{X_1},...,{X_n}} \right)} \right]\]$ תהפוך ל- $plot:\[\forall {X_1}...\forall {X_n}\left[ {p\left( {{f_{20}}\left( {{X_1},...,{X_n}} \right),{X_1},...,{X_n}} \right)} \right]\]$ כאשר $plot:\[{f_{20}}\]$ הינו שם פונקציה חדש.
אם לא קיימים כמתים כוליים משמאל, הפונקציה תהיה בעלת 0 ארגומנטים ונקראת קבוע סקולם.

$plot:\[\begin{gathered} \forall s\forall t\exists x\left[ {\left[ { \in \left( {x,s} \right) \wedge \neg \in \left( {x,t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \Rightarrow \hfill \\ \forall s\forall t\left[ {\left[ { \in \left( {F(s,t),s} \right) \wedge \neg \in \left( {F(s,t),t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \hfill \\ \end{gathered} \]$

שלב 6: הסר את כל הכמתים הכוללים

בשלב זה קיימים רק כמתים כוללים. מסירים אותם וזוכרים שכל המשתנים הינם של כמתים כוללים.

$plot:\[\begin{gathered} \forall s\forall t\left[ {\left[ { \in \left( {F(s,t),s} \right) \wedge \neg \in \left( {F(s,t),t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \Rightarrow \hfill \\ \left[ {\left[ { \in \left( {F(s,t),s} \right) \wedge \neg \in \left( {F(s,t),t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \hfill \\ \end{gathered} \]$

שלב 7: הפוך את הנוסחה לקוניונקציה של דיסיונקטים

נשתמש בשקילות: $plot:\[\left( {A \wedge B} \right) \vee C \equiv \left( {A \vee C} \right) \wedge \left( {B \vee C} \right)\]$

$plot:\[\begin{gathered} \left[ {\left[ { \in \left( {F(s,t),s} \right) \wedge \neg \in \left( {F(s,t),t} \right)} \right] \vee \subseteq \left( {s,t} \right)} \right] \Rightarrow \hfill \\ \left[ { \in \left( {F(s,t),s} \right) \vee \subseteq \left( {s,t} \right)} \right] \wedge \left[ {\neg \in \left( {F(s,t),t} \right) \vee \subseteq \left( {s,t} \right)} \right] \hfill \\ \end{gathered} \]$

שלב 8: נקרא לכל דיסיונקציה בשם clause. שנה שמות משתנים כך שבכל clause יהיו שמות אחרים.

נשתמש בשקילות הבאה: $plot:\[\forall X\left[ {P\left( X \right) \wedge Q\left( X \right)} \right] \equiv \forall X\left[ {P\left( X \right)} \right] \wedge \forall X\left[ {Q\left( X \right)} \right]\]$

$plot:\[\begin{gathered} \left[ { \in \left( {F(s,t),s} \right) \vee \subseteq \left( {s,t} \right)} \right] \wedge \left[ {\neg \in \left( {F(s,t),t} \right) \vee \subseteq \left( {s,t} \right)} \right] \hfill \\ \Downarrow \hfill \\ \left[ { \in \left( {F({x_1},{x_2}),{x_1}} \right) \vee \subseteq \left( {{x_1},{x_2}} \right)} \right] \wedge \hfill \\ \left[ {\neg \in \left( {F({x_3},{x_4}),{x_3}} \right) \vee \subseteq \left( {{x_3},{x_4}} \right)} \right] \hfill \\ \end{gathered} \]$