Формулюються резолюційні лінійні стратегії для упорядкованих диз'юнктів. Доказ їхньої коректності та повноти використовує спеціальне секвенційне числення.
Ключові слова: логіка першого порядку, диз'юнкт, факторізація, пошук суперечності, резолюція, стратегія
Linear strategies of the resolution type are formulated for ordered clauses. Their soundness and completeness are proven by using a special sequent-type calculus.
Key words: first-order logic, clause, factorization, refutation search, resolution, strategy.
