Это командная выдра, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
otter - программа для доказательства теорем в стиле разрешения
СИНТАКСИС
выдра < входной файл > выходной файл
ОПИСАНИЕ
Эта страница руководства кратко документирует выдра команда.
выдра представляет собой программу доказательства теорем в стиле резольвента для логики первого порядка с равенством.
выдра включает в себя двоичное разрешение правил вывода, гиперразрешение, UR-разрешение и
двоичная парамодуляция. Некоторые из его других способностей и функций являются преобразованием с первого взгляда.
упорядочить формулы по статьям, прямое и обратное подчинение, факторинг, взвешивание, ответ
литералы, порядок терминов, прямая и обратная демодуляция, оцениваемые функции и
предикаты, завершение Кнута-Бендикса и стратегия подсказок.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
Параметры командной строки не принимаются; все параметры указаны во входном файле.
Используйте otter онлайн с помощью сервисов onworks.net
