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

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

Otter — это автоматизированное средство доказательства теорем, разработанное Уильямом МакКьюном в Аргоннской национальной лаборатории в Иллинойсе. Otter был первым широко распространенным высокопроизводительным средством доказательства теорем для логики первого порядка , а также первым, кто использовал ряд важных методов реализации. Выдра — это аббревиатура от « Организованные методы доказательства теорем и эффективных исследований» .

Описание

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

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

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

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

См. также

Мейс4

Примечания

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

Ссылки

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

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

Домашняя страница Выдры
«Справочное руководство OTTER 3.3» (PDF) . Архивировано из оригинала 13 ноября 2018 г. Проверено 13 ноября 2018 г. {{cite web}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )

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

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

[InTar-3] Имя файла Legal в архиве.

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

[1]

[2]

[3]

[4]