Повна версія

Головна arrow Природознавство arrow ІНТЕЛЕКТУАЛЬНІ СИСТЕМИ

  • Увеличить шрифт
  • Уменьшить шрифт


<<   ЗМІСТ   >>

АЛГОРИТМИ РОЗПІЗНАВАННЯ ОБЩЕЗНАЧИМОСТИ ФОРМУЛ ЛОГІКИ ВИСЛОВЛЮВАНЬ

У разі логіки висловлювань перевірка общезначимости формули, яка має п змінних, може бути здійснена шляхом перебору всіх 2 П можливих наборів логічних констант, що зіставляються цим змінним при різних інтерпретаціях, і встановленні того, що всі значення формули на цих наборах рівні І. Таким чином тут є не тільки алгоритм перерахування всіх загальнозначущих формул, а й алгоритм перевірки общезначимости. Однак навіть для такого найпростішого випадку залишається проблема зменшення трудомісткості розпізнавання общезначимости в порівнянні з практично мало прийнятним для скільки-небудь значних п перебором всіх 2 Пнаборів значень змінних. До проблеми розпізнавання общезначимости формул логіки висловлювань тісно примикає проблема рішення систем логічних рівнянь зводиться до знаходження всіх наборів значень змінних при яких задана формула алгебри логіки приймає значення І. Остання проблема часто зустрічається в різних прикладних задачах дискретної оптимізації та діагностики, і пошуку ефективних процедур вирішення її , що враховують в своїх евристичних вирішальних правилах статистичні особливості розглянутого класу задач, присвячене велика кількість забезпечує ство досліджень. Ми обмежимося тут лише декількома найпростішими процедурами подібного роду (стосовно до задачі розпізнавання общезначимости), оскільки вони дозволять нам розвинути техніку доведення теорем в логіці висловлювань, що представляє собою спрощений аналог техніки, розвивається далі для автоматичного доведення теорем в логіці предикатів.

Перш за все, опишемо алгоритм Квайна , який здійснює перевірку общезначимости формули / логіки висловлювань за допомогою побудови так званого семантичного дерева. Корню цього дерева - вихідної вершині - приписується формула /. Нехай вже побудовано деяку підмножину вершин семантичного дерева, кожної з яких порівняна деяка формула. Якщо кожної кінцевий вершині даного дерева виявилася сопоставлена константа І, то процес завершується, і формула / є загальнозначущої. Якщо деякої кінцевої вершині дерева сопоставлена константа Л, то формула / НЕ общезначима, і процес буде теж завершено. В іншому випадку знайдеться кінцева вершина г>, якою зіставлено формула відмінна від констант І, Л. Якщо ця формула д не містить змінних, то її можна перетворити в логічну константу, використовуючи тотожності:

Якщо ж вона містить хоча б одну змінну х, і виконуються наступні дії:

  • а) Знаходяться результати д і д ^ підстановки в формулу д замість змінної х, відповідно констант І і Л.
  • б) Знаходяться результати д і д ' 2 спрощення формул д і <72 за допомогою перерахованих вище тотожностей, що застосовуються до тих пір поки це можливо.
  • в) вводяться дві нові вершини Vi і v 2 семантичного дерева, яким приписуються, відповідно, формули д і д 2 . До цих вершин від вершини v проводяться ребра, відмічені відповідно виразами х = І і х = Л.

Далі повторюється описаний вище процес розгляду кінцевих вершин семантичного дерева.

У даній процедурі залишився недовизначених вибір конкретної змінної х формули д , по якій проводиться "розбір випадків". Цей вибір в прикладних програмах, які вирішують системи логічних рівнянь шляхом побудови семантичних дерев, здійснюється на підставі різних евристичних вирішальних правил. Найпростішим таким правилом є вибір змінної, що має найбільше число входжень в <7, для отримання найбільш сильного спрощення при переході до д [ і д 2 , іншим корисним міркуванням є такий вибір змінних х, при якому зіставлені кінцевим вершин семантичного дерева формули д виявлялися б представимо , наприклад, як hi & ch 2 або hi V / 12, де формули h і h 2 не мають загальних змінних. У цьому випадку замість

: Алгоритм Квайна

Мал. 3.1 : Алгоритм Квайна.

побудови гілки дерева для Л1 & Л2 (Л1 V Л2, h -> / 12 і т.п.) можна було б розглянути незалежно формуються дерева для Ль Л 2 і з аналізу їх кінцевих вершин зробити висновок щодо общезначимости д.

Приклад. Як приклад застосування алгоритму Квайна переконаємося в общезначимости формули, отриманої зі схеми аксіом А2:

Дерево розбору випадків для цієї формули наведено на рісун-

ке 3.1.

У прикладних ситуаціях логічні мови рідко використовуються у всьому різноманітті своїх синтаксичних можливостей. Зазвичай їх формули наводяться еквівалентними перетвореннями до того чи іншого "стандартного вигляду", який і зберігається в процесі обробки інформації. З точки зору логіки висловлювань, найбільш типовою логічної стандартною формою, що відбиває тенденцію до опису ситуацій у вигляді кон'юнкції умов, є кон'юнктивна нормальна форма. Формула, представлена, в цій формі, має вигляд Ai & ... & A n , n> 1, де кожне = - формула

виду а V • • • V де mi> 1, причому (вц, ..., B im j -

змінні або заперечення змінних.

Більш точно, для визначення кон'юнктівной нормальної форми введемо спочатку поняття диз'юнкт. Якщо хь ..., x m - різні змінні, т> 1, то формулу виду (x ° l V • • • VxJ? ") Назвемо диз'юнкт. Логічний константу Л за визначенням так само вважаємо диз'юнкт.

Якщо Ль ..., А п - різні диз'юнкт (n> 1), то формула (Л1 & ... & Л П ) називається кон'юнктівной нормальною формою.

Довільну формулу логіки висловлювань можна перетворити до вигляду кон'юнктівной нормальної форми, використовуючи такі еквівалентні перетворення:

а) логічні зв'язки - ?, «-> усуваються за допомогою тотожностей

б) заперечення у формулі '' опускаються до змінних "за допомогою тотожностей

в) застосовуються перетворення дистрибутивности:

г) усуваються повторні входження змінних в диз'юнктивних подформулах, а також константи І, Л (якщо сама формула не є І чи Л):

д) усуваються однакові диз'юнкт: а & а = а.

У процедурах автоматичного доведення теорем часто застосовується метод докази "від протилежного". В цьому випадку для доказу общезначимости формули / переходять до розгляду формули - * / і намагаються довести її нездійсненність.

Наведемо модифікований алгоритм Квайна, призначений для встановлення нездійсненності формули логіки висловлювань д ) перетвореної до виду кон'юнктівной нормальної форми. Вершин семантичного дерева в цьому випадку будуть зіставлятися не формулою, а їх безлічі диз'юнктів.

Спочатку вводимо корінь семантичного дерева і зіставляємо йому безліч диз'юнктів формули д.

Нехай вже побудована частина семантичного дерева.

Якщо кінцевий вершині дерева порівнювати порожня множина диз'юнктів (порожня множина відповідає логічній константі І), то формула д - здійсненна, і алгоритм припиняє роботу.

Якщо кожної кінцевий вершині семантичного дерева відповідає безліч диз'юнктів, що містить диз'юнкт Л, то формула д - нездійсненна, і алгоритм припиняє роботу.

Якщо деякої кінцевої вершині v порівнювати непорожня множина диз'юнктів S, що не містить диз'юнкт Л, то в S входять диз'юнкт зі змінними. Вибираємо одну з таких змінних х і розбиваємо S на три підкласу: S - все диз'юнкт, в які х входить без зовнішнього заперечення, 5г - все диз'юнкт, в які х входить з запереченням, S3 - все диз'юнкт в яких х не зустрічається. Далі розглядаємо безліч диз'юнктів S x = {dd V - "х € S2} (якщо -> х € S2, то тут береться d = Л) і безліч диз'юнктів і безліч диз'юнктів S-, z = {dd V х G Si} ( якщо х? Si, то тут береться d = Л). Неважко бачити, що нездійсненність кон'юнкції диз'юнктів списку S еквівалента одночасної нездійсненності кон'юнкція диз'юнктів списків S x U S3 і S-, x U S3. Тому для продовження побудови семантичного дерева вводимо дві нових вершини v і V 2 , яким зіставляємо, відповідно, безлічі диз'юнктів S z uS3 і 5, z US3, причому проводимо до Vi і г> 2 ребра від v, відмічені відповідно виразами х = І і х = Л.

Далі повторюється описаний вище процес розгляду кінцевих вершин семантичного дерева.

Приклад. Як приклад застосування модифікованого алгоритму Квайна звернемося знову до формули /, заданої виразом (3.1). Після усунення логічних зв'язок - "ми отримаємо формулу

Далі переходимо до розгляду формули яка має вигляд:

: Модифікований алгоритм Квайна. Семантичне дерево для формули -> д наведено на рісун-

Мал. 3.2: Модифікований алгоритм Квайна. Семантичне дерево для формули -> д наведено на рісун-

ке 3.2.

Інший алгоритм розпізнавання нездійсненності кон'юнктівной нормальної форми пов'язаний з розглядом спеціальної дедуктивної системи, що використовує в якості правила виведення так зване правило резолюції. В цьому випадку кон'юнктивна нормальна форма знову представляється як безліч своїх диз'юнктів, ці диз'юнкт і утворюють перелік аксіом даної дедуктивної системи. Правило резолюції будучи застосовано до двох диз'юнкт АУ В і -> А У З створює в якості слідства новий диз'юнкт В У З (тут можливі вироджені випадки відсутності В або С , якщо вони обидва відсутні, то результатом служить диз'юнкт Л). Достатність застосування даного правила виведення для розпізнавання нездійсненності гарантується наступним затвердженням. Теорема 20. Кон'юнкція кінцевого сімейства диз'юнктів S нездійсненна тоді і тільки тоді, коли за кінцеве застосувань правила резолюції з S виводиться диз'юнкт Л.

Доведення. Доводити будемо індукцією по числу п змінних, що зустрічаються в диз'юнкт з 5.

Базис індукції. Якщо п = 0, то твердження очевидно, так як в цьому випадку непорожнє сімейство диз'юнктів може містити тільки логічну константу Л.

Індуктивний перехід. Нехай твердження вже доведено

для деякого п.

Розглянемо сімейство S з n + 1 змінної: х , Х 2 , ..., x n + i • Розіб'ємо S на три підкласу: Si - все диз'юнкт представимо у вигляді x n + i V а, - все диз'юнкт представимо у вигляді -чх п +1 V 6, S3 - диз'юнкт що не містять x n + i *

диз'юнкт безлічі

отримані з диз'юнктів сімейства S застосуванням правила резолюції (тут допускаються вироджені випадки, коли а або b відсутня, причому при одночасній відсутності а й Ь в Я включається константа Л).

Розглянемо сімейство диз'юнктів Я U S3 і покажемо, що його нездійсненність еквівалентна нездійсненності S. Якщо S здійснимо, то інтерпретація, що обертає в І диз'юнкт з S дає значення І і для всіх диз'юнктів з R U S3, тобто R US 3 здійснимо. Нехай S нездійсненно, розглянемо набір істиннісних значень оч, ..., а п змінних xi f ., ~, Z n і покажемо, що на цьому наборі хоча б один з диз'юнктів сімейства R U 5з має значення Л. Так як S нездійсненно, то на наборі а ь ..., а п , і значень змінних Xi, ..., x n , x n + 1 деякий диз'юнкт d з S має значення Л. Якщо d € S3, то він і є шуканим диз'юнкт в Я U S3. Так як x n + i має значення І, то при d ? S3 залишається єдина можливість d € S2, тобто d = " , x n + i V 6. Аналогічно на наборі оч, ..., а", Л значень змінних х % ..., x n , x "+ i деякий диз'юнкт в! з S має значення Л. Знову, якщо d ' 6 S3, то він і є шуканий, а в іншому випадку (так як x n + i має значення Л) необхідно d' ^ Siy тобто d '= x n + i Va. Диз'юнкт а і 6 не містять змінної x n + i, і тому обидва приймають значення Л, якщо змінні xi, ..., х п мають значення ац, ..., a n . Отже і диз'юнкт d " = aV &, що належить Я, матиме на наборі оч, ..., а" значень змінних xi, ..., х п значення Л. Це і означає доказ еквівалентності нездійсненності S і Я U S3.

Але число змінних в RL) S $ не більше п, тобто для нього має місце еквівалентність нездійсненності і існування виведення константи Л.

Якщо константа Л виведена з S, то або диз'юнкт Л належить S, і тоді S - неможливо, або константа Л виведена з Я U S3, тоді Л U S3 - неможливо і, отже, S - неможливо.

Якщо S нездійсненно, то неможливо Лі S3 і з Лі S3, а, значить, і з S виведена константа Л.

Тим самим теорема доведена. ?

Приклад. Як приклад застосування правила резолюції звернемося знову до формули -> д } заданої виразом (3.2). Початкове безліч диз'юнктів має вигляд

З (-> xi V Х 2 ) і х за правилом резолюції виводиться х 2. З (-ЧГ1 V -ЧГ2 V Хз) і Х ВИВОДИМО -1X2 V Х3. З ( "» Х2 V Х3) І ХГ виводимо Х3. І нарешті, з хз і - »хз отримуємо Л. Отже, формула -уд нездійсненна.

вправи

3.1. Які з наступних виразів є правильними виразами (формулами) логіки висловлювань:

  • 3.2. Розставте дужки в таких висловлюваннях (з урахуванням пріоритету операцій &, V, - ?, «- + і лівої асоціативності всіх двомісних операцій), так щоб вийшли правильні вирази логіки висловлювань:
  • 3.3. Які з наступних формул логіки висловлювань загальнозначимі, а які - здійснимі:

3.4. Побудувати таблицю істинності для наступних формул логіки висловлювань:

  • 3.5. Для кожної здійсненним формули з вправ 3.3 і 3.4 знайти хоча б одну її модель.
  • 3.6. Для кожної формули з вправ 3.3 і 3.4 перевірити чи є вона здійсненним, нездійсненним, загальнозначущої за допомогою методу Квайна, модифікованого методу Квайна і методу резолюції.
  • 3.7. Доведіть еквівалентність наступних формул логіки висловлювань:

3.8. Доведіть леми 11, 12 і 13.

3.9. Нехай f, g t h - формули логіки висловлювань. Доведіть справедливість наступних тверджень:

 
<<   ЗМІСТ   >>