E (доказательство теоремы)
-
Обзор системы E
- E — инструмент для доказательства теорем в полной логике первого порядка с равенством.
- Основан на эквациональном суперпозиционном исчислении, использует чисто эквациональную парадигму.
- Интегрирован в другие системы и занял высокие места в соревнованиях по доказательству теорем.
-
Разработка и особенности
- Создан Стефаном Шульцем, разработан в Мюнхенском техническом университете и Государственном кооперативном университете Баден-Вюртемберга.
- Включает совместное переписывание терминов, эффективные структуры данных индексации, расширенные стратегии выбора букв и методы машинного обучения.
- Поддерживает многосортированную логику с версии 2.0.
-
Реализации и лицензии
- Реализован на C, совместим с UNIX и Cygwin.
- Доступна под лицензией GNU GPL.
-
Результаты в соревнованиях
- E показал высокие результаты в CADE ATP System, выиграл в 2000 и 2010 годах.
- Занял второе место в 2008 и 2009 годах, получил награду «лучшая система в целом» в 2010 году.
-
Применение
- Интегрирован в другие программы для доказательства теорем, включая Isabelle Sledgehammer и LEO-II.
- Используется для рассуждений о больших онтологиях, верификации программного обеспечения и сертификации.
-
Рекомендации
- Ссылки на электронную домашнюю страницу и разработчика E.