професор
доктор фізико-математичних наук
професор
611
521-33-45
логіко-математичні засоби специфікацій програм, математична логіка
доктор фізико-математичних наук
професор
611
521-33-45
логіко-математичні засоби специфікацій програм, математична логіка
Закінчив з відзнакою факультет кібернетики Київського університету в 1973 році. Працює в університеті з 1973 року. У 1979 році під керівництвом В.Н. Редька захистив кандидатську дисертацію на тему “Дослідження синтаксичної структури мов програмування”. Посідає посаду доцента кафедри з 1983 року, наукове звання доцента отримав у 1987 році. У 2010 році захистив докторську дисертацію на тему “Спектр логік часткових предикатів, орієнтованих на композиційнo-номінативні моделі програм” за спеціальністю 01.05.01 – теоретичні основи інформатики та кібернетики.
Займався дослідженнями синтаксичної структури мов програмування, вивченням програмних алгебр та логік. У співпраці з проф. М.С. Нікітченком на базі спільного для логіки й програмування композиційно-номінативного підходу ним побудовано широкий спектр програмно-орієнтованих логічних формалізмів, що знаходяться на різних рівнях абстрактності й загальності. Описано мови та досліджено семантичні властивості композиційно-номінативних логік відповідного рівня. Виділено та досліджено неокласичні логіки, які близькі до класичної логіки предикатів і зберігають основні її закони, водночас ці логіки мають більші виразні можливості та істотно ширші класи семантичних моделей. Для композиційно-номінативних логік різних рівнів побудовано і досліджено формально-аксіоматичні системи гільбертівського та секвенційного типу, доведено їх коректність і повноту. Досліджено композиційно-номінативні логіки часткових однозначних, тотальних неоднозначних та часткових неоднозначних квазіарних предикатів. Для них запропоновано різні семантики та різні формалізації відношення логічного наслідку, побудовано числення секвенційного типу. Низка отриманих результатів є узагальненнями відомих тверджень класичної логіки. Результати досліджень застосовуються при розробці інформаційних та програмних систем, зокрема, систем специфікації та верифікації програм.
Математична логіка
Теорія алгоритмів