Мета дослідження - розробка методів перевірки виконуваності формул композиційно-номінативних логік, що орієнтовані на специфікування моделей програм. Композиційно-номінативні логіки є узагальненням класичних логік на класи часткових предикатів і функцій з нефіксованою арністю. Розглянуто пропозиційні, реномінативні, кванторні, чисті першопорядкові, першопорядкові, багатосортні чисті першопорядкові та багатосортні першопорядкові композиційно-номінативні логіки. Для логік вказаних типів запропоновано методи перевірки виконуваності формул, доведено їх коректність та сформульовано алгоритми такої перевірки. Зазначено, що принциповою ідеєю побудованих алгоритмів є зведення задачі перевірки виконуваності формули в композиційно-номінативній логіці до аналогічної задачі для класичних логік. Розроблені алгоритми дозволяють застосувати наявний інструментарій перевірки виконуваності формул класичних логік до перевірки виконуваності формул композиційно-номінативних логік. З'ясовано, що наявність таких алгоритмів відкриває нові можливості для використання композиційно-номінативних логік у формальних підходах до розробки програмних та апаратних систем.

• Тимофєєв Валентин Георгійович (фізико-математичні науки)

  Якщо, ви не знайшли інформацію про автора(ів) публікації, маєте бажання виправити або відобразити більш докладну інформацію про науковців України запрошуємо заповнити "Анкету науковця"