可分解理论

我们在本文中提出了一种用于求解特定称为“可分解理论”的理论中一阶公式的通用算法。首先，我们使用特殊量词器给出可分解理论的形式化描述并展示了其中的一些性质。然后，我们提出了一种在任何可分解理论“T”中求解一阶公式的通用算法。该算法以五条改写规则的形式给出。它将可能包含自由变量的一阶公式“P”转换为一 conjunction“Q”易于转换为由原子公式的存在量化联合词的布尔组合的已解公式。特别地，如果“P”没有自由变量，则“Q”要么是公式“true”，要么是公式“false”。我们的算法的正确性证明了可分解理论的完备性。最后，我们展示了“Tr”中有限或无限树的理论是可分解的，并给出了一些由我们算法的实现实现的基准测试，在“Tr”中解决具有超过160个嵌套交替量词的两方程博弈公式。