FLOTTER - 云端在线

程序：

您的姓名

SPASS - 具有等式的完全一阶逻辑的自动定理证明器

概要

斯帕斯 [选项[输入文件]

商品描述

SPASS 是一个自动定理证明器，用于完全排序的一阶逻辑，具有相等性
通过排序扩展叠加和案例分析的拆分规则。 SPASS也可以
用作模态逻辑和描述逻辑定理证明器。

配置

SPASS 中的命令行选项是通过修改 GNU 命令行实现的
C 的选项包。只提供选项将其值设置为 1 并意味着启用
选项。 为了禁用选项，必须通过声明将值设置为 0 -附加选项= 0。
SPASS 目前支持以下选项：

-汽车
启用/禁用 SPASS 自动配置自身的自动模式。 这
推理/归约规则、排序技术、排序和优先级以及
设置分裂和选择策略。 在自动模式下，SPAS 完成。 混合
具有用户定义选项的自动模式可能会破坏完整性。 默认值为 1。

-标准输入
通过标准输入启用/禁用 SPASS 中的输入。 文件参数被忽略。 默认值为 0。

-交互的
启用/禁用交互模式。 首先，给 SPASS 一组公理，然后
证明者接受后续的证明任务。 默认值为 0。

-弗洛特
启用/禁用 SPASS 的 CNF 转换模式。 如果设置了该选项，则仅 SPASS
执行子句范式翻译。 如果没有给出输出文件参数 SPASS
将 CNF 打印到标准输出。 默认值为 0。

-紧急求救
启用/禁用支持策略集。 默认值为 0。

-拆分=n
将可能的拆分应用程序的数量设置为 n。 如果 n=-1 那么数量
分裂没有限制。 默认值为 0。

-内存=n
将可供 SPASS 用于证明搜索的内存量设置为 n 字节。 这
无法限制启动 SPASS 所需的内存。 默认值为 -1 意味着
内存分配仅受可用内存的限制。

-时间限制=n
将证明搜索的时间限制设置为 n 秒。 默认为 -1 意味着 SPASS
可能永远运行。 当 SPASS 选择一个新的子句时轮询时间限制
推论。 如果单个推理步骤导致生成的数量激增
因此，可能会发生明显超出给定时间限制的情况。

-DocSST
启用/禁用静态软类型的文档输出。 使用的排序理论为
以及打印排序约束的（失败）证明尝试。 默认值为 0。

-文件证明
启用/禁用证明文件。 如果 SPASS 找到证明，它最终会被打印出来。
如果 SPASS 发现饱和，则最终会打印饱和的子句集。
启用证明文件可能会显着降低 SPASS 的性能，因为
证明者必须存储否则可以丢弃的子句。 默认值为 0。

-DocSplit
设置拆分回溯步骤的文档。 如果设置为 1，则当前
打印回溯级别。 如果设置为 2，它也会在拆分的情况下打印
回溯回溯的条款。 默认值为 0。

-循环
设置 SPASS 的最大主循环迭代次数。 默认值为 -1。

-PSub
启用/禁用包含子句的打印。 默认值为 0。

-PRW
启用/禁用简单重写应用程序的打印。 默认值为 0。

-PCon
启用/禁用冷凝应用程序的打印。 默认值为 0。

-PTt
启用/禁用重言式删除应用程序的打印。 默认值为 0。

-PObv
启用/禁用明显减少应用程序的打印。 默认值为 0。

-PSSi
启用/禁用排序简化应用程序的打印。 默认值为 0。

-PSST
启用/禁用静态软打字应用程序的打印。 所有删除的子句都是
打印。 默认值为 0。

-PMRR
启用/禁用匹配替换分辨率应用程序的打印。 默认是
0.

-PUNC
启用/禁用打印单元冲突应用程序。 默认值为 0。

-PAED
启用/禁用打印已删除冗余方程的子句
（分配方程删除）。

-PDer
启用/禁用打印推理派生的子句。 默认值为 0。

-P给定
启用/禁用给定子句的打印，选择执行推理。
预设为0。

-P标签
启用/禁用标签打印。 如果设置了 -DocProof 并且没有标签
公式由输入提供，SPAS 生成通用标签，然后
通过启用此选项打印。 默认值为 0。

-P保持
启用/禁用保留条款的打印。 这些是由推理生成的子句
（回溯）不是多余的。 输入期间派生的子句
不打印减少/饱和度。 默认值为 0。

-P问题
启用/禁用输入子句集的打印。 默认值为 1。

-PemptyClause
启用/禁用派生空子句的打印。 默认值为 0。

-P统计
启用/禁用导出/回溯/保留子句的最终统计信息的打印，
执行拆分，已用时间和已用空间。 默认值为 1。

-FP模型
启用/禁用将最终找到的模型输出到文件。 如果设置为 1，则所有
打印最终集中的子句。 如果设置为 2，则只有潜在的生产性条款
被打印出来，即没有选择否定字面量和最大肯定数的子句
一。 如果是输入问题的名称和最终生成的
set 是饱和的，饱和度被打印到文件中.model，对于
否则.条款。 例如，后一种情况可能是由时间引起的
限制。 默认值为 0。

-FPDFG证明
启用/禁用最终找到的证明输出到文件。 使用这个选项
需要设置选项 -DocProof。 如果是输入的名称
问题证明打印到.prf。 默认值为 0。

-PFlags
启用/禁用所有标志值的输出。 标志设置打印在
以 DFG-Syntax 输入部分的形式运行的 SPASS 结束。 默认值为 0。

-PoptSkolem
启用/禁用优化的 Skolemization 应用程序的输出。 默认值为 0。

-PStrSkolem
启用/禁用强大的 Skolemization 应用程序的输出。 默认值为 0。

-PBDC
启用/禁用由于绑定限制而删除的子句的输出。 默认
是0。

-PBInc
启用/禁用绑定限制更改的输出。 默认值为 0。

-P应用定义
启用/禁用打印原子定义的扩展。 默认值为 0。

-选择
设置 SPASS 的选择策略。 如果设置为 0，则不选择负文字
已经完成了。 如果设置为任何其他值，则子句中最多一个否定文字是
被选中。 如果在具有多个最大文字的子句中设置为 1 个否定文字
被选中。 带有选择列表中谓词的否定文字（请参阅
下面) 被选择，或者如果没有这样的否定文字可用，则使用否定文字
选择最大重量。 如果设置为 2 个负文字，则始终选择。 再次，
带有来自选择列表的谓词的否定文字（见下文）是
选择或如果没有这样的否定文字可用，则具有最大的否定文字
重量被选择。 后一种情况导致有序的超分辨率行为
的有序分辨率。 如果设置为 3 任何带有指定谓词的否定文字
选择列表（见下文）被选中。 默认值为 1。

-R输入
启用/禁用初始子句集的减少。 默认值为 1。

-排序
确定为初始子句构建排序约束的一元文字
放。 如果设置为 0，则不构建排序约束。 如果设置为 1，则所有负 monadic
以变​​量为参数的文字构成排序约束。 如果设置为 2，则所有
负一元文字形成排序约束。 将 -Sorts 设置为 2 可能会造成伤害
完整性，因为排序约束受基本策略和静态约束
软打字。 默认值为 1。

-卫星输入
启用/禁用输入饱和。 饱和是不完整的，但可以保证
终止。 默认值为 0。

-宽动态比
设置按权重或搜索深度选择的给定子句之间的比率
空间。 权重是由 -FuncWeight 和
-VarWeight 选项。 所有初始子句的深度为 0，生成的子句为
inferences 得到父子句的最大深度加 1。默认为 5，意思是
4条按权重选取，第XNUMX条按深度选取。

-PrefCon
设置比率以计算推测子句的权重，因此允许
更喜欢那些。 默认为 0 表示猜想子句的权重计算
没有改变。

-全红
启用/禁用完全减少。 如果设置为 0，则只有一组已处理的子句是
完全相互减少。 如果设置为 1，则所有当前保留的子句（已处理和
可用）完全相互减少。 默认值为 1。

-函数权重
设置函数/谓词符号的权重。 子句的权重是所有的总和
符号权重。 在选择给定条款时会考虑此权重。
预设为1。

-可变权重
设置变量符号的权重（请参阅 -FuncWeight）。 默认值为 1。

-PrefVar
启用/禁用对具有许多变量的子句的偏好。 while 子句是
按权重选择，如果设置了此选项并且两个子句具有相同的权重，则
具有更多变量出现的子句是首选。 默认值为 0。

-绑定模式
选择绑定限制的模式。 模式 0 表示没有限制，如果设置为 1 all
新生成的子句受权重限制（参见 -BoundStart），如果设置为 2
子句受深度限制。 默认值为 0。

-绑定开始
所选绑定模式的启动限制。 例如，如果绑定模式为 1 并且
bound start 设置为 5，所有权重大于 5 的子句都被删除，直到
集饱和。 这会导致所确定的使用边界值增加
通过最小的增加保存删除前的子句。 默认为 -1 表示没有限制
限制。

-绑定循环
应用动作限制/增加界限的循环次数。 如果数
超过循环次数，所有限制都被取消。 默认值为 1。

-应用定义
设置原子定义输入公式的最大应用次数。
默认值为 0，表示根本没有应用程序。

-订购
设置术语排序。 如果为 0，则选择 KBO，如果为 1，则选择 RPOS。 默认
是0。

-CNF量化交易所
如果设置，则替换猜想的子句形式中的非常量 Skolem 项
由常数。 将自动设置为优化的功能翻译
模态或描述逻辑公式。 默认值为 0。

-CNFptSkolem
启用/禁用优化的 Skolemization。 默认值为 1。

-CNFStrSkolem
启用/禁用强 Skolemization。 默认值为 1。

-CNF证明步骤
在优化的 Skolemization 证明尝试中设置证明步骤的最大数量。
预设为100。

-CNFSub
启用/禁用对 CNF 过程生成的子句的包含。 默认
是1。

-CNFCon
启用/禁用压缩 CNF 过程生成的子句。 默认是
1.

-CNFRedTime
设置在 CNF 期间花费在减少上的总时间（以秒为单位）
转型。 受影响的减少是优化的 Skolemization、冷凝和
包容。 默认值为 -1，表示减少时间完全不受限制。

-CNFR命名
启用/禁用公式重命名。 如果设置为 1 优化重命名启用
最小化最终生成的子句的数量。 如果设置为 2 复杂重命名是
启用为每个复杂公式引入新的 Skolem 谓词，即任何
不是文字的公式。 如果设置为 3 量化重命名启用
为每个以量词开头的子公式引入一个新的 Skolem 谓词。
预设为1。

-CNFRenMatch
如果设置，重命名变体子公式将替换为相同的 Skolem 文字。 默认
是1。

-CNFP重命名
启用/禁用公式重命名应用程序的打印。 默认值为 0。

-CNFFEqR
在公式级别启用/禁用某些等式减少技术。 默认
是1。

-IEMS
启用/禁用推理规则空排序。 默认值为 0。

-ISOR
启用/禁用推理规则排序解析。 默认值为 0。

-IqR
启用/禁用推理规则 Equality Resolution。 默认值为 0。

-IERR
启用/禁用推理规则 Reflexivity Resolution。 默认值为 0。

-IqF
启用/禁用推理规则 Equality Factoring。 默认值为 0。

-IMPm
启用/禁用推理规则合并辅助调制。 默认值为 0。

-ISPR
启用/禁用推理规则叠加权。 默认值为 0。

-眼压
启用/禁用推理规则 Ordered Paramodulation。 默认值为 0。

-ISPm
启用/禁用推理规则 Standard Paramodulation。 默认值为 0。

-ISPL
启用/禁用推理规则叠加左。 默认值为 0。

-IORe
启用/禁用推理规则 Ordered Resolution。 如果设置为 1，则有序
分辨率已启用，但不会生成方程的分辨率推断。 如果
设置为 2，方程也被考虑用于有序分辨率步骤。 默认是
0.

-ISRe
启用/禁用推理规则标准分辨率。 如果设置为 1，则标准
分辨率已启用，但不会生成方程的分辨率推断。 如果
设置为 2，标准分辨率步骤也考虑方程。 默认是
0.

-我害羞
启用/禁用推理规则标准超分辨率。 默认值为 0。

-IOHy
启用/禁用推理规则 Ordered Hyper-Resolution。 默认值为 0。

-IURR
启用/禁用推理规则单元结果分辨率。 默认值为 0。

-IOFc
启用/禁用推理规则 Ordered Factoring。 如果设置为 1，则有序因子分解
已启用，但仅生成具有正文字的因子推理。 如果设置
到 2，负文字也被考虑用于推理。 默认值为 0。

-ISFc
启用/禁用推理规则标准因式分解。 默认值为 0。

-IUnR
启用/禁用推理规则单元分辨率。 默认值为 0。

-IBUR
启用/禁用推理规则有界深度单位分辨率。 默认值为 0。

-IDEF
启用/禁用推理规则应用定义。 目前不支持。
预设为0。

-RFRew
启用/禁用减少规则前向重写。 如果设置为 1 个单元重写和
激活基于包含测试的非单元重写。 如果另外设置为 2
单元和非单元重写本地上下文重写被激活。 如果设置为 3
除了单元和非单元重写 subterm 上下文重写是
激活。 子项上下文重写包含本地上下文重写。 如果设置
to 4 除了3的重写规则，subterm contextual rewriting也测试
用于否定字面消除。 默认值为 0。

-RBrew
启用/禁用缩减规则向后重写。 相同的价值观和意义
用于标志 -RFRew 但用于反向。 默认值为 0。

-RFMRR
启用/禁用减少规则前向匹配替换分辨率。 默认
是0。

-RBMRR
启用/禁用减少规则向后匹配替换分辨率。 默认
是0。

-RObv
启用/禁用缩减规则 Obvious Reduction。 默认值为 0。

-RUNC
启用/禁用减少规则单元冲突。 默认值为 0。

-RTer
通过将非单元子句的最大数量设置为启用/禁用终止符
在搜索过程中使用。 默认值为 0。

-RT 拉紧
启用/禁用减少规则重言式删除。 如果设置为 1，则只有语法
重言式被检测和删除。 如果设置为 2，则附加语义重言式
被删除。 默认值为 0。

-RSST
启用/禁用减少规则静态软打字。 默认值为 0。

-RSSi
启用/禁用归约规则排序简化。 默认值为 0。

-RFSub
启用/禁用减少规则前向包含删除。 默认值为 0。

-RBSub
启用/禁用归约规则 Backward Subsumption Deletion。 默认值为 0。

-RAED
启用/禁用归约规则分配方程删除。 此规则删除
从句中特定出现的方程。 如果设置为 1，则减少为
保证是健全的。 如果设置为 2，则只有在任何潜在的情况下，减少才是合理的
所考虑问题的模型具有非平凡的域。 默认值为 0。

-RCon
启用/禁用缩减规则冷凝。 默认值为 0。

-TDfg2OtterOptions
启用/禁用包含 Otter 选项标头。 此选项仅适用于
dfg2otter。 如果设置为 1，它包括一个使 Otter 几乎完成的设置。 如果设置
设置为 2 则激活自动模式，如果设置为 3 则激活 auto2 模式。 默认是
0.

-EML
模态逻辑或描述逻辑公式的特殊 EML 标志。 永远不需要
明确设置。 在解析过程中设置。

-EML汽车
用于 EML 自治模式，但尚未起作用。 默认值为 0。

-EML翻译
确定用于模态逻辑或描述逻辑公式的翻译方法。
如果设置为 0，则标准关系转换方法（由
使用通常的 Kripke 语义）。 如果设置为 1，则函数翻译方法为
用过的。 如果设置为 2，则使用优化的功能翻译方法。 如果设置为 3，
使用半功能翻译方法。 优化的变体
当指定以下设置时，使用函数转换方法：
-EMLTranslation=2 -EMLFuncNary=1。 翻译将在 n 元方面
谓词而不是一元谓词和路径。 在目前的实施中
标准的关系翻译方法是最通用的。 一些限制适用于
其他方法。 功能翻译法和半功能翻译
方法仅适用于基本的多模态逻辑 K(m) 可能带有串行
（总）模态（-EMLTheory=1），加上名词（ABox 语句），术语
公理和一般包含和等价公理。 优化的功能
翻译方法仅适用于 K(m)，可能采用串行方式。
预设为0。

-EML2Rel
如果设置，则命题/布尔型公式转换为关系公式
在它们被转换为一阶逻辑之前。 默认值为 0。

-EML理论
确定假设的背景理论。 如果设置为 0，则背景理论为
空的。 如果设置为 1，则为所有添加序列性（KD 的背景理论）
方式。 如果设置为 2，则为自反性（KT 的背景理论）添加
所有方式。 如果设置为 3，则添加对称性（KB 的背景理论）
适用于所有方式。 如果设置为 4，则传递性（K4 的背景理论）为
为所有方式添加。 如果设置为 5，则 Euclideanness（背景理论
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]) (a 量词 / nde
公式）。 盒式公式的翻译是双重定义的。 设置这个标志是
仅当标记为功能或半功能翻译方法时才有意义
设置。 默认值为 1。

-EMLF函数
如果设置，则使用功能转换为凹槽逻辑。 这意味着 n 元
使用谓词符号代替一元谓词符号和路径。 设置这个
flag 仅对测试多模态 K 中的局部可满足性/有效性有意义。
预设为0。

-EMLF排序
如果设置，则使用术语排序。 默认值为 0。

-EMLElimComp
如果设置，尝试消除模态参数中的关系组合。 默认值为 0。

-EMLPTrans
如果设置，则记录 EML 到一阶逻辑的转换。 默认值为 0。

-TPTP
如果设置，SPAS 需要 TPTP 语法的输入文件。 默认值为 0。

-rf 如果设置，SPAS 将在终止前删除输入文件。 默认值为 0。

示例

要在没有选项的情况下对单个文件运行 SPASS：

一期

要禁用除最终结果之外的所有 SPASS 输出：

SPASS -PGiven=0 -PProblem=0 I

附注

您还可以在输入问题中为 SPASS 指定选项。 在 DFG 语法中，你会
使用

list_of_settings(SPAS)。
{*
set_flag(DocProof,1)。
*}
end_of_list。

设置 DocProof 标志。

您可以在输入中设置三种类型的选项：

设置标志（ , ）。
将标志设置为值。 有效的标志和值在 OPTIONS 部分中描述。

设置优先级（ ）。
设置列出的符号的优先级。 优先级从左到右依次递减
右，即最左边的符号具有最高优先级。

列表中的每个条目都具有以下形式

符号 | (符号, 重量 [, {l, r, m}])

您可以使用第二种形式为符号（对于 KBO）或状态（对于
RPOS）。 状态为@t{l} 表示从左到右，@t{m} 表示多集，或@t{r} 表示
右到左。 重量以整数形式给出。

set_DomPred( ）。
列出谓词 (多普雷德 对于显性谓词）符号首先根据
根据他们的优先级，而不是根据他们的参数列表。 只有在相等的情况下
谓词，参数被检查。 例如，如果我们添加选项

set_DomPred(P)。

然后在条款中

-> R(f(x,y),a), P(x,a)。

原子 P(x,a) 是严格的最大值。 列出的谓词 设置_DomPred 选项是
按照先后顺序进行比较。

设置选择（ ）。
设置 Select 标志可以使用的选择列表（见上文）。

set_ClauseFormulaRelation( , 序列
公理名称字符串））。
该列表特别由 FLOTTER 设置，并为最终找到的
证明显示证明中使用的子句与输入之间的关系
公式。 如果与选项 DocProof 结合使用，则每个条目都需要一个条目
条款编号。 否则报错。

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

使用 onworks.net 服务在线使用 FLOTTER