Otter — это автоматизированное средство для доказательства теорем , разработанное Уильямом МакКьюном в Аргоннской национальной лаборатории в Иллинойсе. Otter был первым широко распространенным высокопроизводительным средством доказательства теорем для логики первого порядка , а также первым, кто использовал ряд важных методов реализации. Выдра — это аббревиатура от « Организованные методы доказательства теорем и эффективных исследований» .
Otter основан на разрешении и парамодуляции, ограниченной упорядочением членов, аналогичным тому, которое используется в исчислении суперпозиции . Доказывающее устройство также поддерживает положительное и отрицательное гиперразрешение и стратегию набора поддержки. Поиск доказательства основан на насыщении с использованием версии алгоритма данного предложения и контролируется несколькими эвристиками. Также существуют метаэвристики, автоматически определяющие параметры поиска. [1] Оттер также был пионером в использовании эффективных методов индексации терминов для ускорения поиска партнеров по выводу в больших наборах предложений. [2]
Выдра была очень стабильной в течение ряда лет, но больше не развивается активно. По состоянию на ноябрь 2008 года последняя запись в журнале изменений датирована 14 сентября 2004 года. Преемником Otter является Prover9 .
Программное обеспечение находится в свободном доступе . Чикагский университет отказался заявить о своих авторских правах на это программное обеспечение, и оно может использоваться, изменяться и распространяться (с изменениями или без них) общественностью. Однако «НИ ПРАВИТЕЛЬСТВО СОЕДИНЕННЫХ ШТАТОВ, НИ КАКОЕ-ЛИБО ЕГО АГЕНТСТВО [...] НЕ ЗАЯВЛЯЕТ, ЧТО ЕГО ИСПОЛЬЗОВАНИЕ НЕ НАРУШАЕТ ЧАСТНЫЕ ПРАВА». [3]
По словам Воса и Пипера, OTTER написан примерно на 28 000 строк на языке программирования C. [4] : 89–91.