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