У роботі досліджується задача перевірки виконуваності формул у композиційно-номінативних логіках кванторно-екваційного рівня. Розглядаються логіки із композицією слабкої рівності. Доводиться, що задача перевірки виконуваності може бути частково зведена до аналогічної задачі у класичних логіках предикатів першого порядку із рівністю. Запропонований метод дозволяє застосовувати наявні процедури перевірки виконуваності для класичних логік для вирішення поставленої задачі, але є неповним.
The satisfiability problem in composition-nominative logics of quantifier-equational level is investigated. Logics with weak equality composition are considered. We prove that the problem in hand can be partly reduced to the satisfiability problem for classical first-order predicate logics with equality. The method proposed enables usage of existent satisfiability checking procedures also for quantifier-equational composition-nominative logics with weak equality, however this method is incomplete.
