1 矛盾検出の基本
1.1 用語と概念
1.1.1 矛盾（不整合）と偽の導出
矛盾（不整合）とは、ある前提群のもとで、論理的に同時成立し得ない結論が導かれる状態を指す。典型的には、前提から「偽」または同値な形式的矛盾（例：恒真でない特定の命題の導出）が引き出せるかどうかで判定する。表現上は、矛盾を直接に「偽」として扱う流儀と、矛盾に至る演繹の存在を否定できないこととして扱う流儀がある。
1.1.2 充足可能性と矛盾の関係
充足可能性とは、与えられた条件（制約・論理式）を同時に満たす解（解釈・変数割当）が存在するかを問う性質である。一般に、集合として充足不能であれば矛盾があると見なせる。逆に、充足可能であれば少なくとも一つの整合的な解釈が存在するため、形式体系の範囲では不整合の否定が成立する。
1.1.3 一貫性（整合性）という考え方
一貫性（整合性）は、前提群が互いに衝突せず、矛盾が生じないことを総称する概念である。実務では「矛盾がない」ことは単なる理論的な性質にとどまらず、仕様が満たすべき性質の保持や、推論エンジンの出力が意味を失わないことの保証として位置づけられる。
1.2 対象と入出力
1.2.1 形式的知識（論理式・制約）の表現
矛盾検出は、入力として形式的に記述された知識を対象とする。命題や述語の論理式、ルール体系、条件付き制約、背景理論（整数、順序、データ構造など）を含むことが多い。表現形式は、扱える推論能力や計算可能性に強く影響するため、問題領域に合わせて選択される。
1.2.2 出力の種類（判定・証明・原因）
出力は目的に応じて段階化されることが多い。まず「矛盾がある／ない」という判定が基本である。次に、矛盾がある場合にその根拠となる証明（反駁可能な導出系列、または証明不能性の根拠）が出力されることがある。さらに実務上重要な出力として、どの条件が衝突しているかの原因候補（集合の特定、最小化された原因集合、反例の構成）が挙げられる。
1.3 関連領域との位置づけ
1.3.1 自動定理証明との関係
自動定理証明は、所望の結論を前提から導くことを中心課題とする。矛盾検出はこれと対照的に、「導けてしまう矛盾の有無」や「充足不能性」を捉える点で位置づけられる。ただし実際には、矛盾検出は証明探索と強く結びつき、矛盾が導出されれば証明に相当し、充足不能性の示唆は反証または導出の欠如として扱われることもある。
1.3.2 検証・診断との関係
検証は、仕様が期待する性質を満たすかを確認する工程であり、矛盾検出は整合性の検査に直結する。診断は、検証で検出された不整合の原因を絞り込むことを主眼とするため、最小矛盾集合（いわゆる診断用の根拠）を抽出する手法と密接に関連する。
2 形式論理における矛盾検出
2.1 古典論理での判定
2.1.1 整合性判定としてのアプローチ
古典論理の枠組みでは、前提集合が整合的（充足可能）であるかを中心に捉える方法が一般的である。整合でない場合は、どこかに偽を導く経路が存在する。したがって、矛盾検出は「充足可能性の判定」と「矛盾導出の可能性」を相互に対応づけて扱える。
2.1.1.1 満足不能性（Unsatisfiability）の判定
満足不能性の判定は、与えられた論理式群を同時に満たす割当が存在しないことを示す。これにより「矛盾がある」という主張が形式的に裏打ちされる。判定が真になるだけでなく、その事実を支える証明オブジェクトが得られると、外部のチェック機構で再検証できる。
2.1.2 反例探索と矛盾の検証
反例探索は、充足可能性の観点で「満たす割当」を探索する過程として理解できる。探索が成功すれば整合的であることが分かり、探索が失敗し、さらに失敗の理由が正当化できれば満足不能として矛盾を確認できる。反例の具体化は、原因の推定にも役立つ。
2.2 推論規則による検出
2.2.1 消去法（解消原理など）の考え方
消去法は、推論規則を用いて中間式を整理しながら、矛盾を導くか、ある形での矛盾が現れないことを示す考え方である。解消原理のような枠組みでは、与えられた節集合から節を組み合わせて新しい節を生成し、空節に相当するものが得られれば矛盾があると結論できる。こうした手続きは、構造化された計算機実装に適している。
2.2.2 導出（演繹）による矛盾検出
演繹による検出は、前提から順に推論規則を適用し、矛盾に相当する結論（例：偽、または明確な不整合命題）が現れるかを追跡する。矛盾が出現するなら、その導出列が根拠となる。逆に導出列を十分に探索しても矛盾に至らない場合は、体系と探索範囲に依存しつつ、整合の見込みを得る段階的な情報になる。
2.3 モデル理論的観点
2.3.1 モデルの存在と矛盾
モデル理論では、与えられた論理式が真になる解釈（モデル）が存在するかどうかで性質を捉える。モデルが存在すれば矛盾はないと判断でき、モデルが存在しないことが証明できれば充足不能として矛盾が確定する。直観的には「言明が同時に成立する世界があるか」が焦点となる。
2.3.2 論理式の分類（充足可能か否か）
論理式（または制約集合）は、充足可能／満足不能に分類される。さらに計算論の観点では、充足不能である場合に証明をどれだけ効率よく構成できるか、充足可能である場合に反例（充足解）をどれだけ早く見つけられるかが重要になる。分類は問題の難度推定や、選択する計算戦略の指針になる。
3 計算モデルとアルゴリズム
3.1 SAT/SMT による手法
3.1.1 SAT（命題論理）での矛盾検出
SAT（充足可能性判定問題）は、命題変数への真偽割当が論理式を満たすかを問う枠組みである。矛盾検出は「満たす割当が存在しない」ことの確認に対応する。実装では、探索過程で部分的な割当を更新し、不整合が局所的に判明した時点で枝を切る。結果として、満足不能なら矛盾証明（形式的根拠）が得られる構成が採られることが多い。
3.1.2 SMT（述語論理・理論組込み）での矛盾検出
SMTは、命題骨格に加えて、数値や順序、配列などの「背景理論」を組み込んだ制約を扱う。矛盾検出では、論理式の一部が変数領域の制約と矛盾する場合、その矛盾が理論ソルバの計算で検出され、上位の探索へフィードバックされる。これにより、単純な命題論理よりも表現力の高い整合性検査が可能になる。
3.1.3 付随情報（矛盾証明、原因候補）
SAT/SMTの実務的価値は判定だけではなく、説明可能性にもある。矛盾証明は、なぜ満足不能なのかを機械的に検証可能な形で示すものである。原因候補は、どの制約が衝突している可能性が高いかを抽出する情報で、診断や修正支援に直結する。
3.2 制約充足としての定式化
3.2.1 制約表現と整合性
矛盾検出を制約充足問題として捉えると、整合性とは「全制約を同時に満たす解があるか」という問いになる。制約は線形、非線形、離散、連続と多様であり、表現方法（係数の扱い、論理接続の分解、補助変数の導入など）は計算効率に影響する。整合性を保つためには、制約の形式化の段階で曖昧さを排除することが重要になる。
3.2.2 近似・ヒューリスティクスの利用
制約の全探索が高コストになる領域では、近似やヒューリスティクスが利用される。例えば、不整合が起きやすい制約から優先して評価する、探索順序を推定する、局所的な矛盾の兆候を手がかりに枝を抑えるといった方針がある。近似は「必ず正しい」ことより「早く有用な情報を得る」ことを目的にするため、結果の扱い（確証と暫定の区別）が設計段階で決められる。
3.3 計算量と実用上の工夫
3.3.1 計算複雑性の見取り図
矛盾検出は、理論の表現力が上がるほど難度が増えやすい。命題論理の満足不能性は計算複雑性の観点で一般に高い計算負荷を持つ一方、実際の問題は構造や制約の偏りによって現実的に解ける場合が多い。したがって、理論的な上界と、実例に基づく平均的性能を併せて理解する必要がある。
3.3.2 実装上の最適化（枝刈り・学習）
実装では、探索の無駄を減らす工夫が中心になる。枝刈りは、不整合が判明した時点でそれ以降の探索を打ち切る仕組みである。学習は、衝突から得られる情報を次の探索判断に転用し、同種の失敗を繰り返さないようにする。さらに、繰り返し呼び出しを前提にしたキャッシュ、前処理による簡約、ソルバ内部の戦略切替なども組み合わされる。
4 原因特定と応用
4.1 最小矛盾集合（診断）
4.1.1 矛盾原因の抽出
最小矛盾集合は、与えられた条件のうち矛盾を引き起こす核となる部分集合を求める考え方である。目的は「全条件を眺めても分からない衝突点」を特定し、修正の対象を絞ることにある。抽出手法では、候補集合を繰り返し再チェックしながら削除可能性を評価するため、計算量と説明の粒度の間にトレードオフが生まれる。
4.1.2 最小化と近似の考え方
最小性には複数の定義があり得る。厳密な最小は探索が難しくなるため、実務では「近似最小」や「十分に小さい原因集合」の抽出が選ばれることがある。近似は、修正の意思決定を速める利点と、原因の完全性が保証されないリスクを併せ持つ。したがって、成果物の性質（厳密か、包含関係での最小か、上限サイズの保証があるか）を明示する運用が望ましい。
4.2 矛盾の解消・修正支援
4.2.1 ルールの優先度や例外の導入
矛盾を解消するには、矛盾を作っている条件を弱める、強める、あるいは例外構文で吸収する方法がある。優先度付けは、同時に適用されるルールの競合に順序を与えることで実行時の解釈を定める。例外導入は、例外条件の追加により「通常は適用されるが特定条件では適用しない」領域を明確化し、衝突の再発を抑える。修正案は形式的な再検証を伴うことで信頼性が増す。
4.2.2 仕様のリライトと整合性維持
仕様リライトは、表現の変更によって矛盾を回避しつつ、意図した要求を保つ試みである。例えば、暗黙の前提を明示化し、曖昧な制約を等価な明確条件へ置き換えることがある。整合性維持の観点では、変更後に再度矛盾検出を走らせ、回避した矛盾が他の要件を損なっていないかを確認するプロセスが重要になる。
4.3 応用分野
4.3.1 ソフトウェア検証
ソフトウェア検証では、プログラムの挙動が仕様と一致するかを確かめるために矛盾検出が使われる。例えば、関数の契約（前提・事後条件）、ループ不変条件、型や情報フローの制約などを論理式へ写像し、矛盾が生じないことを確認する。矛盾が検出された場合は、バグの兆候や契約の過不足が示される。
4.3.2 論理プログラミング
論理プログラミングでは、ルールと事実の組が矛盾していないことが推論の健全性に関わる。矛盾があると、導出の意味が失われたり、到達可能性が破綻したりする。矛盾検出は、ルール集合の整合確認、探索の途中での不可能性の早期判定、さらにはデバッグの手がかりとして利用される。
4.3.3 組合せ最適化や意思決定支援の検査
組合せ最適化や意思決定支援では、制約が競合して成立しない選択肢が混ざり得る。矛盾検出により、制約体系が無理な前提を含んでいないかを事前に検査できる。実行計画やスケジュールの生成では、満足不能が判明した段階で代替案の生成に移る設計が採られ、結果として計算資源の節約と運用の安定化につながる。