Необхідні поняття, факти і нотація із інших математичних дисциплін
Відношення і предикати
Коли <q; a1., am> – кінцевий стан, то
Аналгічно до класів KS-1 схем алгоритмів і ¶нтерпретацій KI-1 введемо, відпвидно, класи KS-2 і KI-2
Операторні та предикатні алгоритми -ІІ
Наслідок. Існує обчислювана функція h, для якої обидві проблеми «x Î Dom(h)» і «х Î Ran(h)» нерозв'язні
Теорема. Нехай c – довільне число. Наступні проблеми нерозв'язні
Логіка висловлень (пропозиційна логіка) [1] – одна з базових теорій математичної логіки, на якій базуються більш складні формальні логіки
Необхідно побудувати кон’юктивну нормальну форму для формули А логіки висловлень, де
Навигация
Логіка висловлень (пропозиційна логіка) [1] – одна з базових теорій математичної логіки, на якій базуються більш складні формальні логіки
Алгоритмічні проблеми
54576
знаков
5
таблиц
0
изображений
1. Логіка висловлень (пропозиційна логіка) [1] – одна з базових теорій математичної логіки, на якій базуються більш складні формальні логіки.
Алфавіт логіки висловлень (ЛВ) складається зі зчисленної множини елементарних висловлень, які позначуються літерами (можливо, з індексами) і 5 логічних операцій: заперечення (^), кон’юнкції (/\, або &), диз’юнкції (\/), імплікації (->) і тотожності, еквівалетності (<->), які задаються скінченими таблицями істинності.
Як відомо, кожне висловлення може мати значення істинно (позначається Т, 1), або хибно (позначається F, 0).
Алфавіт висловлень дає змогу будувати складні висловлення (формулу) із простіших за допомогою логічних операцій [1] по наступній рекурсивній схемі, а саме, формулами ЛВ є тільки наступні конструкції:
– кожне висловлення є формулою;
– якщо А і В є формули, то ^A, (A/\B), (A\/B), (A -> B) i (Aя2=я0B) – є формулами.
Формули задають синтаксис мови ЛВ. А який сенс, семантика цієї мови?
Вона задається за допомогою інтерпретацій. Інтерпретація – це відображення I, що зпівставляє кожному елементарному висловленню р деяке значення істинності. Інтерпретацію I, що задана на множині елементарних висловлень, природнім чином можна продовжити на множину формул за допомогою таблиць істинності. Інтерпретація, при якій істиносне значення формули А є істинно, називається моделлю цієї формули.
Літера, або літерал – це елементарне висловлення р або його заперечення ^p. Літери р і ^р є протилежні.
Формула ЛВ називається виконуваною, якщо вона допускає деяку модель, тобто її можна інтерпретувати із значенням Т.
Формула ЛВ А називається суперечністю (не виконуваною), якщо А = F для всіх моделей А (наприклад, (р/\^p).
Формула ЛВ називається тавтологією, якщо вона істина при всіх інтерпретаціях (на всіх моделях). Відмітимо, що заперечення тавтології є суперечність.
2. Нехай, Е – множина формул ЛВ. Формула А є наслідком (логічним) з Е (позначення, Е (= А), якщо на всіх моделях, на яких істині всі формули з Е, істина також формула А. Ясно, що тавтологія є наслідком із пустої множини формул ЛВ.
Легко довести [1], що мають місце:
Твердження 1. Нехай, Е = {H1, H2,… Hn} є множиною формул ЛВ.
Формула А є наслідком (логічним) з Е (E (= A) тоді і тільки тоді, коли імплікація:
(H1/\H2/\…/\Hn) -> A
є тавтологією. Прямим наслідком із твердження 1 є
Твердження 2. Нехай, Е = {H1, H2..Hn} є множиною формул ЛВ.
Формула А є наслідком (логічним) з Е тоді і тільки тоді, коли формула
(H1/\H2/\…/\Hn/\^A)
є суперечністю.
Диз’юнктом називається диз’юнкція скінченного числа літералів, тобто формула виду
(L1\/L2\/..\/Lm).
Її часто записують у «скороченому» вигляді як послідовність літералів: {L1., Lm}.Пустий диз’юнкт – єдиний диз’юнкт, що не виконується, і його позначають через Л.
Кон’юктивною нормальною формою (КНФ) називається кон’юнкція скінченої кількості диз’юнктів.
Теорема 1. Довільна формула ЛВ має логічно еквівалентну їй КНФ.
Наступний алгоритм нормалізації формул ЛВ дає доведення теореми 1.
Етап 1. Спочатку замінюємо (А<->В) на ((А->B)/\(B->A)), а потім заміняємо (U->V) на (^U\/V). Це робиться для виключення операцій <-> і ->.
Етап 2. Необхідну кількість раз застосовуються перетворення на основі законів де Моргана:
^(X/\Y) ==> (^X\/^Y), ^(X\/Y) ==> (^X/\^Y).
Символ ==> означає «замінити на». В цій заміні подвійні заперечення елімінуються, тобто
^^X ==> X.
На цій стадії операція заперечення залишається тілки безпосередньо перед висловленнями.
Етап 3. необхідну кількість разів застосовуються правила перетворень, що виведені із законів дистрибутивності:
X \/ (Y /\ Z) ==> (X \/ Y) /\ (X \/ Z)
(X /\ Y) \/ Z ==> (X \/ Z) /\ (Y \/ Z).
Етап 4. Диз’юнкти, що містять протилежні літерали (тобто висловлення і його заперечення), є тавтологіями і можуть бути еліміновані. Також елімінуються повторення літералів у межах одного ж і того диз’юнкта.
Формула, що отримується в кінці четвертого етапу, і є КНФ, яка еквівалентна вихідній формулі ЛВ.
Відмітимо, що диз’юнкт є тавтологією тоді і тільки тоді, коли він містить пару протилежних літералів. КНФ є тавтологією тоді і тільки тоді, коли всі її диз’юнкти – тавтології.
Єдиним не виконуваним диз’юнктом є пустий диз’юнкт Л.
3. Не існує загального ефективного критерію для перевірки виконуваності КНФ. Але існує зручний метод для виявлення не виконуваності множини диз’юнктів. Дійсно, множина диз’юнктів є не виконувані тоді і тілки тоді, коли пустий диз’юнкт Л є логічним наслідком із неї. Таким чином, не виконуваність множини S можна перевірити, породжуючи логічні наслідки з S, поки не отримаємо пустий диз’юнкт. Для цього використовується наступна схема міркувань.
Припустимо, що дві формули (A \/ X) i (B \/ ^X) – істині. Якщо Х також істина, то звідси випливає, що B істина. Навпаки, якщо Х хибна, то А істина, тобто отримується правило
{(A \/ X), (B \/ ^X)} [= A \/ B,
яке можна записати у вигляді
{^X -> A, X -> B} [= A \/ B. Зокрема, якщо Х – висловлення, а A i B – диз’юнкти, то правило називається правилом резолюції.
Твердження 3. Нехай s1 i s2 – диз’юнкти КНФ S. Якщо літерал р входить у s1 і ^p – у s2, то диз’юнкт
r = (s1\{p}) \/ (s2\{^p})
є логічним наслідком КНФ S.
Тут через si\{L} позначається диз’юнкт, що отримується з si вилученням літералу L. Диз’юнкт r називається резольвентою диз’юнктів s1 i s2.
Твердження 4. Нормальні форми S i (S /\ r) еквівалентні.
Доведення невиконувансті формул дуже важливо для роботи із знаннями. Воно широко використовується в логічному програмуванні. З твердження 3 і 4 випливає наступний алгоритм – метод резолюцій для доведення того, що КНФ S є суперечністю.
Метод резолюцій
Крок 1. Якщо Л належить S, то КНФ S є суперечністю, і алгоритм зупиняється.
Крок 2. Вибираються довільні L, s1, s2 такі, що літерал L входить в диз’юнкт s1, а ^L входить у s2.
Крок 3. Обчислюється резольвента r.
Крок 4. КНФ S замінюється на КНФ S' = S /\ r, і повертаються на крок 1. Вибираються довільні L, s1, s2 такі, що літерал L входить в диз’юнкт s1, а ^L входить у s2.
Твердження 5. Якщо нормальна форма S є невикнуваною формулою, тобто суперечністю, то цей факт завжди можна виявити за допомогою метода резолюцій.
Похожие работы
... число эпох функционирования алгоритма, или определение его сходимости, обычно путем сравнивания приспособленности популяции на нескольких эпохах и остановки при стабилизации этого параметра. 3. Непрерывные генетические алгоритмы. Фиксированная длина хромосомы и кодирование строк двоичным алфавитом преобладали в теории генетических алгоритмов с момента начала ее развития, когда были получены ...
... в состояние qj, заменяя содержимое ячеек соответственно символами аb1 - аbк, то после этого ленты соответственно сдвигаются в направлениях k1... kk. До сих пор принималось, что различные алгоритмы осуществляются на различных машинах Тьюринга, отличающихся набором команд, внутренним и внешним алфавитами. Однако, можно построить универсальную машину Тьюринга, способную выполнять любой алгоритм ...
... M2(n) = O(l n), C2(n) = O(l n). Оскільки l = log2n, M2(n)=O(n log2 n)), C2(n)=O(n log2 n), Але З(n) = C1(n) + C2(n), M(n) = M1(n) + M2(n). Тому що C1(n) < C2(n), M1(n) < M2(n), остаточно одержуємо оцінки складності алгоритму TreeSort за часом: M(n) = O(n log2 n), C(n) = O(n log2 n), У загальному випадку, коли n не є ступенем 2, сортуюче дерево будується трохи інакше. “Зайвий” елемент ...
... U4 сравнения двух целых чисел оставляем читателю в качестве упражнения. Замечание: исходное слово надо задать в форме * Для нормальных алгоритмов Маркова справедлив тезис, аналогичный тезису Тьюринга. Тезис Маркова: Для любой интуитивно вычислимой функции существует алгоритм, ее вычисляющий. Построение алгоритмов из алгоритмов. До сих пор, строя ту или иную МТ, или НАМ мы каждый раз ...
0 комментариев