Обчислення висловлювань Перевірка виводимості правильних висновків. Алгоритм Квайна. Правило резолюцій. Алгоритм Вонга.
I Формальні системи (ФС)
З - алфавіт спеціальних розділових знаків
ППФ - правильно побудовані формули з імен та знаків
А Î ППФ - формули, які називаються аксіомами
ПВ - правила виведення на безлічі ППФ виду «якщо, то»
Обчислення, таке що I конструктивно породжується з безлічі аксіом застосуванням ПВ.
Приклад 1. Формальні граматики. , Де A - термінальний алфавіт; V - допоміжний алфавіт; Р - правила виведення, виду, де (всі слова з об'єднаного алфавіту); S - початковий допоміжний символ (початок породження) суть аксіома.
Граматика G породжує (обчислює) мова, яка є множиною слів, виділених для цілей синтаксичного опису моделей деяких об'єктів (наприклад, мови програмування ALGOL).
II. Формальна модель висловлювань (мова висловлювань)
A - алфавіт імен =. Z - алфавіт знаків = ®, , ù, V. Å, º, інші знаки логічних операцій, - дужки>. ППФ суть дужкові формули з A і Z. побудовані за певними правилами, наприклад - є ППФ, а формула не є ППФ. Літерами A, B, C і т. Д. Позначаються складні ППФ.
1) Кожне суть атомарному висловлювання. Наприклад, р - «студент спить», q - «слони живуть в Африці»
2) Кожне ППФ утворює складне висловлювання, де знаком надається сенс логічних зв'язок між висловлюваннями.
- сенс: А чи В. але не обидва разом (розділене або).
- сенс: А тотожне (еквівалентно) У.
ù - сенс: чи не А. інше позначення -
Приклад: р - студент спить, q - час йде, r - лекція нудна.
Студент спить, а час йде
Студент спить, якщо лекція нудна -.
5.Інтерпретація ППФ.
1) Кожному атомарному висловом приписується значення.
2) Кожній ППФ приписується значення в залежності від інтерпретації зв'язок як знаків операцій. Інтерпретація зв'язок відповідає таблицями істинності ФАЛ.
3) Якщо при деякій інтерпретації ППФ істинна, то вона називається здійсненним на даній інтерпретації.
4) Якщо ППФ здійсненна (істинна) на всіх наборах, то вона називається тотожно істинною. або тавтологією. або загальнозначущої.
Інші інтерпретації ППФ.
а) Багатозначні логіки. Наприклад, кожне атомарному висловлювання з ППФ і сама ППФ отримують значення з безлічі - тризначна логіка.
б) Правдоподібна логіка. Введена Д. Пойа в книзі «Математика і правдоподібні міркування». ППФ приймають значення з безлічі і інтерпретується як міра правдоподібності висловлювання. Д. Пойа ввів правила для обчислення правдоподібності складених висловлювань по правдоподібності його складових.
III. Спеціальний вид висловлювань - міркування або
Міркування складається з двох висловлювань «p» і «S». р - висловлювання - посилка, S - висловлювання - наслідок, формальна запис міркування - читається «з р слід S», або «якщо Р то S» .Іноді висловлювання S ще називають висновком.
Якими властивостями наділяються правильні міркування? Cлід враховувати наведені відносини:
а) якщо Р = «істина», то і S повинна бути = «істина».
б) якщо Р = «брехня», то з «брехні» може слідувати все, що завгодно, т. е. висновок S може бути і помилковим і істинним.
в) з істинною посилки не повинно слідувати неправдивий висновок.
Всі ці відносини визначають правильні або справжні міркування, як це показано в таблиці нижче.
Можна ввести таку інтерпретацію правильного міркування: Якщо правильне, то і.
Правильно побудоване міркування є тавтологією. У правильному міркуванні не може бути, щоб посилка була справжньою, а висновок помилковим. Цей рядок в таблиці істинності правильного міркування відсутня. Якщо є тавтологією, то кажуть, що міркування побудовано відповідно до логіки і є логічним законом. який не залежить від інтерпретації, а визначається тільки структурою (ППФ) посилок і наслідків.
IV.Логіческіе закони (Арісто-322 д. Н.е.).
Вперше в явному вигляді логічні закони, за допомогою яких можна будувати правильні міркування були сформовані Аристотелем. Дивно, що теорія правильних міркувань, яка називалася силлогистикой і метод виведення правильних висновків з посилок - дедукція були сформовані понад 2 тисячі років тому, ніким не спростовані і вважаються притаманними людському мисленню.
Нагадаємо, що всі логічні закони повинні бути тавтологія. Іноді закони називаються правилами виведення, які визначають правильний висновок з посилок.
1) Modus ponens (правило відділення); сенс: якщо вірно, що з А слід В і А є істинним, то істинно В.
Формальна запис висловлювання (умовиводи, міркування) у вигляді формули. Перевірка правильності міркування проводиться по таблиці істинності.
Перевірка тавтології за допомогою еквівалентних перетворень.
Приклад: Якщо лекція нудна, то студент спить. Лекція нудна.
2) Modus tollens (негативний Марус)
3) Правило силогізму;
4) Закон контрпозиції
5) Всі співвідношення (тотожності) алгебри логіки суть тавтології і тому є логічними законами.
6) Закон виключення третього.
7) Закон дистрибутивности і.
8) Закон «згубна дилема»
Може бути доведена наступна теорема.
Будь-яка формула, яка є тавтологією, може бути приведена до вигляду і оголошена логічним законом.
Наприклад, - є тавтологія, т. К. Позначивши
Для подання F в формі введемо
V.Ісчісленіе висловлювань.
Найбільший інтерес представляє побудова формальної системи, яка серед всіх можливих ППФ висловлювань виділяє такі, які є логічними законами (правильно побудованими міркуваннями, логічними висновками, тавтологія, загальнозначущими висловлюваннями).
Формальна система, яка породжує висловлювання, які є тавтологія і тільки їх, називаються обчисленням висловлювань (ІВ). Вище було показано, що будь-яка формула висловлювань (в тому числі і тавтологія) може бути приведена до структури міркування (умовиводи), «якщо Р. то S».
Формули в ІВ вважаються виведеними з аксіом. У кожному виведенні з тавтологію виводяться тавтології. позначення: # 8870; ; інтерпретація: з виводиться.
Формальна система ІВ визначається:
Формули - аксіоми є тавтологія. Правила виведення у вигляді також є тавтологія.
На сьогоднішній час відомо »20 ІВ, які відрізняються один від одного аксіомами (схемами аксіом) і правилами висновків. Всі ІВ мають 1) властивість повноти - (в них виведені всі тавтології і тільки вони) 2) набір аксіом має мінімальну повнотою (т. Е. Видалення хоча б однієї аксіоми з набору робить ІВ неповної).
1) ІВ Уйтхеда і Рассела (1920¸1930 Англія).
Правила виведення Р1: Підстановка А замість В; Р2: Заміна на еквівалентну формулу Р3: Modus ponens # 8870; В.
2) ІВ Никодим (1952, США)
Єдина аксіома з операцією штрих Шеффера:
єдине ПВ: # 8870; С.
VI. Методи і алгоритми перевірки виводимості.
Нехай задана сукупність ППФ, яка називається посилками (іноді гіпотезами), і ППФ -. «» Називається логічним наслідком. або виведеної з А (записується як # 8870; ), Якщо є тавтологією (тотожне істинним висловлюванням).
Таким чином, завдання перевірки виводимості зводиться до перевірки на тотожну істинність. Існує кілька десятків методів і алгоритмів встановлення тотожною істинності логічної формули.
АІТ зводиться до послідовної підстановці всіх можливих інтерпретацій (наборів «істина» і «брехня») змінних, що входять в. Алгоритм зупиняється, якщо значення брехня (нездійсненна, а значить не виводиться з на всіх інтерпретаціях); істина (здійсненна на всіх інтерпретаціях, значить суть тавтологія і А # 8870;. Такий алгоритм вимагає в найгіршому випадку 2n підстановок (2n можливих інтерпретацій), де «n» число змінних, що входять в формулу F.
2. Алгоритм Квайна (Квайну. 1960 р США)
Ідея: при послідовних підстановках значень змінних можна зменшити довжину формули, виходячи з сукупності проведених перевірок істинності F. і тим самим скорочувати число змінних для перевірки.
Вводиться поняття дерева випробувань, яке по суті справи представляє собою граф всіх інтерпретацій перевіряється формули. Квайну назвав його «семантичним деревом».
Приклад: Нехай необхідно перевірити общезначімость формули
Семантичне дерево. Кожне ліве ребро дерева відповідає змінним, а кожне праве ребро -.
Кожна гілка (наприклад, найлівіша) відповідає набору (p × q × r), найправіша. Дерево перераховує всі можливі елементарні кон'юнкції.
1) Покладемо для F (вершина), тоді
(Формула в вершині «1»)
2) Покладемо для, тоді
(Формула в вершині «2»)