п. 1)
(V H ) Початок
(V 1 ) 1. Ввести формули посилок і теорему
(Z 1 ) 2. Перевірити формули посилок і теорему на наявність знаку еквіваленціі, якщо є, то перейти до п. 3, інакше до п. 4.
(V2) 3. Замінити формулу A В«B на
(Z2) 4. Перевірити формули посилок і теорему на наявність знаку імплікації, якщо є, то перейти до п. 5, інакше до п. 6. p> (V3) 5. Замінити формулу A В® B на
(Z3) 6. Перевірити формули посилок і теорему на наявність загального заперечення, що зв'язує дві або більше букв, якщо є, то перейти до п. 7, інакше до п. 8. p> (V4) 7. Замінити на і на. p> (Z4) 8. Перевірити формули посилок і теорему на наявність подвійного заперечення, якщо є, то перейти до п. 9, інакше до п. 10. p> (V5) 9. Замінити на. p> (Z5) 10. Перевірити формули посилок і теорему на наявність дистрибутивности Гљ щодо Г™, якщо є, то перейти до п. 11, інакше до п. 12. p> (V6) 11. Замінити формули на. p> (V7) 12. Виписати формули посилок ліворуч від стрілки, теорему праворуч. p> (V8) 13. Замінити Г™ ліворуч та Гљ праворуч на кому. p> (Z6) 14. Перевірити чи є однакові і незв'язані висказивательную змінні без заперечення, або з запереченням, ліворуч або праворуч від стрілки, якщо є, то перейти до п. 15, інакше до п. 16. p align="justify"> (V 9 ) 15. Всі однакові змінні ліворуч і праворуч від стрілки викреслити.
(Z 7 ) 16. Перевірити чи є дві однакові і незв'язані висказивательную змінні без заперечення, або з запереченням, ліворуч або праворуч від стрілки, якщо є, то перейти до п. 17, інакше до п. 18.
(V 10 ) 17. Висказивательную змінну з запереченням перенести ліворуч на права або справа на ліво від стрілки з винятком знака заперечення. Помітити що цей рядок закрита (доведена).
(Z 8 ) 18. Перевірити чи всі формули посилок розкриті, якщо ні, то перейти до п. 19, інакше до п. 20.
(Z 9 ) 19. Перевірити чи всі змінні незв'язних, і одна змінна ліворуч і праворуч від стрілки в однаковій формі, якщо так то перейти до п. 20, інакше до п. 21.
(V 11 ) 20. Видати рішення. Теорема доведена.
(V 12 ) 21. Розбити i - ту посилку на рядки, по кожній висказивательной змінної, перейти до п. 14. ...
