証明論の可視化とゲンツェンのカット除去定理

Toy Hauptsatz は、古典命題論理の証明探索プロセスを視覚的に再現するクライアントサイドの論理エンジンです。論理式をLispのS式にコンパイルし、優先度付きキューによる自動推論（Modus Ponens）を行って、前提からターゲットに至る自然演繹のステップを鮮やかなツリー構造で可視化します。背景となる理論として、ゲルハルト・ゲンツェンのカット除去定理（Hauptsatz）がもたらす「部分論理式特性」を利用しており、有限の探索空間で効率的かつ完全な証明探索が完了する仕組みを直感的に学ぶことができます。