Выдра (доказатель теорем)

Выдра
Оригинальный автор(ы)	Уильям МакКьюн
Написано в	С
Тип	Автоматизированное доказательство теорем
Веб-сайт	www.mcs.anl.gov/research/projects/AR/otter/

Автоматизированный доказатель теорем

Otter — это автоматизированный доказатель теорем, разработанный Уильямом МакКьюном в Аргоннской национальной лаборатории в Иллинойсе. Otter был первым широко распространенным, высокопроизводительным доказателем теорем для логики первого порядка , и он стал пионером ряда важных методов реализации. Otter — это аббревиатура от Organized Techniques for Theorem-proving and Effective Research (организованные методы доказательства теорем и эффективного исследования) .

Описание

Otter основан на разрешении и парамодуляции, ограниченных порядками терминов, аналогичными тем, что используются в исчислении суперпозиции . Доказатель также поддерживает положительное и отрицательное гиперразрешение и стратегию множества поддержки. Поиск доказательств основан на насыщении с использованием версии алгоритма заданного предложения и контролируется несколькими эвристиками. Также существуют метаэвристики, автоматически определяющие параметры поиска. ^[1] Otter также был пионером в использовании эффективных методов индексации терминов для ускорения поиска партнеров вывода в больших наборах предложений. ^[2]

Otter был очень стабилен в течение ряда лет, но больше не разрабатывался активно. По состоянию на ноябрь 2008 года последняя запись в журнале изменений датирована 14 сентября 2004 года. Преемником Otter является Prover9 .

Программное обеспечение находится в общественном достоянии . Чикагский университет отказался заявлять о своих авторских правах на это программное обеспечение, и оно может использоваться, изменяться и распространяться (с изменениями или без них) общественностью. Однако «НИ ПРАВИТЕЛЬСТВО СОЕДИНЕННЫХ ШТАТОВ, НИ ЛЮБОЕ ЕГО АГЕНТСТВО [...] НЕ ЗАЯВЛЯЕТ, ЧТО ЕГО ИСПОЛЬЗОВАНИЕ НЕ БУДЕТ НАРУШАТЬ ПРАВА ЧАСТНОЙ СОБСТВЕННОСТИ». ^[3]

По словам Воса и Пипера, OTTER написан примерно на 28 000 строках языка программирования C. [ ^4]^{: 89–91}

Смотрите также

Мейс4

Примечания

^ МакКьюн, Уильям; Ларри Вос (1997). «Otter: воплощения соревнований CADE-13». Журнал автоматизированного рассуждения . 18 (2): 211–220. doi :10.1023/A:1005843632307.
^ МакКьюн, Уильям (1992). «Эксперименты с индексацией дерева дискриминации и индексацией путей для поиска терминов». Журнал автоматизированного рассуждения . 9 (2): 147–167. doi :10.1007/BF00245458.
^ Имя файла Legal в tarball
^ Вос, Ларри; Пипер, Гейл В. (1999). "3.11 OTTER и более ранние программы автоматического доказательства теорем". Увлекательная страна в мире вычислений: ваш путеводитель по автоматизированным рассуждениям . World Scientific. ISBN 978-9810239107.

Ссылки

Калман, Джон Арнольд (февраль 2001 г.). Автоматизированное рассуждение с OTTER . Rinton Press. ISBN 978-1589490048.

Внешние ссылки

Домашняя страница Otter
"OTTER 3.3 Reference Manual" (PDF) . Архивировано из оригинала 2018-11-13 . Получено 2018-11-13 .{{cite web}}: CS1 maint: бот: исходный статус URL неизвестен ( ссылка )

[CADE13-WC-1] МакКьюн, Уильям; Ларри Вос (1997). «Otter: воплощения соревнований CADE-13». Журнал автоматизированного рассуждения . 18 (2): 211–220. doi :10.1023/A:1005843632307.

[ATP1992-2] МакКьюн, Уильям (1992). «Эксперименты с индексацией дерева дискриминации и индексацией путей для поиска терминов». Журнал автоматизированного рассуждения . 9 (2): 147–167. doi :10.1007/BF00245458.

[InTar-3] Имя файла Legal в tarball

[Fascinating-4] Вос, Ларри; Пипер, Гейл В. (1999). "3.11 OTTER и более ранние программы автоматического доказательства теорем". Увлекательная страна в мире вычислений: ваш путеводитель по автоматизированным рассуждениям . World Scientific. ISBN 978-9810239107.