递归方案、MSO逻辑和U量词
摘要：递归方案模型检测问题的可决问题、递归方案生成的树是否满足给定的逻辑句子。对于MSO逻辑的句子已知该问题是可决的。我们证明了在MSO的扩展中可决，其中还有一个不限定量化符号U，意味着子公式在任意大的有限集合上为真。这个量化符号只能用于所有自由变量表示有限集合的子公式（而不受限制地使用该量化符号会导致不可决）。我们还展示了递归方案生成的树对于反射和有效选择的性质。
作者：Pawe{l} Parys
论文ID：1810.04763
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22