Деякі наукові досягнення факультету кібернетики

Система автоматизації дедукції (САД)

Мета

Автоматизація наукової й освітньої діяльності теоретичних і прикладних досліджень в рамках програми Алгоритм Очевидності (Evidence Algorithm)

Програму було запропоновано В.М. Глушковим для створення засобів дедуктивної та аналітичної обробки комп'ютерних знань, поданих близькою до природної формальною мовою.

Актуальність

Ефективність практичних застосувань інформаційних технологій залежить від методів автоматизації міркувань, які необхідні для проведення логічних умозаключень.

Основами є:

• машинні методи пошуку логічного виводу в сигнатурі початкової формальної теорії
• лінгвістичні засоби представлення теорій у вигляді, зручному для користувача, з застосування напівформальних мов, близьких до відповідних фрагментів природної мови

Галузі застосування

• Автоматизація міркувань
• Перевірка коректності математичних (та інших формалізованих) текстів
• Дистанційне навчання математичним дисциплінам
• Виділення знань з математичних праць
• Створення баз формалізованих знань
• Перевірка коректності протоколів (криптографічних, комунікаційних й т.п.)
• Верифікація програмного та апаратного забезпечення

Переваги

• САД є однією із провідних світових систем допомоги людині в інтелектуальній (математичній) діяльності.
• За низкою прийнятих рішень і характеристик САД перевершує їх.
• САД не має аналогів в Україні.

Апробація

Проведено ряд експериментів по верифікації реальних математичних текстів.

Публікації

• Lyaletski A., Paskevich A., and Verchinine K. SAD as a mathematical assistant – How should we go from here to there? // Journal of Applied Logic. – 2006. – P. 560-591.
• Lyaletski A. Sequent forms of Herbrand theorem and their applications // Annals of Mathematics and Artificial Intelligence, Springer. – 2006. – V. 46, № 1-2. – P. 191-230.
• Лялецкий А.В. Эвиденциальная парадигма: логический аспект // Кибернетика и системный анализ. – 2003. – № 5. – С. 37-47.

Основні результати

Розроблено лінгво-дедуктивний підхід для здійснення автоматизації міркувань з метою підтримки інтелектуальної діяльності людини в різних галузях.

Версія здійснює автоматичний пошук виведень в логіці 1-го порядку та верифікує математичні тексти, подані природною формальною мовою.

Реалізовано онлайновий доступ до системи САД, яку розміщено на сервері факультету кібернетики Київського національного університету імені Тараса Шевченка