Про резолюційні стратегії з слабкою факторизацією
Loading...
Date
2009
Authors
Афонін, Андрій
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
В роботі досліджуються резолюційні стратегії лінійного типу для впорядкованих диз'юнктів, що використовують ослаблений варіант правила факторізациі. Доведення їхньої коректності та повноти спирається на так зване літеральне числення. Особливості виведення за допомогою таких стратегій демонструються на прикладах.
Description
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 the help of such strategies are demonstrated by means of examples.
Keywords
диз'юнкт, коректність методу пошуку несумісності, лінійна резолюція, правило факторизації
Citation
Афонін А. Про резолюційні стратегії з слабкою факторизацією / Афонін А. О. // Вісник Київського університету. Серія : Фізико-математичні науки. - 2009. - Вип. 4. – С. 69-72.