計算可能性とチューリングマシン

「計算とは何か」を抽象機械で定式化し、判定問題の解法と難しさを論じる分野。論理と代数的手法（有限体上のグレブナー基底）に橋を架ける。

チューリングマシン

アラン・チューリングが計算可能性のために考案した抽象機械 (1936)。両方向無限のテープ・ヘッダ・制御器からなり、形式的には
$M=(Q,\Sigma ,\Gamma ,q_0,A,\delta ),\delta :Q\times \Gamma \to Q\times \Gamma \times \{L,R\}$
で与えられる。状態遷移図で動作を表現でき、あらゆる「計算」を TM の動作に還元できる（万能性）。

神託機械

特定の決定問題を 1 ステップで答えるブラックボックス（オラクル）を付けた TM が神託機械。停止性問題を解くオラクルを仮定することもでき、多項式階層の議論に繋がる。無作為に一貫した値を返すランダムオラクルは理想的な一方向関数として暗号の安全性証明（ランダムオラクル仮定）で使われる。

充足可能性ソルバ

• SAT：ブール式の充足可能性問題。現代のソルバは DPLL を基礎にする。
• SMT（Satisfiability Modulo Theories）：値がブールでなくなった拡張。SAT が命題論理、SMT が一階述語論理に対応。Microsoft z3 が有名（Julia バインディングあり）。充足判定を二分探索すれば最適化問題が解ける。

代数的・組合せ的手法

• グレブナー基底（Buchberger アルゴリズム）：多値論理を多項式で表して判断推理を解いたり、有限体 ${\mathbb{F}}_{p^m}$ 上の算術回路の形式検証（等価性判定）に使われる。逆トポロジカル順序での基底導出でバグを含む回路でも検証を完了できる、という論文がある。
• Schwartz–Zippel の補題：誤った多項式はランダム評価点で高確率に異なる値を返す（恒等性検査の基礎）。
• Chordal Graph（弦グラフ、木の同型判定）、マトロイド、有限体上の行列簡約の計算量など組合せ最適化の話題。

関連: mathematical-logic / galois-theory / np-complexity-classes / _moc-math