Реєстраційний номер
0207U008334,
0105U001346
, Науково-дослідна робота
Назва роботи
Розробити систему дедуктивних та індуктивних доведень теорем у математичному інформаційному середовищі.
Назва етапу роботи
Керівник роботи
Капітонова Ю.В.,Летичевський О.А.,
Дата реєстрації
10-12-2007
Організація виконавець
Інститут кібернетики ім. В.М.Глушкова НАН України
Опис етапу
Розроблено та реалізовано анотаційний чекер для SDL-специфікацій, що здійснює верифікацію SDL-програми шляхом її символьного моделювання. Розроблено новий метод побудови ефективної дедуктивної системи для аналізу тотожної істинності формул скінченнозначної логіки. Створено засоби реалізації алгоритмів поповнення критичними парами. Розроблена методику перевірки інваріантності формули, що базується на ітеративному поповненні множини інваріантів.
Опис продукції
Автори роботи
Додано/оновлено в НРАТ
2020-04-02
