SPASS3.5与Dei定理证明器：功能升级与应用拓展

### SPASS 3.5与Dei定理证明器：功能升级与应用拓展 #### 1. SPASS Version 3.5特性升级 SPASS Version 3.5在多个方面进行了显著的改进，极大地提升了其性能和功能。 ##### 1.1 改进的分裂回溯（Improved Split Backtracking） 在SPASS 3.0及之前版本，分裂规则的实现已经包含了一种通过分支压缩实现的智能回溯方式。为每个子句在位域中存储其依赖的分裂信息。当推导出空子句时，可根据空子句的分裂位域轻松检查并移除那些对空子句无贡献的分裂。 近期，对分裂演算进行了细化。在每次分裂时，存储回溯其一个分支后得到的空子句的位域。若第二个分支也被反驳，可通过合并兄弟分支或子树的位域，将此信息在分裂树中向上传播，从而撤销那些对左右空子句都无贡献的分裂。实验表明，这一改进在TPTP问题上显著减少了分裂次数。在所有SPASS执行分裂且3.0和3.5版本都能解决的TPTP问题中，3.5版本平均每个问题进行783次分裂，而3.0版本为916次，节省了14%的分裂次数。此外，由于分裂改进，SPASS 3.5多解决了28个TPTP问题，虽然也有21个问题未能解决，但整体上赢得了49个问题。 | 版本 | 平均分裂次数 | 多解决问题数 | 未解决问题数 | 净增解决问题数 | | ---- | ---- | ---- | ---- | ---- | | 3.0 | 916 | - | - | - | | 3.5 | 783 | 49 | 21 | 28 | ##### 1.2 FLOTTER改进（Improvements to FLOTTER） FLOTTER是SPASS强大的CNF转换程序，包含诸如优化Skolem化等复杂转换规则，这些规则在CNF转换过程中需要进行证明计算。对于较大的问题，这些技术可能会消耗大量时间，导致FLOTTER无法在可接受的时间内终止。 为解决这一问题，对FLOTTER关键部分的实现进行了针对大问题的改进，并添加了新的标志来限制CNF转换期间的复杂约简操作： - `-CNFSub`：控制CNF转换期间的包含关系使用。 - `-CNFCon`：控制CNF转换期间的压缩操作使用。 - `-CNFRedTimeLimit`：设置FLOTTER在CNF翻译期间执行所有约简操作的总体时间限制。 ##### 1.3 其他增强功能（Further Enhancements） - **更快的解析（Faster Parsing）**：在SPASS 3.0之前，整体输入机制是为“小”输入文件开发的。为满足对“大”问题（如表达现实世界有限域理论）的需求，重新实现了SPASS的整体解析技术。现在，能够在不到10秒内解析60 MB的文件，并在约30秒内为像TPTP版本3.5.0中的SEU410 + 2这样的1 MB输入文件构建完整的FLOTTER CNF翻译和约简。 - **TPTP输入语法支持（TPTP Input Syntax Support）**：从SPASS 3.5版本开始，通过新标志`-TPTP`支持TPTP输入文件。由于TPTP输入文件可能包含包含命令，会在本地目录或TPTP环境变量指定的目录中解析这些命令。 - **包含命令（Include Commands）**：SPASS输入文件现在也可以包含包含指令，这些指令在解析时会被解析，包含的文件会在本地目录以及SPASSINPUTS环境变量绑定的目录中查找。 - **tptp2dfg工具**：新工具tptp2dfg可将TPTP输入文件转换为SPASS语法，通过`-include`标志可控制包含内容是展开还是转换为SPASS包含指令。 - **排序模块（Sort Module）**：在SPASS中，排序用于软类型和排序简化约简。重新实现了该模块，使其速度提高了约10倍，并扩展了其范围。 - **对称约简（Symmetric Reduction）**：在SPASS 3.0之前，一些更复杂的重写约简仅在正向实现。现在为所有约简规则添加了反向约简。 #### 2. Dei定理证明器：支持整数指数项 Dei是基于叠加的E - prover的扩展，允许输入语言中包含带