В роботі досліджуються резолюційні стратегії лінійного типу для впорядкованих диз'юнктів, що використовують ослаблений варіант правила факторизациї. Доведення їхньої коректності та повноти спирається на так зване літеральне числення. Особливості виведення за допомогою таких стратегій демонструються на прикладах.
Ключові слова: диз'юнкт, коректність методу пошуку несумісності, лінійна резолюція, повнота методу пошуку несумісності, правило резолюції, правило факторизації, числення.
Linear-type resolution strategies using a simplified modification of the factorization rule for ordered clause are investigated in the paper. The proofs of their soundness and completeness are based on a so-called literal calculus. Peculiarities of inference search with thehelp of such strategies are demonstrated by means of examples.
Key words: clause, soundness of refutation method, linear resolution, completeness of refutation method, resolution rule, factorization rule, calculus.
