Система автоматического доказательства теорем в исчислении позитивно-образованных формул pcfbucket
автоматическое доказательства теорем логический вывод позитивно-образованные формулы
Программа pcfbucket предназначена для автоматического доказательства теорем в исчислении позитивно-образованных формул (ПОФ). Данная программа специализирована для решения класса ПОФ без неограниченных переменных. Для данного класса разработаны эффективные алгоритмы поиска логического вывода. Программа позволяет отслеживать всю историю логического вывода от самого начала решения проблемы; производить откат системы назад в случае неудачных попыток выбора пути решения; подключать дополнительные стратегии логического вывода, написанные на языке Rust (Раст). Кроме того, реализованы методы, направленные на экономию используемой оперативной памяти, такие как разделение общих структур данных формул (терм, подформула, подстановка).
Для решения задач планирования действий. Для проверки различных свойств дискретно-событийных систем (наблюдаемость, ко-наблюдаемость, управляемость).
Игорь
Бычков
Вячеславович
директор
Доктор технических наук
Академик
O-1579-2013
56308077400
62875
РОССИЯ
Игорь
Бычков
Вячеславович
директор
РОССИЯ
28.23.29
Программная реализация интеллектуальных систем
28.23.11
Языки представления и языки манипулирования знаниями
28.23.17
Логика в искусственном интеллекте
01.02.EP
COMPUTER SCIENCE, ARTIFICIAL INTELLIGENCE
Александр
Ларионов
Александрович
Разработка архитектуры и алгоритмов программы, реализация программного кода, тестирование
РОССИЯ
ФАНО России
Федеральное агентство научных организаций
5137746009462
Организация
Правительство Российской Федерации
Федеральные государственные бюджетные учреждения
ИДСТУ СО РАН
Федеральное государственное бюджетное учреждение науки Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук)
1023801757000
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные бюджетные учреждения