SPASS - Интернет в облаке

ПРОГРАММА:

ИМЯ

SPASS - автоматическое доказательство теорем для полной логики первого порядка с равенством

СИНТАКСИС

СПАСС [кредита] [входной_файл]

ОПИСАНИЕ

SPASS - это автоматическое средство доказательства теорем для полностью отсортированной логики первого порядка с равенством, которое
расширяет суперпозицию с помощью сортировки и правила разделения для анализа случаев. SPASS также может быть
используется в качестве средства доказательства теорем модальной логики и описательной логики.

ДОПОЛНИТЕЛЬНЫЕ ОПЦИИ

Параметры командной строки в SPASS реализованы посредством модификаций командной строки GNU.
пакет опций для C. Простое предоставление опции устанавливает ее значение в 1 и означает включение
вариант. Чтобы отключить параметр, значение должно быть установлено на 0, объявив -Опция= 0.
В настоящее время SPASS поддерживает следующие параметры:

-Авто
Включает / отключает автоматический режим, в котором SPASS настраивается автоматически. В
правила вывода / сокращения, технология сортировки, порядок и приоритет, а также
задаются стратегии разделения и выбора. В автоматическом режиме СПАСС завершен. Смешивание
автоматический режим с параметрами, определяемыми пользователем, может нарушить полноту. По умолчанию 1.

-Стдин
Включает / отключает ввод в SPASS через стандартный ввод. Аргумент файла игнорируется. По умолчанию 0.

-Интерактивный
Включает / отключает интерактивный режим. Сначала SPASS дается набор аксиом, а затем
доказывающий принимает последующие задачи доказательства. По умолчанию 0.

-Флоттер
Включает / отключает режим трансляции CNF для SPASS. Если опция установлена, только SPASS
выполняет перевод предложения в нормальной форме. Если не указан аргумент выходного файла SPASS
печатает CNF в стандартный вывод. По умолчанию 0.

-SOS
Включает / отключает набор стратегии поддержки. По умолчанию 0.

-Splits =n
Устанавливает количество возможных приложений разделения на n. Если n= -1, то количество
шпагаты не ограничены. По умолчанию 0.

-Память =n
Устанавливает объем памяти, доступной для SPASS для пробного поиска, равным n байтов. В
объем памяти, необходимый для запуска SPASS, не может быть ограничен. По умолчанию -1 означает, что
распределение памяти ограничено только доступной памятью.

-TimeLimit =n
Устанавливает ограничение по времени для поиска проверки на n секунд. По умолчанию -1 означает, что SPASS
может работать вечно. Срок опрашивается, когда SPASS выбирает новый пункт для
выводы. Если один шаг вывода вызывает взрыв до количества сгенерированных
статьями, поэтому может случиться так, что установленный срок значительно превышен.

-Документ SST
Включает / отключает вывод документации для статической мягкой печати. Используемая теория сортировки как
также печатается (неудачная) попытка доказательства ограничения сортировки. По умолчанию 0.

-Доказательство
Включает / отключает подтверждающую документацию. Если SPASS найдет доказательство, оно будет напечатано.
Если SPASS обнаруживает насыщение, в конечном итоге печатается насыщенный набор предложений.
Включение подтверждающей документации может значительно снизить производительность SPASS, потому что
доказывающая сторона должна хранить предложения, которые в противном случае можно было бы отбросить. По умолчанию 0.

-ДокСплит
Устанавливает документацию для разделенных шагов обратного отслеживания. Если установлено значение 1, текущая
печатается уровень возврата. Если установлено значение 2, он также распечатывается в случае разделения
вернуться к возвращенной clauese. По умолчанию 0.

-Петли
Устанавливает максимальное количество итераций основного цикла для SPASS. По умолчанию -1.

-PSub
Включает / отключает печать отдельных пунктов. По умолчанию 0.

-PRew
Включает / отключает печать простых приложений перезаписи. По умолчанию 0.

-ПКон
Включает / отключает печать приложений с конденсацией. По умолчанию 0.

-Птаут
Включает / отключает печать приложений удаления тавтологии. По умолчанию 0.

-PObv
Включает / отключает печать приложений очевидного сокращения. По умолчанию 0.

-PSSi
Включает / отключает печать приложений упрощения сортировки. По умолчанию 0.

-ПССТ
Включает / отключает печать статических приложений мягкой печати. Все удаленные статьи
напечатан. По умолчанию 0.

-ПМРР
Включает / отключает печать подходящих приложений для замены разрешения. По умолчанию
0.

-ПУНК
Включает / отключает печать приложений конфликта модулей. По умолчанию 0.

-ПАЭД
Включает / отключает печать предложений, в которых были удалены повторяющиеся уравнения
(удаление уравнения присваивания).

-ПДер
Включает / отключает печать предложений, полученных на основе выводов. По умолчанию 0.

-PДано
Включает / отключает печать данного предложения, выбранного для выполнения выводов.
По умолчанию 0.

-Лейблы
Включает / отключает печать этикеток. Если установлен -DocProof и нет меток для
формулы предоставляются входными данными, SPASS генерирует общие метки, которые затем
напечатано, включив эту опцию. По умолчанию 0.

-PKept
Включает / отключает печать сохраненных статей. Это предложения, порожденные выводами
(возврат), которые не являются избыточными. Предложения, полученные во время ввода
уменьшение / насыщенность не печатаются. По умолчанию 0.

-P Проблема
Включает / отключает печать набора входных предложений. По умолчанию 1.

-PEmptyClause
Включает / отключает печать производных пустых предложений. По умолчанию 0.

-ПСтатистический
Включает / отключает печать окончательной статистики по производным / обратным / сохраненным предложениям,
выполненные сплиты, использованное время и использованное пространство. По умолчанию 1.

-FPModel
Включает / отключает вывод найденной модели в файл. Если установлено значение 1, все
статьи в окончательном наборе печатаются. Если установлено значение 2, только потенциально продуктивные предложения
печатаются, то есть предложения без выбранного отрицательного литерала и максимального положительного
один. Если это имя входной проблемы и в конечном итоге сгенерированный
набор насыщен, насыщенность печатается в файл .model, для
в противном случае . статьи. Последний случай может быть вызван, например, временем
предел. По умолчанию 0.

-FPDFGДоказательство
Включает / отключает вывод найденного доказательства в файл. Используя эту опцию
требует установки опции -DocProof. Если это имя входа
проблема, на которую распечатано доказательство .prf. По умолчанию 0.

-Pфлаги
Включает / отключает вывод всех значений флагов. Настройки флага печатаются на
конец прогона SPASS в виде секции ввода DFG-Syntax. По умолчанию 0.

-ПоптСколем
Включает / отключает вывод оптимизированных приложений Skolemization. По умолчанию 0.

-ПСтрСколем
Включает / отключает вывод приложений с сильной сколемизацией. По умолчанию 0.

-ПБДК
Включает / отключает вывод предложений, удаленных из-за связанных ограничений. Дефолт
это 0.

-PBInc
Включает / отключает вывод связанных изменений ограничений. По умолчанию 0.

-PApplyDefs
Включает / отключает печать расширений определений атомов. По умолчанию 0.

-Выбрать
Устанавливает стратегию выбора для SPASS. Если установлено в 0, выбор отрицательных литералов невозможен.
сделано. Если установлено любое другое значение, не более одного отрицательного литерала в предложении
выбрано. Если установлено значение 1 отрицательный литерал в предложениях с более чем одним максимальным литералом
выбраны. Либо отрицательный литерал с предикатом из списка выбора (см.
ниже) выбран или, если такой отрицательный литерал недоступен, отрицательный литерал с
выбирается максимальный вес. Если установлено значение 2, всегда выбираются отрицательные литералы. Опять таки,
либо отрицательный литерал с предикатом из списка выбора (см. ниже)
выбран или, если такой отрицательный литерал недоступен, отрицательный литерал с максимальным
вес выбран. Последний случай приводит к упорядоченному гиперразрешению, подобному поведению
заказанного разрешения. Если установлено значение 3, любой отрицательный литерал с предикатом, заданным
список выбора (см. ниже) выбран. По умолчанию 1.

-RВвод
Включает / отключает сокращение начального набора предложений. По умолчанию 1.

-Сорта
Определяет монадические литералы, которые построили ограничение сортировки для начального предложения
установленный. Если установлено значение 0, ограничение сортировки не создается. Если установлено в 1, все отрицательные монадические
литералы с переменной в качестве аргумента образуют ограничение сортировки. Если установлено значение 2, все
отрицательные монадические литералы образуют ограничение сортировки. Установка -Sorts на 2 может навредить
полнота, поскольку ограничения сортировки подчиняются базовой стратегии и статическим
мягкий набор текста. По умолчанию 1.

-Сатвход
Включает / отключает насыщение входа. Насыщение неполное, но гарантированно
прекратить. По умолчанию 0.

-WDRсоотношение
Устанавливает соотношение между заданными предложениями, выбранными по весу или глубине поиска.
Космос. Вес - это сумма весов всех символов, определяемых -FuncWeight и
-VarWeight параметры. Глубина всех начальных предложений равна 0, а предложения, генерируемые
выводы получают максимальную глубину родительского предложения плюс 1. По умолчанию - 5, что означает
что 4 предложения выбраны по весу, а пятое предложение - по глубине.

-Предварительная конференция
Устанавливает коэффициент для вычисления веса гипотезы и, следовательно, позволяет
предпочитаю те. По умолчанию 0 означает, что вычисление веса для гипотез
не изменено.

-Полный красный
Включает / отключает полное уменьшение. Если установлено значение 0, будет использоваться только набор отработанных предложений.
полностью уменьшен. Если установлено в 1, все текущие предложения удержания (отработанные и
пригодны к использованию) полностью уменьшены. По умолчанию 1.

-FuncWeight
Устанавливает вес символов функции / предиката. Вес пунктов - это сумма всех
символ веса. Этот вес учитывается при выборе данного пункта.
По умолчанию 1.

-ВарВес
Устанавливает вес символов переменных (см. -FuncWeight). По умолчанию 1.

-ПрефВар
Включает / отключает предпочтение предложений со многими переменными. В то время как статьи
выбрано по весу, если этот параметр установлен и два предложения имеют одинаковый вес,
предложение с большим количеством переменных вхождений является предпочтительным. По умолчанию 0.

-BoundMode
Выбирает режим для связанных ограничений. Режим 0 означает отсутствие ограничений, если установлен в 1 все
новые сгенерированные предложения ограничены по весу (см. -BoundStart), и если установлено значение 2
статьи ограничены по глубине. По умолчанию 0.

-BoundStart
Ограничение начала выбранного режима привязки. Например, если режим привязки равен 1 и
ограниченное начало установлено в 5, все предложения с весом больше 5 удаляются до тех пор, пока
набор насыщен. Это вызывает увеличение используемого связанного значения, которое определяется
при минимальном увеличении, сохраняющем до удаленного пункта. По умолчанию -1 означает без ограничений
ограничение.

-Связанные петли
Количество циклов, применяющих ограничения действий / возрастающую границу. Если число
циклов превышено все связанные ограничения отменены. По умолчанию 1.

-ApplyDefs
Устанавливает максимальное количество применений определений атомов к входным формулам.
По умолчанию 0, что означает отсутствие приложений.

-Заказ
Устанавливает порядок терминов. Если 0, то выбирается KBO, если 1 выбирается RPOS. Дефолт
это 0.

-CNFQuantExch
Если установлено, непостоянные термины Сколема в клаузальной форме гипотезы заменяются
константами. Будет автоматически настроен для оптимизированного функционального перевода
формулы модальной или описательной логики. По умолчанию 0.

-CNFOptSkolem
Включает / отключает оптимизированную сколемизацию. По умолчанию 1.

-CNFStrSkolem
Включает / отключает сильную сколемизацию. По умолчанию 1.

-CNFroofSteps
Устанавливает максимальное количество шагов доказательства в оптимизированной попытке доказательства сколемизации.
По умолчанию 100.

-CNFSub
Включает / отключает отнесение к предложениям, сгенерированным процедурой CNF. Дефолт
это 1.

-CNFКон
Включает / отключает уплотнение предложений, генерируемых процедурой CNF. По умолчанию
1.

-CNFRedTime
Устанавливает общее количество времени в секундах, которое нужно потратить на сокращение во время CNF
трансформация. Затронутые сокращения оптимизированы Сколемизация, конденсация и
подчинение. По умолчанию -1 означает, что время сокращения вообще не ограничено.

-CNFПереименование
Включает / отключает переименование формулы. Если установлено значение 1, оптимизированное переименование включено,
минимизирует количество сгенерированных в конечном итоге предложений. Если установлено значение 2, сложное переименование
включен, который вводит новый предикат Сколема для каждой сложной формулы, т. е. любой
формула, которая не является буквальной. Если установлено значение 3, переименование квантификации включено,
вводит новый предикат Сколема для каждой подформулы, начинающейся с квантора.
По умолчанию 1.

-CNFRenMatch
Если установлено, переименованные подформулы заменяются тем же сколемским литералом. Дефолт
это 1.

-CNFPПереименование
Включает / отключает печать приложений для переименования формул. По умолчанию 0.

-CNFFEqR
Включает / отключает определенные методы уменьшения равенства на уровне формулы. Дефолт
это 1.

-ИМС
Включает / отключает правило вывода Пустая сортировка. По умолчанию 0.

-ISoR
Включает / отключает правило вывода Sort Resolution. По умолчанию 0.

-IEqR
Включает / отключает правило вывода Equality Resolution. По умолчанию 0.

-ИЕРРР
Включает / отключает разрешение рефлексивности правила вывода. По умолчанию 0.

-IEqF
Включает / отключает правило вывода Equality Factoring. По умолчанию 0.

-ИМПм
Включает / отключает правило вывода Merging Paramodulation. По умолчанию 0.

-ISPR
Включает / отключает правило вывода Superposition Right. По умолчанию 0.

-ВГДм
Включает / отключает правило вывода Ordered Paramodulation. По умолчанию 0.

-ISPm
Включает / отключает правило вывода Standard Paramodulation. По умолчанию 0.

-ИСпЛ
Включает / отключает правило вывода Superposition Left. По умолчанию 0.

-IORe
Включает / отключает правило вывода «Упорядоченное разрешение». Если установлено значение 1, заказано
Разрешение включено, но выводы о разрешении с уравнениями не создаются. Если
Если установлено значение 2, уравнения также учитываются для шагов упорядоченного разрешения. По умолчанию
0.

-ISRe
Включает / отключает стандартное разрешение правила вывода. Если установлено значение 1, Standard
Разрешение включено, но выводы о разрешении с уравнениями не создаются. Если
Если установлено значение 2, уравнения также рассматриваются для шагов стандартного разрешения. По умолчанию
0.

-Я стесняюсь
Включает / отключает правило вывода Standard Hyper-Resolution. По умолчанию 0.

-IOHy
Включает / отключает правило вывода Ordered Hyper-Resolution. По умолчанию 0.

- IURR
Включает / отключает правило вывода "Результирующее разрешение модуля". По умолчанию 0.

-IOFC
Включает / отключает правило вывода Ordered Factoring. Если установлено в 1, упорядоченный факторинг
включен, но генерируются только выводы факторинга с положительными литералами. Если установлено
до 2 отрицательные литералы также рассматриваются для вывода. По умолчанию 0.

-ISFc
Включает / отключает правило вывода Standard Factoring. По умолчанию 0.

-ИУнР
Включает / отключает разрешение модуля правила вывода. По умолчанию 0.

-ИБУР
Включает / отключает правило вывода «Ограниченное разрешение единицы глубины». По умолчанию 0.

-ИДЭФ
Включает / отключает правило вывода «Применить определения». В настоящее время не поддерживается.
По умолчанию 0.

-RFRew
Включает / отключает правило сокращения Forward Rewriting. Если установлено 1 единица перезаписи и
не-модульная перезапись на основе теста подчинения активируется. Если установлено значение 2 дополнительно
для модульной и не-модульной перезаписи активируется локальная контекстная перезапись. Если установлено значение 3
в дополнение к единичной и не единичной перезаписи контекстная перезапись под термином
активирован. Подчиненное контекстное переписывание включает в себя локальное контекстное переписывание. Если установлено
до 4 в дополнение к правилам перезаписи 3, субтермное контекстное переписывание также проверяет
для отрицательного буквального устранения. По умолчанию 0.

-RBRew
Включает / отключает правило сокращения Backward Rewriting. Те же значения и значение, что и
для флага -RFRew, но используется в обратном направлении. По умолчанию 0.

-РФМРР
Включает / отключает правило сокращения Forward Matching Replacement Resolution. Дефолт
это 0.

-РБМРР
Включает / отключает правило сокращения Backward Matching Replacement Resolution. Дефолт
это 0.

-РОбв
Включает / отключает правило сокращения "Очевидное сокращение". По умолчанию 0.

-RUnC
Включает / отключает правило сокращения Unit Conflict. По умолчанию 0.

-RTer
Включает / отключает терминатор, устанавливая максимальное количество неединичных предложений на
использоваться во время поиска. По умолчанию 0.

-RTаут
Включает / отключает правило сокращения «Удаление тавтологии». Если установлено в 1, только синтаксический
обнаруживаются и удаляются тавтологии. Если установлено значение 2, дополнительно семантические тавтологии
удалены. По умолчанию 0.

-РССТ
Включает / отключает правило сокращения Static Soft Typing. По умолчанию 0.

-RSSi
Включает / отключает правило сокращения «Упрощение сортировки». По умолчанию 0.

-RFSub
Включает / отключает правило сокращения Forward Subsuming Deletion. По умолчанию 0.

-RBSub
Включает / отключает правило сокращения Backward Subsuming Deletion. По умолчанию 0.

-RED
Включает / отключает правило редукции «Удаление уравнения назначения». Это правило удаляет
частные вхождения уравнений из пунктов. Если установлено в 1, уменьшение будет
гарантированно будет звук. Если установлено значение 2, снижение будет звучать только в том случае, если есть потенциал
Модель рассматриваемой задачи имеет нетривиальную область. По умолчанию 0.

-RCon
Включает / отключает правило уменьшения конденсации. По умолчанию 0.

-TDfg2OtterOptions
Включает / отключает включение заголовка параметров Otter. Эта опция применима только к
dfg2otter. Если установлено значение 1, он включает настройку, которая делает Otter почти готовой. Если установлено
значение 2 активирует автоматический режим, а если установлено значение 3, активирует режим auto2. По умолчанию
0.

-ЕМЛ
Специальный флаг EML для модальной логики или формул логики описания. Никогда не должно быть
установлен явно. Устанавливается при парсинге.

-EMLАвто
Предназначен для автономного режима EML, пока не работает. По умолчанию 0.

-EMLПеревод
Определяет метод перевода, используемый для формул модальной логики или логики описания.
Если установлено значение 0, стандартный метод реляционного перевода (который определяется
обычная семантика Крипке). Если установлено в 1, функциональный метод перевода
использовал. Если установлено значение 2, используется оптимизированный метод функциональной трансляции. Если установлено значение 3,
используется полуфункциональный метод перевода. Вариант оптимизированного
Функциональный метод перевода используется, если указаны следующие настройки:
-EMLTranslation = 2 -EMLFuncNary = 1. Перевод будет с точки зрения n-арного
предикаты вместо унарных предикатов и путей. В текущей реализации
стандартный метод реляционного перевода является наиболее общим. Некоторые ограничения распространяются на
другие методы. Функциональный метод перевода и полуфункциональный перевод
методы доступны только для базовой мультимодальной логики K(м) возможно с серийным
(всего) модальности (-EMLTheory = 1), плюс номиналы (утверждения ABox), терминологические
аксиомы и общие аксиомы включения и эквивалентности. Оптимизированный функционал
методы перевода реализованы только для K(m), возможно, с последовательными модальностями.
По умолчанию 0.

-EML2Rel
Если установлено, пропозициональные / логические формулы преобразуются в реляционные формулы.
прежде, чем они будут переведены в логику первого порядка. По умолчанию 0.

-ЭМЛТеория
Определяет, какая теория предполагается. Если установлено значение 0, основная теория
пустой. Если установлено значение 1, то для всех добавляется серийность (основная теория KD).
модальности. Если установлено значение 2, то рефлексивность (фоновая теория для KT) добавляется для
все модальности. Если установлено значение 3, то добавляется симметрия (базовая теория для KB).
для всех модальностей. Если установлено значение 4, то транзитивность (основная теория для K4) равна
добавлено для всех модальностей. Если установлено значение 5, то евклидовость (базовая теория для
K5) добавляется для всех модальностей. Если установлено в 6, то транзитивность и евклидовость
(базовая теория для S4) добавлена ​​для всех модальностей. Если установлено значение 7, то
рефлексивность, транзитивность и евклидовость (фоновая теория для S5) добавлены
для всех модальностей. По умолчанию 0.

-EMLFuncNdeQ
Если установлено, формулы ромба переводятся в соответствии с tr (dia (phi), s) = nde (s) / \ exists
x tr (phi, [sx]) (формула nde / квантора), иначе перевод будет в
в соответствии с tr (dia (phi), s) = exists x nde (s) / \ tr (phi, [sx]) (квантор / nde
формула). Перевод формул блока определяется попарно. Установка этого флага
имеет смысл только тогда, когда флаг функционального или полуфункционального метода перевода
установлен. По умолчанию 1.

-EMLFuncNary
Если установлено, используется функциональный перевод в рифленую логику. Это означает н-арный
предикатные символы используются вместо унарных предикатных символов и путей. Установка этого
flag имеет значение только для проверки локальной выполнимости / валидности в мультимодальном K.
По умолчанию 0.

-EMLFFSorts
Если установлено, используются сортировки терминов. По умолчанию 0.

-EMLElimComp
Если установлено, попробуйте исключить реляционную композицию в модальных параметрах. По умолчанию 0.

-ЭМЛПТранс
Если установлено, преобразование EML в логику первого порядка документируется. По умолчанию 0.

-ТТТП
Если установлено, SPASS ожидает входной файл в синтаксисе TPTP. По умолчанию 0.

-rf Если установлено, SPASS удаляет входной файл перед завершением. По умолчанию 0.

ПРИМЕРЫ

Чтобы запустить SPASS для одного файла без параметров:

СПАСС I

Чтобы отключить весь вывод SPASS, кроме окончательного результата:

SPASS -PGiven = 0 -PProblem = 0 I

ПРИМЕЧАНИЯ

Вы также можете указать параметры для SPASS в задаче ввода. В синтаксисе DFG вы должны
использование

list_of_settings (СПАСС).
{*
set_flag (Доказательство, 1).
*}
конец_списка.

чтобы установить флаг DocProof.

Во входных данных можно задать три типа параметров:

set_flag ( , ).
Устанавливает флаг в значение. Допустимые флаги и значения описаны в разделе ОПЦИИ.

set_precedence ( ).
Устанавливает приоритет для перечисленных символов. Приоритет уменьшается слева на
right, т. е. крайний левый символ имеет наивысший приоритет.

Каждая запись в списке имеет форму

СИМВОЛ | (СИМВОЛ, ВЕС [, {l, r, m}])

Вы можете использовать вторую форму для присвоения весов символам (для KBO) или статуса (для
RPOS). Статус: @t {l} для письма слева направо, @t {m} для мультимножества или @t {r} для
справа налево. Вес задается целым числом.

set_DomPred ( ).
Указанный предикат (ДомПред для доминирующего предиката) символы сначала упорядочиваются в соответствии с
согласно их приоритету, а не согласно их спискам аргументов. Только в случае равных
предикаты, аргументы исследуются. Например, если мы добавим опцию

set_DomPred (P).

затем в предложении

-> R (е (х, у), а), Р (х, а).

атом Р (х, а) строго максимальное. Предикаты, перечисленные set_DomPred вариант
сравнил по старшинству.

set_selection ( ).
Устанавливает список выбора, который может использоваться флагом Select (см. Выше).

set_ClauseFormulaRelation ( , последовательность
строки имени аксиомы)).
Этот список, в частности, установлен FLOTTER и включает SPASS для найденных в конечном итоге
доказательство, чтобы показать связь между предложениями, используемыми в доказательстве, и вводом
формулы. В сочетании с опцией DocProof должна быть запись для каждого
номер статьи. В противном случае выдается сообщение об ошибке.

set_ClauseFormulaRelation((1,ax2),(2,ax1),(3,ax3,ax1)).

Используйте SPASS онлайн с помощью сервисов onworks.net