#LyX 1.3 created this file. For more info see http://www.lyx.org/
\lyxformat 221
\textclass seminar
\begin_preamble
\let\olditem\item
\renewcommand\item{\olditem\raggedright{}}
\end_preamble
\options slidesec
\language hebrew
\inputencoding auto
\fontscheme default
\graphics default
\paperfontsize default
\spacing single 
\papersize Default
\paperpackage a4
\use_geometry 0
\use_amsmath 0
\use_natbib 0
\use_numerical_citations 0
\paperorientation portrait
\secnumdepth 3
\tocdepth 3
\paragraph_separation skip
\defskip medskip
\quotes_language english
\quotes_times 2
\papercolumns 1
\papersides 1
\paperpagestyle plain

\layout Standard


\begin_inset FormulaMacro 
\newcommand{\t}{\mathbf{TRUE}}
\end_inset 


\begin_inset FormulaMacro 
\newcommand{\f}{\mathbf{FALSE}}
\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout Standard
\align right 

\size giant 
שימוש בלוגיקה לייצוג ידע
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

תחשיב הפרדיקטים
\layout Itemize

תחשיב הפרדיקטים זוהי שפה לייצוג טיעונים.
\layout Itemize

לטיעונים בתחשיב הפרדיקטים יש שני מרכיבים: עצמים ותכונות שמייחסים להם.
 התכונות נקראות פרדיקטים )יחסים(.
\layout Itemize

לדוגמא: 
\begin_deeper 
\layout Itemize

כל הלימונים צהובים.
\layout Itemize

אורי סטודנט.
 
\end_deeper 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

תחשיב הפרדיקטים )תחביר(
\layout Standard
\align right 
השפה מכילה:
\layout Enumerate

סימני קבועים 
\begin_inset Formula $c_{1},c_{2},c_{3},\ldots$
\end_inset 


\layout Enumerate

סימני משתנים 
\begin_inset Formula $x_{1},x_{2},x_{3},\ldots$
\end_inset 


\layout Enumerate

לכל 
\begin_inset Formula $n$
\end_inset 

 טבעי קבוצה של סימני פונקציות 
\begin_inset Formula $n$
\end_inset 

-מקומיות: 
\begin_inset Formula $f_{1}^{n},f_{2}^{n},f_{3}^{n},\ldots$
\end_inset 


\layout Enumerate

לכל 
\begin_inset Formula $n$
\end_inset 

 טבעי חיובי קבוצה של סימני פרדיקטים 
\begin_inset Formula $n$
\end_inset 

-מקומיים: 
\begin_inset Formula $p_{1}^{n},p_{2}^{n},p_{3}^{n},\ldots$
\end_inset 


\layout Enumerate

קשרים לוגיים: 
\begin_inset Formula $\vee,\wedge,\rightarrow,\neg$
\end_inset 

.
\layout Enumerate

כמתים: 
\begin_inset Formula $\forall,\exists$
\end_inset 


\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

תחשיב הפרדיקטים )תחביר( - המשך
\layout Standard
\align right 
נגדיר את אוסף 
\emph on 
שמות העצם
\emph default 
 )ביטויים( בשפה:
\layout Itemize

קבועים.
\layout Itemize

משתנים.
\layout Itemize

אם 
\begin_inset Formula $t_{1},t_{2},\ldots,t_{n}$
\end_inset 

 שמות עצם ו- 
\begin_inset Formula $f_{k}^{n}$
\end_inset 

 סימן פונקציה 
\begin_inset Formula $n$
\end_inset 

 מקומית, אזי 
\begin_inset Formula $f_{k}^{n}(t_{1},t_{2},\ldots,t_{n})$
\end_inset 

 הינו שם עצם.
 
\layout Standard
\align right 
נגדיר את אוסף ה
\emph on 
נוסאות
\emph default 
:
\layout Itemize

אם 
\begin_inset Formula $t_{1},t_{2},\ldots,t_{n}$
\end_inset 

 הם שמות עצם, ו- 
\begin_inset Formula $p_{k}^{n}$
\end_inset 

 הוא סימן פרדיקט 
\begin_inset Formula $n$
\end_inset 

 מקומי, אזי 
\begin_inset Formula $p_{k}^{n}(t_{1},t_{2},\ldots,t_{n})$
\end_inset 

 נוסחא.
 
\newline 
נוסחא כנ"ל נקראת פסוק אטומי.
\layout Itemize

תהי 
\begin_inset Formula $\alpha$
\end_inset 

 נוסחא, אזי 
\begin_inset Formula $\neg\alpha$
\end_inset 

 נוסחא.
\layout Itemize

יהיו 
\begin_inset Formula $\alpha,\beta$
\end_inset 

 נוסחאות, אזי 
\begin_inset Formula $\alpha\vee\beta,\alpha\wedge\beta,\alpha\rightarrow\beta$
\end_inset 

 נוסחאות.
\layout Itemize

תהי 
\begin_inset Formula $\alpha$
\end_inset 

 נוסחא ויהי 
\begin_inset Formula $x$
\end_inset 

 משתנה, אזי 
\begin_inset Formula $\exists x:\alpha,\forall x:\alpha$
\end_inset 

 נוסחאות.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

הצבה
\layout Standard
\align right 
הגדרות:
\layout Itemize

משתנה 
\emph on 
קשור
\emph default 
 )
\lang english
bound
\lang hebrew
( - משתנה המופיע בנוסחא עם כמת.
\newline 
דוגמא: 
\begin_inset Formula $\forall x:Apple(x)\rightarrow Red(x)$
\end_inset 

.
\layout Itemize

משתנה 
\emph on 
חופשי
\emph default 
 )
\lang english
free
\lang hebrew
( - משתנה שאינו קשור.
\newline 
דוגמא: 
\begin_inset Formula $Apple(x)\rightarrow Red(x)$
\end_inset 

.
\layout Itemize

נוסחא תקרא 
\emph on 
פסוק
\emph default 
 אם לא מופיעים בה משתנים חופשיים.
\layout Itemize

יהיו 
\begin_inset Formula $s$
\end_inset 

 ו-
\begin_inset Formula $t$
\end_inset 

 שמות עצם, יהי 
\begin_inset Formula $x$
\end_inset 

 משתנה, נגדיר את 
\begin_inset Formula $s(x|t)$
\end_inset 

 כשם העצם המתקבל מ-
\begin_inset Formula $s$
\end_inset 

 כאשר כל מופע של המשתנה 
\begin_inset Formula $x$
\end_inset 

 מוחלף ב- 
\begin_inset Formula $t$
\end_inset 

.
\layout Itemize

תהי 
\begin_inset Formula $\alpha$
\end_inset 

 נוסחא ו-
\begin_inset Formula $t$
\end_inset 

 שם עצם, יהי 
\begin_inset Formula $x$
\end_inset 

 משתנה, נגדיר את 
\begin_inset Formula $\alpha(x|t)$
\end_inset 

 כנוסחא המתקבלת מ-
\begin_inset Formula $\alpha$
\end_inset 

 כאשר כל מופע חופשי של המשתנה 
\begin_inset Formula $x$
\end_inset 

 מוחלף בשם העצם 
\begin_inset Formula $t$
\end_inset 

.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

האקסיומות הלוגיות
\layout Standard
\align right 
קבוצת 
\emph on 
האקסיומות הלוגיות
\emph default 
 היא קבוצת הנוסחאות הבאה:
\layout Enumerate


\begin_inset Formula $\alpha\rightarrow(\beta\rightarrow\alpha)$
\end_inset 


\layout Enumerate


\begin_inset Formula $(\alpha\rightarrow(\beta\rightarrow\gamma))\rightarrow((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma))$
\end_inset 


\layout Enumerate


\begin_inset Formula $(\neg\alpha\rightarrow\beta)\rightarrow((\neg\alpha\rightarrow\neg\beta)\rightarrow\alpha)$
\end_inset 


\layout Enumerate


\begin_inset Formula $(\forall x:(\alpha\rightarrow\beta))\rightarrow(\forall x:\alpha\rightarrow\forall x:\beta)$
\end_inset 


\layout Enumerate


\begin_inset Formula $\alpha\rightarrow\forall x:\alpha$
\end_inset 

 )כאשר 
\begin_inset Formula $x$
\end_inset 

 אינו חופשי ב- 
\begin_inset Formula $\alpha$
\end_inset 

(
\layout Enumerate


\begin_inset Formula $\forall x:\alpha\rightarrow\alpha(x|t)$
\end_inset 

 )כאשר 
\begin_inset Formula $t$
\end_inset 

 הינו שם עצם ללא משתנים חופשיים שהופכים להיות קשורים כאשר מציבים אותו במקום
 
\begin_inset Formula $x$
\end_inset 

(
\layout Standard
\align right 
האקסיומות הנ"ל הינן סכימות של נוסחאות.
 ניתן להציב כל נוסחא במקום 
\begin_inset Formula $\alpha,\beta,\gamma$
\end_inset 

 לעיל כדי לקבל נוסחת אקסיומה ספציפית.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

הוכחה
\layout Itemize

תהי 
\begin_inset Formula $\Phi$
\end_inset 

 קבוצת נוסחאות ותהי 
\begin_inset Formula $\alpha$
\end_inset 

 נוסחא.
 
\emph on 
הוכחה
\emph default 
 של 
\begin_inset Formula $\alpha$
\end_inset 

 מתוך 
\begin_inset Formula $\Phi$
\end_inset 

 היא סדרה סופית ולא ריקה 
\begin_inset Formula \[
\psi_{1},\psi_{2},\ldots,\psi_{n}\]

\end_inset 

של נוסחאות המקיימת את שני התנאים הבאים:
\begin_deeper 
\layout Itemize

לכל 
\begin_inset Formula $k=1,\ldots,n$
\end_inset 

:
\begin_deeper 
\layout Itemize


\begin_inset Formula $\psi_{k}$
\end_inset 

 אקסיומה לוגית; או
\layout Itemize


\begin_inset Formula $\psi_{k}$
\end_inset 

 נוסחא ב- 
\begin_inset Formula $\Phi$
\end_inset 

; או
\layout Itemize

קיימים 
\begin_inset Formula $i,j<k$
\end_inset 

 כך ש- 
\begin_inset Formula $\psi_{i}=\psi_{j}\rightarrow\psi_{k}$
\end_inset 

.
\end_deeper 
\layout Itemize


\begin_inset Formula $\psi_{n}=\alpha$
\end_inset 


\end_deeper 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

כלל היסק ויכיחות
\layout Itemize

כלל היסק - כלל ניתוק הרישא 
\lang english
Modes ponens
\lang hebrew
:
\newline 
בהינתן נוסחאות 
\begin_inset Formula $\alpha\rightarrow\beta$
\end_inset 

 ו- 
\begin_inset Formula $\alpha$
\end_inset 

, ניתן להסיק 
\begin_inset Formula $\beta$
\end_inset 

.
\layout Itemize

בהינתן 
\begin_inset Formula $\Phi=\{\alpha,\alpha\rightarrow\beta\}$
\end_inset 

 נאמר כי 
\begin_inset Formula $\beta$
\end_inset 

 
\emph on 
יכיח
\emph default 
 מתוך 
\begin_inset Formula $\Phi$
\end_inset 

 ונסמן 
\begin_inset Formula $\Phi\vdash\beta$
\end_inset 

.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

סמנטיקה
\layout Itemize

תהי 
\begin_inset Formula $U$
\end_inset 

 קבוצת עצמים )עולם(.
\layout Itemize


\emph on 
פירוש
\emph default 
 
\begin_inset Formula $I$
\end_inset 

 הוא פונקציה הממפה איברים של השפה לאיברים של הייצוג באופן הבא:
\begin_deeper 
\layout Enumerate

הקבועים ממופים לאובייקטים בעולם.
\layout Enumerate

הפונקציות ממופות לפונקציות המתאימות בין 
\begin_inset Formula $n$
\end_inset 

-יות של איברים בעולם לאיברים בעולם.
\layout Enumerate

הפרדיקטים ממופים ליחסים בעולם.
\end_deeper 
\layout Itemize


\emph on 
השמה
\emph default 
 לכל המשתנים היא מיפוי של המשתנים החופשיים לאיברים ב-
\begin_inset Formula $U$
\end_inset 

.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

ערך האמת של נוסחאות
\layout Itemize

פונקצית הערכה של נוסחאות ממפה נוסחא ל-
\lang english
TRUE
\lang hebrew
 או 
\lang english
FALSE
\lang hebrew
:
\layout Itemize


\emph on 
ערך האמת
\emph default 
 
\begin_inset Formula $V$
\end_inset 

 של נוסחא 
\begin_inset Formula $\alpha$
\end_inset 

 תחת פירוש 
\begin_inset Formula $I$
\end_inset 

 מוגדר באופן רקורסיבי:
\begin_deeper 
\layout Itemize

אם 
\begin_inset Formula $\alpha=P(t_{1},t_{2},\ldots,t_{n})$
\end_inset 

 נוסחא אטומית אזי:
\begin_deeper 
\layout Itemize

אם 
\begin_inset Formula $I(P)\left\langle I(t_{1}),I(t_{2}),\ldots,I(t_{n})\right\rangle $
\end_inset 

, אזי 
\begin_inset Formula $V(\alpha)=\t$
\end_inset 

.
\end_deeper 
\end_deeper 
\layout Itemize

אחרת, 
\begin_inset Formula $V(\alpha)=\f$
\end_inset 

.
\layout Itemize

אם 
\begin_inset Formula $\alpha=\neg\beta$
\end_inset 

 אזי 
\begin_inset Formula $V(\alpha)$
\end_inset 

 יקבע עפ"י טבלת האמת של 
\begin_inset Formula $\neg$
\end_inset 

 עבור 
\begin_inset Formula $V(\beta)$
\end_inset 

.
\layout Itemize

אם 
\begin_inset Formula $\alpha=\beta\vee\gamma$
\end_inset 

 או 
\begin_inset Formula $\alpha=\beta\wedge\gamma$
\end_inset 

 או 
\begin_inset Formula $\alpha=\beta\rightarrow\gamma$
\end_inset 

 אזי 
\begin_inset Formula $V(\alpha)$
\end_inset 

 יקבע עפ"י טבלת האמת של הקשרים 
\begin_inset Formula $\rightarrow,\wedge,\vee$
\end_inset 

 בהתאמה עבור 
\begin_inset Formula $V(\beta)$
\end_inset 

 ו- 
\begin_inset Formula $V(\gamma)$
\end_inset 

.
\layout Itemize

אם 
\begin_inset Formula $\alpha=\forall x:\beta$
\end_inset 

 אזי:
\begin_deeper 
\layout Itemize

אם לכל השמה של איבר מ-
\begin_inset Formula $U$
\end_inset 

 ב-
\begin_inset Formula $x$
\end_inset 

 נקבל 
\begin_inset Formula $V(\beta)=\t$
\end_inset 

, אז 
\begin_inset Formula $V(\alpha)=\t$
\end_inset 

.
\layout Itemize

אחרת, 
\begin_inset Formula $V(\alpha)=\f$
\end_inset 

.
\end_deeper 
\layout Itemize

הערה: 
\begin_inset Formula $\exists x:\beta$
\end_inset 

 שקול ל: 
\begin_inset Formula $\neg\forall x:\neg\beta$
\end_inset 

.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

טבלאות האמת
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
hfill{}
\end_inset 


\begin_inset  Tabular
<lyxtabular version="3" rows="3" columns="2">
<features>
<column alignment="center" valignment="top" leftline="true" width="0">
<column alignment="center" valignment="top" leftline="true" rightline="true" width="0">
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\alpha$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\neg\alpha$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
</lyxtabular>

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
hfill{}
\end_inset 

 
\begin_inset  Tabular
<lyxtabular version="3" rows="5" columns="3">
<features>
<column alignment="center" valignment="top" leftline="true" width="0">
<column alignment="center" valignment="top" leftline="true" width="0">
<column alignment="center" valignment="top" leftline="true" rightline="true" width="0">
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\alpha$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\beta$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\alpha\vee\beta$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
</row>
</lyxtabular>

\end_inset 

 
\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
hfill{}
\end_inset 


\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
hfill{}
\end_inset 


\begin_inset  Tabular
<lyxtabular version="3" rows="5" columns="3">
<features>
<column alignment="center" valignment="top" leftline="true" width="0">
<column alignment="center" valignment="top" leftline="true" width="0">
<column alignment="center" valignment="top" leftline="true" rightline="true" width="0">
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\alpha$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\beta$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\alpha\wedge\beta$
\end_inset 

 
\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
</row>
</lyxtabular>

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
hfill{}
\end_inset 


\begin_inset  Tabular
<lyxtabular version="3" rows="5" columns="3">
<features>
<column alignment="center" valignment="top" leftline="true" width="0">
<column alignment="center" valignment="top" leftline="true" width="0">
<column alignment="center" valignment="top" leftline="true" rightline="true" width="0">
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\alpha$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\beta$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\alpha\rightarrow\beta$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
<row topline="true" bottomline="true">
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{F}$
\end_inset 


\end_inset 
</cell>
<cell alignment="center" valignment="top" topline="true" leftline="true" rightline="true" usebox="none">
\begin_inset Text

\layout Standard


\begin_inset Formula $\mathbf{T}$
\end_inset 


\end_inset 
</cell>
</row>
</lyxtabular>

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
hfill{}
\end_inset 


\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

ספיקות
\layout Itemize

פירוש 
\begin_inset Formula $I$
\end_inset 

 
\lang english
(interpretation)
\lang hebrew
 והשמה 
\begin_inset Formula $V$
\end_inset 

 מספקים נוסחא אם"ם הנוסחא מקבלת ערך 
\lang english
TRUE
\lang hebrew
 תחת הפירוש וההשמה.
\layout Itemize

קבוצת פסוקים 
\begin_inset Formula $\Phi$
\end_inset 

 
\emph on 
גוררת לוגית
\emph default 
 פסוק 
\begin_inset Formula $\alpha$
\end_inset 

 אם"ם כל פירוש והשמה שמספקים את 
\begin_inset Formula $\Phi$
\end_inset 

 מספקים גם את 
\begin_inset Formula $\alpha$
\end_inset 

.
 נסמן: 
\begin_inset Formula $\Phi\models\alpha$
\end_inset 

.
\layout Itemize


\series bold 
משפט השלמות
\series default 
: נוסחא נובעת לוגית מקבוצת נוסחאות אם"ם היא יכיחה מתוכן:
\begin_inset Formula \[
\Phi\vdash\alpha\Leftrightarrow\Phi\models\alpha\]

\end_inset 


\layout Itemize

משפט השלמות מקשר בין סינטקס לסמנטיקה.
\layout Itemize

משפט השלמות מספק כלי לבדיקת גרירה לוגית.
 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

ייצוג ידע )
\lang english
Knowledge Representation
\lang hebrew
(
\layout Itemize

ייצוג עצמים:
\begin_deeper 
\layout Standard
\align left 

\lang english
Table (my_desk)
\layout Standard
\align left 

\lang english
Car (my_suzuki)
\end_deeper 
\layout Itemize

ייצוג תכונות של עצמים:
\begin_deeper 
\layout Standard
\align left 

\lang english
Num_of_legs(my_desk,4)
\layout Standard
\align left 

\lang english
Color (my_suzuki, silver)
\end_deeper 
\layout Itemize

ייצוג תכונות כלליות של עצמים:
\begin_deeper 
\layout Standard
\align left 

\lang english

\begin_inset Formula $\forall x:[\textrm{\L{Table}}(x)\rightarrow\textrm{\L{Num\_ of\_ legs}}(x,4)]$
\end_inset 


\end_deeper 
\layout Itemize

ייצוג יחסים בין עצמים:
\begin_deeper 
\layout Standard
\align left 

\lang english
Parent (avraham, izak)
\layout Standard
\align left 

\lang english
On (coffee_glass, my_desk)
\end_deeper 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

ייצוג ידע - המשך
\layout Itemize

ייצוג יחסים כלליים:
\begin_deeper 
\layout Standard

הגדרת יחס 
\lang english
Above
\lang hebrew
 לפי קואורדינאטת גובה של עצמים: 
\begin_inset Formula \[
\forall x\forall y[\textrm{\L{Greater}}(\textrm{\L{z\_ coord}}(x),\textrm{\L{z\_ coord}}(y))\rightarrow\textrm{\L{Above}}(x,y)]\]

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
vspace{-1em}
\end_inset 


\end_deeper 
\layout Itemize

ייצוג תכונות של יחסים:
\begin_deeper 
\layout Standard

טרנזיטיביות של יחס 
\lang english
Above
\lang hebrew
: 
\begin_inset Formula \[
\forall x\forall y\forall z[\textrm{\L{Above}}(x,y)\wedge\textrm{\L{Above}}(y,z)\rightarrow\textrm{\L{Above}}(x,z)]\]

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
vspace{-1em}
\end_inset 


\end_deeper 
\layout Itemize

ייצוג היררכיות: 
\begin_inset Formula \[
\begin{array}{l}
\forall x:[\textrm{\L{Work\_ Table}}(x)\rightarrow\textrm{\L{Table}}(x)]\\
\forall x:[\textrm{\L{Table}}(x)\rightarrow\textrm{\L{Num\_ of\_ legs}}(x,4)]\\
\textrm{\L{Work\_ Table}}(\textrm{\L{my\_ desk}})\end{array}\]

\end_inset 


\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

ייצוג ידע - דוגמא
\layout Standard
\align right 
המירו את המשפטים הבאים לייצוג לוגי:
\layout Itemize


\lang english
Jack owns a dog.
\layout Itemize


\lang english
Every dog owner is an animal lover.
\layout Itemize


\lang english
No animal lover kills an animal.
\layout Itemize


\lang english
Either Jack or Curiosity killed the cat, who is named Tuna.
\layout Itemize


\lang english
Did Curiosity kill the cat?
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

פרוצדורת הוכחה
\layout Itemize

פרוצדורה שבהינתן משפט )נוסחא יכיחה( תמצא לו הוכחה.
\layout Itemize


\series bold 
אם נוסחא אינה משפט אזי לא מובטח לנו שפרוצדורה כזו תעצור!
\layout Standard
\align right 

\series bold 
הפרוצדורה:
\layout Enumerate


\begin_inset Formula $S\leftarrow\emptyset$
\end_inset 

.
\layout Enumerate

הוסף אקסיומה ל- 
\begin_inset Formula $S$
\end_inset 

 לפי מניה כלשהי של האקסיומות.
\layout Enumerate

הפעל את כללי ההיסק על נוסחאות ב-
\begin_inset Formula $S$
\end_inset 

.
\layout Enumerate

הוסף את הנוסחאות החדשות ל-
\begin_inset Formula $S$
\end_inset 

.
\layout Enumerate

אם הנוסחא המבוקשת נמצאת ב-
\begin_inset Formula $S$
\end_inset 

, החזר "כן".
\layout Enumerate

אחרת, חזור ל-2.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

רזולוציה
\layout Itemize

פרוצדורה יעילה יותר ופשוטה יותר למימוש הינה הרזולוציה.
\layout Itemize

פרוצדורה זו מסתמכת על מבנה קנוני של נוסחאות 
\lang english
CNF (Conjuctive Normal Form)
\lang hebrew
:
\begin_inset Formula \[
(L_{11}\vee L_{12}\vee\cdots\vee L_{1n^{1}})\wedge\cdots\wedge(L_{m1}\vee L_{m2}\vee\cdots\vee L_{mn^{m}})\]

\end_inset 


\layout Itemize


\begin_inset Formula $L_{ij}$
\end_inset 

נקרא ליטרל - פסוק אטומי או שלילת פסוק אטומי.
\layout Itemize

כל אחת מהשורות נקראת פסוקית 
\lang english
(clause)
\lang hebrew
.
\layout Itemize

לנוסחת 
\lang english
CNF
\lang hebrew
 מתייחסים כקבוצת פסוקיות ולכל פסוקית כקבוצת ליטרלים.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

אלגוריתם הרזולוציה )ללא משתנים(
\layout Enumerate

הנחה: האקסיומות והנוסחא אותה נרצה להוכיח חסרות משתנים.
\layout Enumerate

קלט: קבוצת אקסיומות 
\begin_inset Formula $A$
\end_inset 

, נוסחא 
\begin_inset Formula $P$
\end_inset 

 )אותה רוצים להוכיח(
\layout Enumerate

הפוך את 
\begin_inset Formula $A\cup\{\neg P\}$
\end_inset 

 לקבוצת פסוקיות 
\begin_inset Formula $E$
\end_inset 

.
\layout Enumerate

אתחל 
\begin_inset Formula $D\leftarrow E$
\end_inset 

.
\layout Enumerate


\begin_inset LatexCommand \label{enu:res-loop}

\end_inset 

בחר שתי פסוקיות ב- 
\begin_inset Formula $D$
\end_inset 

 מהצורה: 
\begin_inset Formula \[
A=\{ A_{1},\ldots A_{n},L\};B=\{ B_{1},\ldots B_{m},\neg L\}\]

\end_inset 


\layout Enumerate

עדכן: 
\begin_inset Formula $D\leftarrow D\cup\{\{ A_{1},\ldots A_{n},B_{1},\ldots B_{m}\}\}$
\end_inset 

.
\layout Enumerate

אם לא ניתן להמשיך - החזר "לא".
\layout Enumerate

אם נמצאה סתירה )
\begin_inset Formula $\emptyset\in D$
\end_inset 

( - החזר "כן".
\layout Enumerate

אם משאבי החישוב שהוקצו נצרכו - החזר "לא ידוע".
\layout Enumerate

חזור ל- 
\begin_inset LatexCommand \ref{enu:res-loop}

\end_inset 

.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

אלגוריתם הרזולוציה )ללא משתנים( - הערות
\layout Itemize

כדי לקבל פסוקית ריקה, 
\begin_inset Formula $D$
\end_inset 

 צריך להכיל שתי פסוקיות 
\begin_inset Formula $\{ L\}$
\end_inset 

 ו- 
\begin_inset Formula $\{\neg L\}$
\end_inset 

.
 זוג פסוקיות כאלו מובילות לסתירה כיוון שבין כל הפסוקיות קיים קשר 
\begin_inset Formula $\wedge$
\end_inset 

.
\layout Itemize

פרוצדורת הרזולוציה מבצעת הוכחה בדרך השלילה )מוכיחה כי שלילת המשפט מובילה
 לסתירה(.
\layout Itemize

כלל הרזולוציה שומר על נכונות.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

טענות לגבי תהליך הרזולוציה
\layout Itemize

תהליך הרזולוציה 
\emph on 
נאות
\emph default 
 
\lang english
(sound)
\lang hebrew
.
 כל פסוקית שנגזרה מקבוצת פסוקיות 
\begin_inset Formula $D$
\end_inset 

 ע"י תהליך הרזולוציה, נובעת לוגית מ-
\begin_inset Formula $D$
\end_inset 

.
\layout Itemize

תהליך הרזולוציה הינו 
\emph on 
\lang english
refutation complete
\emph default 
\lang hebrew
.
 אם קבוצת פסוקיות 
\begin_inset Formula $D$
\end_inset 

 אינה ספיקה, ניתן לגזור מ-
\begin_inset Formula $D$
\end_inset 

 את הפסוקית הריקה.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

אלגוריתם הרזולוציה עם משתנים
\layout Itemize

כעת נסיר את ההנחה כי האקסיומות והנוסחא אותה נרצה להוכיח חסרות משתנים.
\layout Itemize

במקרה זה בצעד 
\begin_inset LatexCommand \ref{enu:res-loop}

\end_inset 

 של האלגוריתם, במקום לחפש שני ליטרלים זהים כאשר אחד מהם מופיע עם סימן שלילה,
 אנו נחפש שני ליטרלים שניתן להפוך אותם לזהים ע"י הצבה מתאימה.
 
\layout Itemize

לתהליך המוצא הצבה שהופכת שני פסוקים לזהים קוראים 
\emph on 
האחדה
\emph default 
 
\lang english
(unification)
\lang hebrew
.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

פרוצדורות בתהליך הרזולוציה
\layout Itemize

כדי לממש את הרזולוציה עם משתנים עלינו להוסיף את הפרוצדורות הבאות:
\begin_deeper 
\layout Itemize

הפיכת נוסחא כלשהי לקבוצת פסוקיות 
\lang english
(CNF)
\lang hebrew
.
\layout Itemize

מציאת הצבה מאחדת )יוניפיקציה(.
\end_deeper 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

העברת נוסחאות לצורת 
\lang english
CNF
\layout Itemize

הסר את סימני הגרירה 
\begin_inset Formula $\rightarrow$
\end_inset 

.
 השתמש בשקילות: 
\begin_inset Formula \[
A\rightarrow B\equiv\neg A\vee B\]

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
vspace{-1em}
\end_inset 


\layout Itemize

הקטן את טווח השליליות לפסוקים אטומיים.
 השתמש בשקילויות: 
\begin_inset Formula \begin{eqnarray*}
\neg(\neg A) & \equiv & B\\
\neg(A\wedge B) & \equiv & \neg A\vee\neg B\\
\neg(A\vee B) & \equiv & \neg A\wedge\neg B\\
\neg\exists x:P(x) & \equiv & \forall x:\neg P(x)\\
\neg\forall x:P(x) & \equiv & \exists x:\neg P(x)\end{eqnarray*}

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
vspace{-1em}
\end_inset 


\layout Itemize

שנה את שמות המשתנים כך שלא יופיע אותו שם בשני כמתים.
\layout Itemize

העבר את כל הכמתים לתחילת הנוסחא תוך שמירה על סדר הופעתם.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

העברת נוסחאות לצורת 
\lang english
CNF
\lang hebrew
 - המשך
\layout Itemize

הסר את הכמתים הישיים )
\begin_inset Formula $\exists$
\end_inset 

(:
\begin_deeper 
\layout Itemize

יהי 
\begin_inset Formula $n$
\end_inset 

 מספר הכמתים הכוללים משמאל לכמת הישי.
 הנוסחא עם הכמת הישי נמצאת בטווח 
\begin_inset Formula $n$
\end_inset 

 הכמתים.
 יהיו 
\begin_inset Formula $x_{1},\ldots,x_{n}$
\end_inset 

 המשתנים של הכמתים הנ"ל.
\layout Itemize

החלף את כל ההופעות של המשתנה של הכמת הישי בפונקציה חדשה בעלת שם חדש כלשהו
 )שאינו מופיע במקום אחר( בעלת 
\begin_inset Formula $n$
\end_inset 

 ארגומנטים 
\begin_inset Formula $x_{1},\ldots,x_{n}$
\end_inset 

.
 הפונקציה נקראת 
\emph on 
פונקצית סקולם
\emph default 
 
\lang english
(Skolem function)
\lang hebrew
.
\layout Itemize

אם לא קיימים כמתים כוללים משמאל, הפונקציה תהיה בעלת 0 ארגומנטים.
 במקרה זה הפונקציה נקראת 
\emph on 
קבוע סקולם
\emph default 
.
\end_deeper 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

העברת נוסחאות לצורת 
\lang english
CNF
\lang hebrew
 - המשך
\layout Itemize

הסר את הכמתים הכוללים.
\begin_deeper 
\layout Standard

עכשיו קיימים רק כמתים כוללים.
 מסירים אותם וזוכרים שכל המשתנים הינם של כמתים כוללים.
\end_deeper 
\layout Itemize

הפוך את הנוסחא לקוניונקציה של דיסיונקטים.
 השתמש בשקילות: 
\begin_inset Formula \begin{eqnarray*}
(A\wedge B)\vee C & \equiv & (A\vee C)\wedge(B\vee C)\end{eqnarray*}

\end_inset 


\begin_inset ERT
status Collapsed

\layout Standard

\backslash 
vspace{-1em}
\end_inset 


\layout Itemize

קרא לכל דיסיוניקציה 
\lang english
clause
\lang hebrew
.
 שנה שמות משתנים כך שבכל 
\lang english
clause
\lang hebrew
 יהיו שמות אחרים.
 הסתמך על השקילות: 
\begin_inset Formula \[
\forall x:[P(x)\wedge Q(x))\equiv\forall x:(P(x))\wedge\forall x:(Q(x))\]

\end_inset 


\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

מציאת הצבה מאחדת
\layout Itemize

הצבה - אוסף של זוגות 
\begin_inset Formula $\{ x_{1}|t_{1},\ldots x_{n}|t_{n}\}$
\end_inset 

 כאשר 
\begin_inset Formula $t_{i}$
\end_inset 

 הם ביטויים ו- 
\begin_inset Formula $x_{i}$
\end_inset 

 הם משתנים ומתקיימים התנאים הבאים:
\begin_deeper 
\layout Itemize


\begin_inset Formula $\forall i\neq j:x_{i}\neq x_{j}$
\end_inset 

 
\layout Itemize


\begin_inset Formula $x_{i}$
\end_inset 

 אינו מופיע באף אחד מהביטויים 
\begin_inset Formula $t_{i},\ldots,t_{n}$
\end_inset 

.
\end_deeper 
\layout Itemize

ניתן להפעיל הצבה 
\begin_inset Formula $\sigma$
\end_inset 

 על נוסחא 
\begin_inset Formula $\alpha$
\end_inset 

 ולקבל נוסחא חדשה ע"י החלפת כל המשתנים בנוסחא המופיעים בהצבה בביטויים המתאימים.
 נסמן את הביטוי החדש ב- 
\begin_inset Formula $\alpha\sigma$
\end_inset 

.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

מציאת הצבה מאחדת - המשך
\layout Itemize

תהי 
\begin_inset Formula $\sigma$
\end_inset 

 הצבה.
 אם בהצבה 
\begin_inset Formula $\tau$
\end_inset 

 לא מופיעים משתנים המקבלים ערך בהצבה 
\begin_inset Formula $\sigma$
\end_inset 

 ניתן להגדיר את ההרכבה של 
\begin_inset Formula $\tau$
\end_inset 

 על 
\begin_inset Formula $\sigma$
\end_inset 

 )נסמן 
\begin_inset Formula $\sigma\tau$
\end_inset 

(.
\layout Itemize

תהי 
\begin_inset Formula $\sigma=\{ x_{1}|t_{1},\ldots,x_{n}|t_{n}\}$
\end_inset 

.
 תהי 
\begin_inset Formula $\tau$
\end_inset 

 הצבה כנ"ל.
 אזי: 
\begin_inset Formula \[
\sigma\tau=\{ x_{1}|t_{1}\tau,\ldots,x_{n}|t_{n}\tau\}\cup\tau\]

\end_inset 

 )כלומר מפעילים את 
\begin_inset Formula $\tau$
\end_inset 

 על הביטויים של 
\begin_inset Formula $\sigma$
\end_inset 

 ומוסיפים את הזוגות החדשים לזוגות של 
\begin_inset Formula $\tau$
\end_inset 

(.
\layout Itemize

האחדה של שני ביטויים היא הצבה ההופכת אותם לזהים.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

אלגוריתם ההאחדה של רובינזון
\layout Standard
\align right 
האלגוריתם מוצא האחדה 
\begin_inset Formula $\sigma$
\end_inset 

 בהניתן שני ליטרלים אם קיימת כזו.
\layout Standard
\align right 
קלט: שני ליטרלים 
\begin_inset Formula $L_{1}$
\end_inset 

, 
\begin_inset Formula $L_{2}$
\end_inset 

.
\layout Enumerate

אתחל 
\begin_inset Formula $L_{0}^{1}\leftarrow L_{1};L_{0}^{2}\leftarrow L_{2};k\leftarrow0;\sigma_{0}\leftarrow\emptyset$
\end_inset 

.
\layout Enumerate


\begin_inset LatexCommand \label{enu:unif-loop}

\end_inset 

אם 
\begin_inset Formula $L_{k}^{1}=L_{k}^{2}$
\end_inset 

, סיים והחזר את 
\begin_inset Formula $\sigma_{k}$
\end_inset 

.
\layout Enumerate

תהי 
\begin_inset Formula $D_{k}$
\end_inset 

 נקודת אי-הסכמה בין 
\begin_inset Formula $L_{k}^{1}$
\end_inset 

 ל- 
\begin_inset Formula $L_{k}^{2}$
\end_inset 

.
 נסמן 
\begin_inset Formula $D_{k}=\{ T_{j},v_{j}\}$
\end_inset 

, כלומר באחד הביטויים 
\begin_inset Formula $L_{k}^{1},L_{k}^{2}$
\end_inset 

 מופיע 
\begin_inset Formula $T_{j}$
\end_inset 

 ובאחר 
\begin_inset Formula $v_{j}$
\end_inset 

.
\layout Enumerate

אם 
\begin_inset Formula $v_{j}$
\end_inset 

 משתנה, 
\begin_inset Formula $T_{j}$
\end_inset 

 ביטוי ו- 
\begin_inset Formula $v_{j}\notin T_{j}$
\end_inset 

, אזי בצע:
\begin_deeper 
\layout Enumerate


\begin_inset Formula $L_{k+1}^{1}\leftarrow L_{k}^{1}\{ T_{j}|v_{j}\}$
\end_inset 

.
\layout Enumerate


\begin_inset Formula $L_{k+1}^{2}\leftarrow L_{k}^{2}\{ T_{j}|v_{j}\}$
\end_inset 

.
\layout Enumerate


\begin_inset Formula $\sigma_{k+1}\leftarrow\sigma_{k}\{ T_{j}|v_{j}\}$
\end_inset 

.
\layout Enumerate


\begin_inset Formula $k\leftarrow k+1$
\end_inset 

.
\layout Enumerate

חזור ל- 
\begin_inset LatexCommand \ref{enu:unif-loop}

\end_inset 

.
\end_deeper 
\layout Enumerate

אחרת, סיים והחזר כישלון.
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

רזולוציה עם משתנים
\layout Standard
\align right 
נתון אוסף הנחות )נוסחאות( 
\begin_inset Formula $A_{1},\ldots,A_{n}$
\end_inset 

 ומשפט 
\begin_inset Formula $T$
\end_inset 

 אותו נרצה להוכיח.
\layout Itemize

הפוך את הנוסחא 
\begin_inset Formula $A_{1}\wedge\cdots\wedge A_{n}\wedge\neg T$
\end_inset 

 לאוסף של פסוקיות 
\begin_inset Formula $\{ C_{1},\ldots,C_{m}\}$
\end_inset 

.
\layout Itemize

התחל עם אוסף פסוקיות 
\begin_inset Formula $P=\{ C_{1},\ldots,C_{m}\}$
\end_inset 

.
\layout Itemize

בצע את הלולאה הבאה:
\begin_deeper 
\layout Itemize

בחר 2 פסוקיות 
\begin_inset Formula $C_{h}=\{ L_{1},\ldots,L_{h}\},\; C_{k}=\{ D_{1},\ldots,D_{k}\}$
\end_inset 

 כך שקיימים 
\begin_inset Formula $D_{j}=\alpha,L_{j}=\neg\beta$
\end_inset 

 כאשר 
\begin_inset Formula $\alpha,\beta$
\end_inset 

 ניתנים להאחדה עם הצבה 
\begin_inset Formula $\sigma$
\end_inset 

.
\layout Itemize

תהי 
\begin_inset Formula $C_{new}=[C_{h}\cup C_{k}\setminus\{ L_{i},D_{j}\}]$
\end_inset 

.
\layout Itemize

החלף את שמות המשתנים ב- 
\begin_inset Formula $C_{new}$
\end_inset 

 לשמות חדשים שלא מופיעים ב- 
\begin_inset Formula $P$
\end_inset 

.
\layout Itemize

בצע 
\begin_inset Formula $P\leftarrow P\cup\{ C_{new}\}$
\end_inset 

.
\end_deeper 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

רזולוציה עם משתנים - המשך
\layout Itemize

תנאי העצירה:
\begin_deeper 
\layout Itemize

נמצאה סתירה - החזר "המשפט הוכח"; או
\layout Itemize

לא ניתן להמשיך - החזר "המשפט לא ניתן להוכחה"; או
\layout Itemize

המשאבים שהוקצו נצרכו - החזר "לא נמצאה הוכחה במשאבים המוקצים".
\end_deeper 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

ייצוג ידע - דוגמא
\layout Standard
\align right 
המירו את המשפטים הבאים לייצוג לוגי:
\layout Itemize


\lang english
Jack owns a dog.
\layout Itemize


\lang english
Every dog owner is an animal lover.
\layout Itemize


\lang english
No animal lover kills an animal.
\layout Itemize


\lang english
Either Jack or Curiosity killed the cat, who is named Tuna.
\layout Itemize


\lang english
Did Curiosity kill the cat?
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

ייצוג ידע - פתרון דוגמא
\layout Itemize


\lang english
Jack owns a dog.
\begin_inset Formula \[
\exists x:[\textrm{\L{Dog}}(x)\wedge\textrm{\L{Own}}(\textrm{\L{jack}},x)]\]

\end_inset 


\layout Itemize


\lang english
Every dog owner is an animal lover.
 
\begin_inset Formula \[
\forall x:[(\exists y:\textrm{\L{Dog}}(y)\wedge\textrm{\L{Own}}(x,y))\rightarrow\textrm{\L{Animal\_ lover}}(x)]\]

\end_inset 


\layout Itemize


\lang english
No animal lover kills an animal.
\begin_inset Formula \[
\neg\exists x:[\textrm{\L{Animal\_ lover}}(x)\wedge\exists y:(\textrm{\L{Animal}}(y)\wedge\textrm{\L{Kill}}(x,y))]\]

\end_inset 


\layout Itemize


\lang english
Either Jack or Curiosity killed the cat, who is named Tuna.
\begin_inset Formula \[
\textrm{\L{Cat}}(\textrm{\L{tuna}})\wedge(\textrm{\L{Kill}}(\textrm{\L{jack}},\textrm{\L{tuna}})\vee\textrm{\L{Kill}}(\textrm{\L{curiosity}},\textrm{\L{tuna}}))\]

\end_inset 


\layout Itemize


\lang english
(A cat is an animal)
\begin_inset Formula \[
\forall x:[\textrm{\L{Cat}}(x)\rightarrow\textrm{\L{Animal}}(x)]\]

\end_inset 


\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

העברה ל- 
\lang english
CNF
\layout Itemize


\lang english

\begin_inset Formula $\textrm{\L{Dog}}(\textrm{D})$
\end_inset 


\layout Itemize


\lang english

\begin_inset Formula $\textrm{\L{Own}}(\textrm{\L{jack}},\textrm{D})$
\end_inset 


\layout Itemize


\lang english

\begin_inset Formula $\neg\textrm{\L{Dog}}(y)\vee\neg\textrm{\L{Own}}(x,y)\vee\textrm{\L{Animal\_ lover}}(x)$
\end_inset 


\layout Itemize


\lang english

\begin_inset Formula $\neg\textrm{\L{Animal\_ lover}}(z)\vee\neg\textrm{\L{Animal}}(t)\vee\neg\textrm{\L{Kill}}(z,t)$
\end_inset 


\layout Itemize


\lang english

\begin_inset Formula $\textrm{\L{Cat}}(\textrm{\L{tuna}})$
\end_inset 


\layout Itemize


\lang english

\begin_inset Formula $\textrm{\L{Kill}}(\textrm{\L{jack}},\textrm{\L{tuna}})\vee\textrm{\L{Kill}}(\textrm{\L{curiosity}},\textrm{\L{tuna}}))$
\end_inset 


\layout Itemize


\lang english

\begin_inset Formula $\neg\textrm{\L{Cat}}(w)\vee\textrm{\L{Animal}}(w)$
\end_inset 


\layout Itemize

הנחת השלילה:
\lang english
 
\begin_inset Formula $\neg\textrm{\L{Kill}}(\textrm{\L{curiosity}},\textrm{\L{tuna}})$
\end_inset 

 
\end_deeper 
\layout Standard


\begin_inset ERT
status Collapsed

\layout Standard

\end_inset 


\layout LandscapeSlide

\begin_deeper 
\layout SlideHeading

אסטרטגית רזולוציה
\layout Itemize

נסתכל על תהליך הרזולוציה כעל חיפוש:
\layout Itemize

מצב - הוא אוסף פסוקיות.
\layout Itemize

מצב התחלתי - אוסף האקסיומות + שלילת המשפט בצורת 
\lang english
CNF
\lang hebrew
.
\layout Itemize

מצב סופי - כל קבוצת פסוקיות המכילה את הפסוקית הריקה.
\layout Itemize

פונקצית מעבר - כלל הרזולוציה: בהינתן מצב 
\begin_inset Formula $S$
\end_inset 

 קבוצת המצבים הבאה היא
\layout Itemize


\begin_inset Formula $\{ S\cup\{ r_{i}\}|\textrm{\R{ע"י רזלוציה} }S\textrm{ \R{מתקבלת מתוך} $r_{i}\}$}$
\end_inset 


\the_end