论文标题
两个可变逻辑，最终定期计数
Two variable logic with ultimately periodic counting
论文作者
论文摘要
我们考虑使用两个变量逻辑的扩展，并指出公式保留的元素的数量应属于给定的最终定期集。我们表明，逻辑的可满足性和有限性是可决定的。我们还表明，在前爆发算术中，任何句子的频谱都是可以定义的。在此过程中，我们向``双毛图方法''提供了几种改进。在这种方法中，有关两种可变性逻辑的可决定性问题被简化为有关与分区图关联的整数向量确定性的问题，在分区中，分区中的节点满足其内和级别的某些约束。
We consider the extension of two variable logic with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the ``biregular graph method''. In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.
