Splitting Through New Proposition Symbols
Splitting Through New Proposition Symbols
复制标题
通过新的命题符号进行分裂
DOI：
10.1007/3-540-45653-8_12
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Hans de Nivelle
中科院分区：
文献类型：
--
作者：
Hans de Nivelle
拆分规则是类似表格的规则，用于解析上下文。如果搜索状态包含子句 C1 V C2，且 C1 和 C2 之间没有共享变量，则证明者会拆分搜索状态，并尝试分别反驳 C1 和 C2。
我们可以创建一个新的命题符号 α，并用 C1 V α 和 Øα V C2 替换 C1 V C2，而不是分割定理证明者的状态。在第一个子句中，a 是最不优选的文字。在第二个子句中选择α。这样，只要C1没有被反驳，C2就无能为力。
这种拆分方式仅部分模拟搜索状态拆分，因为从 C1 V α 继承的子句无法包含或简化不从 C1 继承的子句。通过搜索状态分割，从 C1 继承的子句原则上可以包含或简化不是从 C1 派生的子句。因此，通过新符号进行分裂不如搜索状态分裂强大。在本文中，我们提出了这个问题的解决方案。
The splitting rule is a tableau-like rule, that is used in the resolution context. In case the search state contains a clause C1 V C2, which has no shared variables between C1 and C2, the prover splits the search state, and tries to refute C1 and C2 separately.
Instead of splitting the state of the theorem prover, one can create a new proposition symbol α, and replace C1 V C2 by C1 V α and ¬α V C2. In the first clause a is the least preferred literal. In the second clause α is selected. In this way, nothing can be done with C2 as long as C1 has not been refuted.
This way of splitting simulates search state splitting only partially, because a clause that inherits from C1 V α cannot subsume or simplify a clause that does not inherit from C1. With search state splitting, a clause that inherits from C1 can in principle subsume or simplify clauses that do not derive from C1. As a consequence, splitting through new symbols is less powerfull than search state splitting. In this paper, we present a solution for this problem.