Core Concepts
理論の組み合わせにおける様々な性質の組み合わせを分析し、可能な組み合わせと不可能な組み合わせを特徴付けた。特に、最小モデルの計算可能性に着目し、他の性質との関係を明らかにした。
Abstract
本論文は、Satisfiability Modulo Theories (SMT) における理論の組み合わせに関する研究の一環である。以前の研究では、7つの性質(凸性、安定無限性、滑らかさ、有限証拠可能性、強有限証拠可能性、有限モデル性、安定有限性)が分析されていた。しかし、最小モデルの計算可能性という重要な性質は未だ分析されていなかった。
本論文では、この最小モデルの計算可能性とその他の性質との関係を明らかにする。具体的には、以下のような結果を示した:
有限モデル性と最小モデルの計算可能性は、有限証拠可能性を含意する(定理4)。
空シグネチャの滑らかな理論は、最小モデルの計算可能性を持つ(定理5)。
任意のシグネチャにおいて、ある種の安定無限性の欠如は最小モデルの計算可能性を意味する(定理6)。
1ソート理論や2ソート理論などの特殊な場合でも、同様の結果が成り立つ(定理7, 8)。
さらに、これらの結果を踏まえて、可能な性質の組み合わせと不可能な組み合わせを完全に特徴付けた(定理3)。この結果は、理論の組み合わせ手法を適用する際の指針となる。
Stats
任意の量化子自由式φに対して、最小モデルの集合minmodT,S(φ)は有限集合である。(命題1)
量化子自由式φがT-満足可能ならば、minmodT,S(φ)は φを満たすT-解釈の最小要素集合である。(命題2)
理論Tが有限モデル性を持つならば、minmodT,S(φ)の要素はすべて自然数である。(命題3)
理論Tが安定有限性を持つならば、minmodT,S(φ)の要素はすべて自然数である。(命題3)
Quotes
"最小モデルの計算可能性という重要な性質は未だ分析されていなかった。"
"理論の組み合わせ手法を適用する際の指針となる。"