Основні схеми логічно правильних міркувань.

Принцип дедукції

III. ОСНОВИ ТЕОРІЇ ОБЧИСЛЮВАЛЬНОСТІ

Кажуть, що формула В логічно випливає з формули А, якщо формула В має значення І при всіх інтерпретаціях, при яких формула А має значення І. Кажуть, що формули А і В логічно еквівалентні (позначається А? B або просто А = В), якщо вони є логічним наслідком один одного. Логічно еквівалентні формули мають однакові значення істинності при будь-якій інтерпретації.

Найбільш короткий і простий спосіб виведення заснований на теоремі дедукції.

Поряд з алфавітом і правилами побудови складних висловлювань - логічних формул, мови логіки висловлювань містять правила прео рення логічних формул. В алгебрі логіки - це еквівалентні співвідношення, а також правило підстановки і правило заміни; в обчисленні висловлювань - це загальні логічні аксіоми і правила підстановки і висновку, звані правилами виведення. Правила перетворення реалізують загальні логічні закони і забезпечують логічно правильні міркування. Коректність допустимих в логіці перетворень є фундаментальним властивістю формальної (математичної) логіки.

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

Процес отримання нових знань, виражених висловлюваннями, з інших знань, також виражених висловлюваннями, називається міркуванням (умовиводом). Вихідні висловлювання називаються посилками (гіпотезами, умовами), а одержувані висловлювання - ув'язненням (наслідком).

Наведемо приклади найбільш уживаних схем логічно правильних міркувань:

1. Правило висновку - стверджує модус (Modus Ponens):

"Якщо з вислову А слід вислів В і справедливо (істинно) висловлювання А, то справедливо В" (Спосіб спуску). Позначається:

.

2. Правило заперечення - негативний модус (Modus Tollens):

"Якщо з А випливає В, але вислів У невірно, то невірно А "(Доказ від протилежного). Позначається:

.

3. Правила твердження-заперечення (Modus Ponendo-Tollens):

"Якщо справедливо чи висловлювання А, або висловлювання В (в розділовому значенні) і істинно одне з них, то інше брехливо" (розділовий силогізм). Позначається:

; .

4. Правила заперечення-ствердження (Modus Tollen-Ponens):

а) "Якщо істинно або А або В (в розділовому значенні) і невірно одне з них, то істинне інше":

; .

б) "Якщо істинно А або В (в неразделітельном сенсі) і невірно одне з них, то істинно інше "(діз'юнктівную силогізм). Позначається:

; .

5. Правило транзитивності (спрощене правило силогізму):

"Якщо з А випливає В, а з В слід С, то з А випливає С" (гіпотетичний силогізм). Позначається:

.

6. Закон суперечності:

"Якщо з А випливає В і В, то невірно А":

.

7. Правило контрапозиции:

"Якщо з А випливає В, то з того, що невірно В, випливає, що невірно А":

.

8. Правило складної контрапозиции:

"Якщо з А і В слід С, то з А і С слід В":

.

9. Правило перетину:

"Якщо з А випливає В, а з В і С слід D, то з А і С слід D":

.

Наведемо без пояснень ще кілька правил умовиводів.

10. Правило імпортаціі (об'єднання посилок):

.

11. Правило експортаціі (роз'єднання посилок):

.

12. Правила дилем:

а) (Проста конструктивна дилема);

б) (Складна конструктивна дилема);

в) (Проста деструктивна дилема);

г) (Складна деструктивна дилема).

Примітка. Для побудови логічних формул, що відображають зазначені вище логічно правильні міркування, слід все посилки з'єднати зв'язкою "І" (&) і отриману таким чином узагальнену посилку - зв'язкою "якщо ..., то ..." (?). Наприклад, правило ув'язнення (Modus Ponens) має бути представлено логічною формулою:

.

Прикладами міркувань, які не є правильними, можуть служити:

а)

б)

в) та ін

Для того щоб перевірити, чи є даний умовивід логічно правильним, слід відновити схему міркування і визначити, чи відноситься вона до схем логічно правильних міркувань. Однак така перевірка ускладнюється тим, що схем логічно правильних міркувань нескінченна безліч. Для перевірки правильності міркувань може бути використаний метод докази від протилежного (закон протиріччя - правило 6).

Метод резолюцій в численні висловів.
Метод резолюції є одним з методів доказу від супротивного. Метод, запропонований Дж. Робінсоном, в даний час є теоретичною базою більшості методів доказу. Хоча загальноприйняті правила виводу, наприклад, правило modus ponens, дозволяють людині простежити за кожним кроком процедури докази, існує більш сильний правило резолюцій, яке важко піддається сприйняттю, але ефективно реалізується на комп'ютері.

В даний час не існує ефективних критеріїв перевірки виконуваності КНФ. Метод резолюцій дозволяє виявити нездійсненність безлічі диз'юнктів.