Формулюються лінійні стратегії для впорядкованих диз'юнктів з правилами резолюції, парамодуляції та слабкою факторизації. Даються результати про їх коректність та повноту для класичної логіки з рівністю.
Ключові слова: факторизація, резолюція, парамодуляція, диз'юнкт, класична логіка першого порядку з рівністю, стратегія.
Linear strategies are formulated for the resolution rule, weak factorization rule, and paramodulation rule being applied to ordered clauses. Their soundness and completeness are given for classical logic with equality.
Key words: clause, factorization, resolution, paramodulation, first-order logic with equality, strategy.
