Это команда prover9, которую можно запустить в бесплатном хостинг-провайдере OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
prover9 - средство доказательства теорем о разрешении / парамодуляции
СИНТАКСИС
испытатель9 [кредита] входной файл > выходной файл
испытатель9 [кредита] -ф входной файл > выходной файл
ОПИСАНИЕ
Эта страница руководства кратко документирует испытатель9 команда.
испытатель9 представляет собой автоматическое средство доказательства теорем для логики первого порядка и эквациональной логики. Это
наследник выдра(1) прувер. испытатель9 использует методы логического вывода упорядоченных
разрешение и парамодуляция с буквальным выбором.
ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ
Сводка опций приведена ниже.
-h Просмотрите список параметров командной строки.
-x Включает экспериментальный улучшенный автоматический режим. Для получения дополнительной информации обратитесь к
испытатель9 руководство.
-p Вывод полностью в скобках.
-t n Ограничьте поиск продолжительностью около n секунд. Для UNIX-подобных систем параметр user
Используется процессорное время.
-f файл
Принимайте участие в файл вместо стандартного ввода.
Используйте prover9 онлайн с помощью сервисов onworks.net
