Выдра (доказательство теоремы)
-
Описание Otter
- Otter — инструмент для доказательства теорем, разработанный в Аргоннской лаборатории.
- Основан на разрешении и парамодуляции, с ограничениями порядка элементов.
- Поддерживает положительное и отрицательное гиперрешение, а также стратегию набора вспомогательных средств.
- Поиск доказательств основан на алгоритме с эвристиками и мета-эвристиками для оптимизации поиска.
- Ускоряет поиск партнеров по выводу с помощью эффективных методов индексации терминов.
-
История и развитие
- Otter был стабилен в течение многих лет, но не получал активного развития после 2004 года.
- Prover9 стал преемником Otter.
-
Доступность и авторские права
- Otter находится в открытом доступе, Чикагский университет не защищает авторские права.
- Использование Otter не нарушает права частной собственности, но не подтверждено правительством США.
-
Технические детали
- Программа написана на языке программирования Си, содержит около 28 000 строк кода.
-
Ссылки
- Ссылки на Mace4, записи и рекомендации, а также на домашнюю страницу Otter.