有限或无限树理论再探

本文提出了一种扩展的有限或无限树理论 $T$ 的一阶公理化体系，该体系建立在包含无限函数符号集和一个关系 $\fini(t)$ 的签名之上，后者用于区分有限树和无限树。我们证明了 $T$ 至少存在一个模型，并通过不仅提供判定过程，而且提供一个完整的一阶约束求解器来证明其完备性；该求解器能为 $T$ 中的任何一阶约束满足问题给出清晰且显式的解。该求解器以 16 条重写规则的形式给出，这些规则将任何一阶约束 $\phi$ 转换为等价的简单公式析取式 $\phi$，其中 $\phi$ 要么是公式 $\true$，要么是公式 $\false$，要么是至少含有一个自由变量的公式（既不等价于 $\true$ 也不等价于 $\false$），且自由变量的解以清晰显式的方式表达。我们规则的正确性蕴含了 $T$ 的完备性。我们还描述了该算法在 CHR（约束处理规则）中的实现，并将其性能与 C++ 实现以及最近针对可分解理论的判定过程进行了比较。