Афонін, Андрій2012-07-162012-07-162009Афонін А. Про резолюційні стратегії з слабкою факторизацією / Афонін А. О. // Вісник Київського університету. Серія : Фізико-математичні науки. - 2009. - Вип. 4. – С. 69-72.https://ekmair.ukma.edu.ua/handle/123456789/1609Linear-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 the help of such strategies are demonstrated by means of examples.В роботі досліджуються резолюційні стратегії лінійного типу для впорядкованих диз'юнктів, що використовують ослаблений варіант правила факторізациі. Доведення їхньої коректності та повноти спирається на так зване літеральне числення. Особливості виведення за допомогою таких стратегій демонструються на прикладах.ukдиз'юнкткоректність методу пошуку несумісностілінійна резолюціяправило факторизаціїArticle