Tymofieiev V. Investigation and development of algorithms for checking satisfiability in composition-nominative logics.

The goal of the thesis is to develop satisfiability checking methods for formulas of composition-nominative logics that are oriented on specification of program models. Composition-nominative logics are generalizations of classical logics on classes of partial predicates and functions with non-fixed arity. Such logics appear to be an adequate formalism for constructing and reasoning about formal models of programs. In the thesis such types of logics are considered: propositional, renominative, quantifier, pure first-order, first-order, many-sorted pure first-order, and many-sorted first order composition-nominative logics. For logics of these kinds methods of satisfiability checking are proposed, correctness of the methods is proved and algorithms of satisfiability checking are formulated. The underlying idea of the algorithms constructed consists in reduction of satisfiability problem for a composition-nominative logic to the same problem in some fragment of classical first-order logic. The algorithms developed allow to leverage existing methods and tools for satisfiability checking in first-order logic for checking satisfiability of formulas of composition-nominative logics. Such algorithms provide new possibilities for using composition-nominative logics in formal development of software and hardware systems.