二変数論理式における最終的に周期的な計数

本論文では、二変数論理式FO2にPresburger算術の量化子を追加した拡張論理式FO2Presの満足可能性と有限満足可能性が決定可能であることを示す。また、任意のFO2Pres文の有限モデルの大きさの集合(スペクトラム)がPresburger算術で定義可能であることを示す。