Тимофєєв В. Г. Дослідження та розробка алгоритмів перевірки виконуваності в логіках композиційно-номінативного типу.

Композиційно-номінативні логіки є узагальненням класичних логік на класи часткових предикатів та функцій з нефіксованою арністю. Такі логіки видаються адекватним формалізмом для побудови формальних моделей програм та проведення міркувань над ними. В роботі розглядаються пропозиційні, реномінативні, кванторні, чисті першопорядкові, першопорядкові, багатосортні чисті першопорядкові та багатосортні першопорядкові композиційно-номінативні логіки. Для логік вказаних типів запропоновано методи перевірки виконуваності формул, доведено їх коректність та сформульовано алгоритми такої перевірки. Принциповою ідеєю побудованих алгоритмів є зведення задачі перевірки виконуваності формули в композиційно-номінативній логіці до аналогічної задачі для класичних логік.