多項式時間決定可能性のk-否定断片に関する第一階理論

本論文は、特定の固定パラメータ処理可能性要件を満たす第一階理論の固定否定断片の多項式時間決定可能性を保証するための十分条件を提供する一般的な枠組みを紹介します。この枠組みを用いることで、任意の存在量化、同時、および固定数の否定記号を含む理論の文を多項式時間内に決定できるようになります。最近、NguyenとPakによって、より制限されたPresburger算術の断片（加算および順序を持つ整数の第一階理論）がNP困難であることが示されました。対照的に、我々の枠組みを適用することで、Presburger算術から順序関係を除き等式を優先する弱Presburger算術の固定否定断片が多項式時間内に決定可能であることを示します。