14. Логічне слідування на базі алгебри висловлень.

Розглянемо кілька схем логічного слідування правила виводу:

1. Першим іде правило, яке називається правилом МТ (modes popens) і має вигляд ; над рискою записують посилки , під рискою висновок, це саме правило зустрічається під назвою ( правило висновку , правило відокремлення).

2. П равило МТ (modus tollens) мають вигляд .

Перша посилка має вигляд: якщо 22 кратне 8, то 22 кратне 4.

Друге 22 некратне 4 , 22 некратне 8.

3. Правило контрпозиції : ;

4. Правило вилучення кон’юнкції :

5. Правило введення кон’юнкції: ;

6. Правило введення диз’юнкції : ;

7. Правило вилучення диз’юнкції : ;

8. Правило силуїзму: ;

15. Методи перевірки тотожної істинності формул числення висловлювань.

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

• Аксіоматичний метод (базується на використанні аксіом та мета символів);

• Конструктивний метод ( оснований на використанні таблиць істинності );

• Метод резолюції ( оснований на перетворенні диз’юнктів та скороченні термів ).

Кожен з них здійснюється за певними правилами та за різним алгоритмом.

16. Аксіоматичний метод доведення в логіці висловлень.

Аксіоматичний метод побудови доведення полягає в тому, щоб на основі незалежних системах аксіом довести справедливість довільної «Клаузи».

Клауза – це формальний запис речення, яке необхідно довести, якщо замість букв в ній підставити об’єктивні висловлення вона наповнюється конкретним змістом і називається легендою.

Окремі ланцюги доведення звязанні символом імплікації(→) проте при доведенні використовують символ => - мета символ або суб’єктивним або → об’єктивним символом.

Аналогічно замість об’єктивної кон’юнкції використовують об’єктивний символ «,» , замість об’єктивної диз’юнкції використовують «;».

Клауза – це мета речення , в якому використовується відношення порядку через символ мета імплікації w.

Доведення будується на основі відношення порядку, тобто закони, комутативності, дистрибутивності, «0» та «1» стають аксіомами.

17. Конструктивний метод доведення в логіці висловлень.

Конструктивний метод бере за основу використання таблиць істинності. Клауза Р₁, Р₂, Р₃, Р₄, …, Р_n → А, вважається істиною , якщо всі 1 наслідку покривають всі одиниці узагальненої причини.

18. Метод резолюції доведення в логіці висловлень.

Метод революції відноситься до напівконструктивного методу. Суть цього методу полягає в тому , що два посилкові диз’юнкти з протилежними термами завжди можна скласти в один загальний диз’юнкт в якому відсутні протилежні терми. При послідовному застосуванні послідовної резолюції зменшується число букв , деякі повністю знищуються, а вихідна клауза будується у формі кон’юктивного протиріччя.

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

Метод резолюції є формальним методом.