fy"> вирішити (В, [У | Реш1]): -
після (В, В1),
вирішити (В1, Реш1).
Ця програма і є реалізація пошуку в глибину. Ми говоримо "в глибину", маючи на увазі той порядок, в якому розглядаються альтернативи в просторі станів. Завжди, коли алгоритмом пошуку в глибину належить вибрати з декількох вершин ту, в яку слід перейти для продовження пошуку, він вважає за краще саму "глибоку" з них. Найглибша вершина - це вершина, розташована далі за інших від стартової вершини. br/>
7. Семантика логіки предикатів
Стратегія визначення семантичних значень компонент і формул логіки предикатів базується на понятті інтерпретації логічного формули. Нагадаємо це поняття. p align="justify"> Об'єктами вивчення природничих і формальних мов є зокрема, синтаксис (який дозволяє розпізнавати фрази серед набору слів) і семантика (яка надає певне значення фразам). У рівній мірі це відноситься до обчислення висловлювань. p align="justify"> Вже зазначалося, що висловлювання або істинно, або хибно. Тому введемо семантичну область {І, Л}. Інтерпретувати формулу - значить приписати їй одне з двох значень істинності І чи Л.
Семантика (тобто набір правил інтерпретації формул) повинна бути композиційної: значення формули повинно бути функцією значень її складових. Точніше, значення істинності формули залежить тільки від структури цієї формули і від значень істинності складових її висловлювань. Таким чином, зв'язки числення висловів представляють функції істинності: наприклад значення істинності формули буде відомо, якщо відомі значення істинності Х і Y. Наступні дві таблиці описують семантику заперечення і бінарних зв'язок. br/>
Х Хілл
ХYX YX YX YX YІІІІІІІЛЛІЛЛЛІЛІІЛЛЛЛЛІІ
Інтерпретація - це відображення i, зіставляє кожному елементарному висловлюванню р деяке значення істинності. Інтерпретацію i, задану на множині елементарних висловлювань, можна поширити (продовжити) на безліч формул (висловлювань) за допомогою таблиць істинності. Відповідне продовження (розширення) I теж називається інтерпретацією. Інтерпретація, при якій істиннісне значення формули є І, називається моделлю цієї формули. p> Літера - це елементарне висловлювання або його заперечення. Літери р і протилежні. Інтерпретація визначає розбиття множини L літер на дві підмножини Lі і Lл, кожне з яких містить по одному елементу з кожної пари протилежних літер. p> Формули обчислення предикатів, як і формули обчислення висловлювань, можуть бути інтерпретовані, тобто можуть отримати значення істинності. Однак формули обчислення предикатів складаються не тільки з подформул, але також з термів. Отже, необхідно інтерпретувати також терми. Терм інтуїтивно означає об'єкт. Таким чином, інтерпретація повинна специфікувати безліч об'єктів, зване областю інтерпретації. p> Точніше, інтерпретація I - це трійка (D, Ic, Iv) з наступними властивостями:
В· D - непорожнє безліч, область інтерпретації.
В· Ic - функція, яка зіставляє кожної функціональної n-місній константі f деяку функцію Ic (f) з Dn в D і яка зіставляє кожній предикатной m-місцевій константі Р деяку функцію Ic (Р) з Dm в {І, Л}.
В· Iv - функція, що зіставляє кожної змінної деякий елемент із D.
Тепер можна задати для інтерпретації I = (D, Ic, Iv) такі правила, які кожній формулі А ставлять у відповідність деяке значення істинності I (A), а кожному терму t зіставляється елемент I (t) з D.
В· Якщо х - вільна змінна, то I (x) = def Iv (x).
В· Якщо f - функціональна n-місна константа, t1, ... , Tn - терми, то I (f (t1, ..., tn)) = def == (Ic (f)) (I (t1), ..., I (tn))
В· Якщо Р - предикатна m-місна константа, t1, ... , Tm - терми, то I (P (t1, ..., tm)) = def == (Ic (P)) (I (t1), ..., I (tm))
В· Якщо s і t терми, то I (s = t) є І при I (s) = I (t), а інакше Л.
В· Якщо А і В - формули, то А, (АВ), (АВ), (АВ) і (АВ) інтерпретуються як в обчисленні висловлювань.
Залишилось задати інтерпретацію для двох типів квантифікованій формул. Введемо спочатку одне поняття. Якщо I - інтерпретація c областю DI, x - змінна, d - елемент з DI, то Ix/d означає таку інтерпретацію J, що DJ = DI, Jc = Ic, Jv (x) = d і Jv (y) = Iv ( y) для всіх вільних змінних у відмінних від х.
