математична логіка, математическая логика ; теорія алгоритмів, теория алгоритмов
Побудовано спеціальні числення для перевірки виконуваності множин формул в чистих першопорядкових логіках квазіарних предикатів - числення виконуваних множин. Проаналізовано застосовність традиційних секвенційних числень та числень виконуваних множин. Для пропонованих числень доведено теореми коректності й повноти.
Построены специальные исчисления для проверки выполнимости множеств формул в чистых первопорядковых логиках квазиарных предикатов - исчисления выполнимых множеств. Проанализированы применимость традиционных секвенциальных исчислений и исчислений выполнимых множеств. Для предложенных исчислений доказаны теоремы корректности и полноты.
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 different 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.
