(Z 10 ) 22. Перевірити чи всі висказивательную змінні незв'язних і різні.
Якщо так, то перейти до п. 23 інакше до п. 21.
(V 13 ) 23. Вивести рішення. Теорема не доказова і припущення не вірно.
(V До ) Кінець
4. Змістовний словесний алгоритм і граф - схема алгоритму доведення методом пропозіціональной резолюції (до п. 3)
(Vn) Початок
(V1) 1. Вводимо формули посилок і теореми
(Z1) 2. Перевіряємо всі формули на наявності еквіваленціі, якщо є еквіваленція, то переходимо до п. 3, інакше - до п. 4.
(V2) 3. Замінюємо еквіваленцію за формулою:
(Z2) 4. Перевіряємо всі формули на наявності імплікації, якщо є імплікація, то переходимо до п. 5, інакше - до п. 6
(V3) 5. Замінюємо імплікації диз'юнкцій за формулою:
В
(Z3) 6. Перевіряємо всі формули на наявність загальної інверсії, якщо є загальна інверсія, то переходимо до п. 7, інакше - до п. 8
(V4) 7. Застосовуємо правило де Моргана:,
(Z4) 8. Перевіряємо всі формули на наявність дистрибутивности, якщо є дистрибутивность, то переходимо до п. V5, інакше до п. V6
(V5) 9. Застосовуємо дистрибутивний закон:
,
(V6) 10. Отриману перетворену формулу теореми інвертуємо. p align="justify"> (V7) 11. Всі отримані пропозиції (диз'юнктів) поміщаються в єдину групу з n елементів
(V8) 12. Відбираємо з групи (отримана вище) за черговістю, від 1 до n, одна пропозиція (s1), яке раніше не брали
(Z5) 13. Якщо в групі немає пропозицій (s1), які раніше не бралися, то теорема спростовується, і переходимо до п. Vk. Інакше до п. V9
(V9) 14. Відбираємо з групи друге речення (s2), таке що воно не є s1, і які раніше не бралося (після останнього відбору пропозиції s1)
(Z6) 15. Якщо в групі немає пропозиції (s2) які раніше не бралися, то переходимо до пункту V8. Інакше до п. Z7
(Z7) 16. Якщо в одному з двох пропозицій існує така мінлива, що в іншому реченні існує змінна, то переходимо до п.V10. Інакше до п.V9. p> (V10) 17. З цих двох пропозицій будується нова пропозиція (s3), що складається із сполучених зв'язкою І елементів двох відібраних пропозицій, причому включаються всі елементи, крім і. Пропозиція s1 замінюється отриманою пропозицією (s3). p> (Z8) 18. Якщо в результаті злиття отримали пусте пропозицію, то ми отримали протиріччя, отже теорема доведена і переходимо до п. Vk. Інакше до п. V11
(V11) 19. Новоствор...
