Системы автоматизированного построения логического вывода и их приложения
Преподаватели:
Канович Макс Иосифович
Департамент анализа данных и искусственного интеллекта: Профессор
Яворский Ростислав Эдуардович
Департамент анализа данных и искусственного интеллекта: Доцент
- Формальные языки и исчисления
- Разрешающие алгоритмы для пропозициональных логик
- SAT-солверы
- Автоматические солверы для модальных логик
- Semantic Web и его инструменты
- Логика первого и второго порядка
- Теория типов
- SMT-солверы
- Формализация свойств вычислительных систем в теории типов и логике высших порядков
- Системы автоматизированного построения вывода HOL, Coq и их использование в задачах верификации
Программа дисциплины (PDF, 648 Кб)