Побудовано спеціальні числення для перевірки виконуваності множин формул в чистих першопорядкових логіках квазіарних предикатів - числення виконуваних множин. Проаналізовано застосовність традиційних секвенційних числень та числень виконуваних множин. Для пропонованих числень доведено теореми коректності й повноти.
Построены специальные исчисления для проверки выполнимости множеств формул в чистых первопорядковых логиках квазиарных предикатов - исчисления выполнимых множеств. Проанализированы применимость традиционных секвенциальных исчислений и исчислений выполнимых множеств. Для предложенных исчислений доказаны теоремы корректности и полноты.
Special sequent calculi to check satisfiability of sets of formulas in pure first-order logics of quasiarypredicates are constructed. They are called calculi of satisfiable sets. Axioms of the proposed calculi are closed (inconsistent) sets of formulas; inferences rules are forms of decomposition. Applicability of such calculi and traditional sequent calculi are analyzed. In logics of non-deterministic predicates the traditional notion of satisfiability becomes trivial therefore calculi of satisfiable sets are used only for logics of deterministic predicates. Moreover, sequent calculi are built for diff&erent relations of logical consequence both for deterministic and total and partial non-deterministic predicates. For the proposed calculi closedness conditions of sets of formulas and forms of decomposition are described. Soundness and completeness &theorems are proved for the proposed calculi.
