Unicode Logic Kit

unicode-logic-kit

Unicode 演算子を使った論理のための Python ツールキットです。古典一階述語論理をはるかに超えた、様相論理、時相論理、ハイブリッド論理、多値論理、ファジィ論理、直観主義論理、関連論理、二階・三階論理、記述論理、依存性／IF 論理、部分構造論理、その他さまざまな非古典論理の論理式を、解析、変換、推論できます。さらに、自然言語から論理への研究を支える基盤も備えています。検証ループから呼び出せる小さな API、十数種類の証明器で共通して使える判定型、ベンチマークの正解データと照合して LLM 生成の論理式を採点する評価ツールボックスを提供します。

from unicode_logic_kit import MSFLParser, is_valid

phi = MSFLParser().parse(
    "∀x (Human(x) → Mortal(x)) ∧ Human(socrates) → Mortal(socrates)")
print(is_valid(phi))   # True

0.31.0 で名称を変更しました。 0.30.0 まで、このパッケージの名前は unicode-fol-kit でした（import unicode_fol_kit）。一階述語論理は、このパッケージが扱う論理の一つであり、すべてではありません。pip install -U unicode-fol-kit は引き続き動作し、このパッケージをインストールして、古いインポート名を DeprecationWarning とともに引き継ぎます。ただし、新しいコードでは pip install unicode-logic-kit と import unicode_logic_kit を使用してください。UFK_ 環境変数を含め、それ以外の名前に変更はありません。

このキットを選ぶ理由

• 1 つのファサード、7 つの動詞、LLM のループ向けに構築されています。 api.parse_any（Unicode／TPTP／LaTeX／Prover9／SMT-LIB の方言を自動検出します。例外は発生させず、各パーサーの異議をすべて記録します）、api.check（適切な形式かどうかとシグネチャへの適合性を確認し、「もしかして」の候補を提示します）、api.equivalent、api.prove、api.countermodel、api.repair（診断→提案→修正を行うジェネレーターで、修正コールバックはお使いの LLM です）、api.translate（コモルフィズムレジストリを介して論理間を変換します）。すべての結果は JSON 互換の to_dict() を備え、API には明示的な安定性ポリシーがあります。
• 値としての論理と、側条件を伴う変換。 FOL(MSFOL(f)) はソート付き論理式を変換し、その側公理（各ソートは空でないこと、各ソート付き定数はそのソートに属すること）を項とともに Sentence として保持します。api.prove はそれらを前提として自動的に追加します。これが、証明と誤った反例モデルとの違いです。レジストリの 9 つのエッジはそれぞれ、何を保持するか（comorphism.GUARANTEES）、イメージに必要な側公理、読み取るオプションを宣言します。合成された経路では、その経路における最も弱い保証が報告されます。意図的に、論理間の暗黙的な型強制はありません。変換がアップキャストではない理由については、論理間の変換をご覧ください。
• すぐに使える MCP サーバー。 pip install unicode-logic-kit[mcp] を実行し、続いて python -m unicode_logic_kit.mcp を実行するか、何もインストールせずに uvx "unicode-logic-kit[mcp]" mcp を実行すると、このツールキットが 37 個の Model Context Protocol ツール（汎用 23 個、化学向け 6 個、記述論理向け 8 個）として公開されます。任意の MCP クライアント（Claude Code/Desktop、エージェントフレームワーク、エディター）から、Python を書かずに解析、証明、診断、変換を実行できます。修復ループは自然に逆向きに動作し、クライアント側の LLM が修正器になります。エラー分析レイヤーも含まれています。シンボル差分を含む予測と正解の比較（compare_formulas）、コーパスメトリクス（score_batch）、モデル証人を伴う前提集合の充足可能性判定（check_consistency）、正規形、構文間レンダリング、真理値表、シグネチャ抽出、談話現象向けの DRS→FOL などを利用できます。
• モデル発見だけでなく、実際の構造に対するモデル検査。 分子、知識グラフの近傍、シーングラフといった構造が与えられている場合、定義がその構造で成り立つかどうかを問えます。FiniteStructure と evaluate_in_structure が直接それに答えます。前置形も CNF も不要です（どちらも別の箇所でタイムアウトの原因として説明されています）。量化子の対象は領域全体ではなくインデックス付きの候補集合で、個数限定量化子は展開せずに数えられます。また、構造上では決定可能でもその構造上の一階論理では定義できない性質（連結性、環への所属）を、計算述語として使用できます。unicode_logic_kit.chem は SMILES 文字列を ChemLog シグネチャ上のこのような構造に変換します。
• 両方向のルール学習と、見逃されがちな失敗の可視化。 unicode_logic_kit.ilp は同じ構造を ILP タスク（Popper の bk.pl／exs.pl／bias.pl）に変換し、学習された Prolog 節をキットの論理式として読み戻すので、モデル検査を実行できます。2 つのエンコードミスは、適合率 1.00 なのに何の意味もない仮説を生みます。学習器が例をまたいで結び付ける、例ごとに異なる個体名と、すべての述語に付ける例の引数です。この 2 つは文書で注意喚起するだけでなく、変換時と読み戻し時の両方で拒否されます。check_separation は、最初に問うべきこと、つまり参照定義が 2 つの例集合をそもそも分離できるかを確認します。
• 厳密な確率論理 — サンプリングなし、浮動小数点数なし。 prob.entailment_bounds は「P(bird)=0.9 から P(fly) について何が導かれるか」という問いに、厳密で最も狭い区間で答えます（条件文を含む、可能世界上の有理数線形計画法による Nilsson の確率的含意）。prob.query は Sato の分布意味論に従い、独立した確率的事実を含む確定プログラムに対して ProbLog 形式のクエリに答えます。結果はすべて厳密な Fraction で返され、サポートされないフラグメントは明示的に拒否されます。
• 25 種類の定理証明バックエンド、誠実な Verdict は 1 つ。 キット独自の計算体系と意味論的探索（分解法 — 等号に対する健全なパラモジュレーション／デモジュレーションを備え、手動で合同性公理を与える必要はありません —、記録され個別に検証可能な証明オブジェクトを備えた解析的タブロー、様相タブロー、有限モデルファインダー、有界 Kripke 列挙、QML 埋め込み）は、Z3、 cvc5、Vampire、E、Zipperposition、Twee（等式証明はキットが報告する前に独立したチェッカーで再検証されます）、Prover9、Leo-III、Isabelle、nanoCoP-M（ネイティブな一階様相論理で、オプトイン時には独立したクロスチェックが必須です）、Docker 化された HETS サーバー（ネイティブな多ソート性を備えた CASL のエクスポートと往復インポート、複数仕様の DOL ライブラリ出力、1 つの名前での SPASS／darwin、すべての判定結果におけるコモルフィズムの由来情報）と並ぶ第一級の機能です。すべての経路は、意味論上のステータス（proved／refuted／unknown／error）、独立した「これ以上の結果にならなかった理由」の軸（timeout ≠ bound_hit ≠ incomplete ≠ unsupported）、SZS ステータス、実時間、JSON 化可能な証人を含む、同じ Verdict を返します。チェーン、ポートフォリオ（portfolio_prove。合意しきい値を用いて並列実行し、証明器間の不一致に対する健全性アラームを備えます）、キャッシュされたバッチ実行（batch_decide）も、この上に構築されています。
• NL→FOL 作業向けの評価ツールボックス。 段階的な同値性評価（厳密一致→標準化→語彙整合→ソルバー。ソルバーレベルは三値で、部分点にも対応）、AST レベルのシンボル整合、正解論理式の自己監査、FOLIO、MALLS、GROVES、WillowNLtoFOL、ProntoQA、ProofWriter、LogicNLI、ProverQA、FraCaS 向けアダプターを備えています。それぞれ、上流スキーマを原典で検証し、制約を取り繕わずに文書化しています。FraCaS は純粋な NLI 形式で、正解論理式がありません。そのため、変換ステップには注入可能な呼び出し可能オブジェクトを使い、キットは判定のみを行います。
• 自らを説明する反例モデル。 api.countermodel は、機械可読な証人に加えて平易な英語による説明（「反例モデルには 2 つの可能世界があります。… 世界 0 では論理式が成り立ちません。」）を返します。反証は時間論理フラグメントにも対応しており、Ⓕ P → P は「unknown」ではなく、2 世界の Kripke 証人とともに反証されます。
• 誠実さを契約として保証。 どの経路も、暗黙のうちに機能を低下させることはありません。あいまいな入力は古典論理の証明器で単純化されずに拒否され、利用できないバックエンドはチェーンから黙って消えるのではなく例外を発生させます。不完全な手法は停止した理由を報告し、すべての証明手法には独立したチェッカーがあります。

from unicode_logic_kit import api

result = api.parse_any("∀x (Raven(x) → Black(x))")     # LLM output, any dialect
report = api.check(result.formula,
                   signature={"predicates": {"Raven": 1, "Black": 1}})
verdict = api.prove(api.parse_any("Black(tweety)").formula,
                    premises=[result.formula,
                              api.parse_any("Raven(tweety)").formula])
print(verdict.status, verdict.backend, verdict.szs_status)  # proved z3 Theorem

1つのパーサークラス MSFLParser が、1階、2階、3階の古典論理を読み取ります。それぞれにソートを付けるかどうか、また様相系（様相／時制／認識／義務／ハイブリッド）を付けるかどうかを選べます。コンストラクターの3つのフラグによる組み合わせは12通りです。さらに4つ目のフラグ fuzzy を指定すると、12通りのそれぞれで二値論理演算子の代わりに Łukasiewicz の論理演算子を使います。これらに加え、チーム意味論に基づく依存／IF 論理、直観主義線形論理、ラムベック計算を利用できます。 表層構文は自然な Unicode（∀ ∃ ∧ ∨ ¬ → ↔ ⊕ ⊗ □ ◇ @ ⊸ 𝟙 …）で、ASCII への代替表記はありません。

AST の上には、完全な推論スタックが構築されています。4つの証明手法（組み込みの解消法証明器、チェッカーと検索器を備えたフィッチ式自然演繹、ゲンツェンのシークエント計算 LK／LJ――後者は Dyckhoff の G4ip によって支えられており、命題直観主義論理に対する真の停止性を持つ決定手続きです――および解析的タブロー）、有限モデル探索器、SMT（Z3）および外部証明器（Prover9／Vampire）バックエンド、真理値表、そしてすべての論理に対応する専用の意味論が揃っています。すべての証明手法に独立したチェッカーがあります。これには、独自の一からの単一化処理で外部生成された解消導出（パラモジュレーションのステップを含む）を検証する check_resolution_proof や、独自の置換および δ の新鮮性チェックを用いて、記録されたタブローのすべての α／β／γ／δ ステップを再導出する check_tableau_proof が含まれます。 数式は TPTP（parse_tptp_problem によるヘッダーの Status／Rating メタデータを含む）、Prover9、SMT-LIB、LaTeX、JSON との間でインポート／エクスポートできます。

📖 ドキュメント

完全なガイドと API リファレンス：https://unicode-logic-kit.readthedocs.io/

ドキュメントでは、実行可能な例を使ってすべての論理を解説しています。まずは クイックスタートと ツールの選び方をご覧ください。

数式の判定にとどまらず、以下も利用できます。 モデル検査 （分子を含め、すでに用意されている構造で数式を評価します）、 検証 （定義の集合に整合性があるか、それとも簡単に満たされすぎるかを調べます）、 確率論理 （サンプリングなしで厳密な範囲とクエリを扱います）、そして MCP （文法も含めたツールキットを、言語モデル向けのツールとして利用できます）。

インストール

pip install unicode-logic-kit

Python 3.10 以降が必要です。Z3 はパッケージに同梱されています。pip install "unicode-logic-kit[cvc5]" を実行すると、2つ目のインプロセス SMT バックエンドとして cvc5 が追加されます（追加後はデフォルトの証明チェーンで Z3 の直後に加わります）。[mcp] は MCP サーバー（python -m unicode_logic_kit.mcp）を追加し、[hf] は HuggingFace の evaluate メトリックラッパーを追加します。[owl] は owlready2 を追加するため、dl.owl_reasoner から記述論理の問題を HermiT に渡して解決できます（PATH 上に JVM が必要です）。また、内蔵のタブローが名前を挙げて対応を拒む逆ロールやノミナルも判定できます。なお、owlready2 は LGPL-3.0-or-later でライセンスされており、MIT ライセンスのこのキットとは異なります。Prover9、Vampire、E、Zipperposition、Twee、nanoCoP-M（独自の ECLiPSe／SWI-Prolog のインストールが必要です。$UFK_NANOCOP_CMD）、Isabelle は、対応するバックエンドを利用するために別途インストールする任意の外部ツールです。また、HETS バックエンドには Docker が必要です（docker pull spechub2/hets:latest を実行してください。実行中のサーバーは localhost:8000 または $UFK_HETS_URL から検出されます）。各ツールは明示的に検出され、利用できない場合は、ひそかに表示から消えるのではなく、利用不可として報告されます。

論理の概要

論理	有効化／エントリーポイント	決定／推論方法
古典 FOL / MSFOL	MSFLParser() / many_sorted=True	分解法、Z3、Prover9/Vampire、タブロー、Fitch、LK、有限モデル探索
ファジー Łukasiewicz / Gödel / product	MSFLParser(fuzzy=True)	fuzzy_evaluate、fuzzy_is_valid(…, tnorm=…)（Z3 の実数、量化子のグラウンディング。Łukasiewicz と Gödel のみ対応 — product t-norm は評価のみ対応し、fuzzy_is_valid は名称を指定すると拒否します）；古典的な処理経路（is_valid、標準形、分解法）は、ファジー入力を暗黙に古典論理へ変換せず拒否します。明示的に to_fol(node) を指定してください
ファジー様相論理、二階論理、三階論理	MSFLParser(fuzzy=True, modal=True)、second_order=True、third_order=True	satisfies_fuzzy_modal（重み付き辺、定数領域上の量化子）、fuzzy_modal_search（最大 n 個の世界を持つ反例モデル。妥当性の証明は行いません）；fuzzy_evaluate と fuzzy_is_valid で、∀P / ∃P をファジー解釈上の厳密な下限／上限として扱います；三階原子は文字として指定するか、functionals= で計算します
様相論理／時相論理／認識論理／義務論理	MSFLParser(modal=True)	satisfies_modal、standard_translation、ネイティブの is_modal_valid / modal_decide（K…S5、B、KD45）
量化様相論理	KripkeModel(domains=…)	領域の条件とフレームごとの qml_is_valid；THF / Isabelle へのエクスポート
多値論理 K3 / LP / Belnap FDE	truth_table、semantics.matrix	任意の有限 TruthMatrix に対する matrix_is_valid / matrix_entails。THF/Isabelle へのエクスポートを含みます
直観主義論理	int_valid / int_countermodel	命題論理の決定手続き（int_prove/int_decide、G4ip）＋有界一階 Kripke 探索；LJ チェッカー
二階論理	MSFLParser(second_order=True)	satisfies_so、有界版 so_is_valid_finite / so_find_countermodel
三階論理（様相論理を含む）	MSFLParser(third_order=True[, modal=True])	引数が性質である述語（Pos(G)、Pos(λx. ¬G(x))）；理論全体からスロットの型を推論；to_thf_to / to_isabelle_to と浅い様相埋め込み hol.ho_modal；hol.goedel は Gödel の存在論的論証を双方向に検証します
記述論理 ALCHQ	unicode_logic_kit.dl	concept_satisfiable / subsumes / abox_consistent（タブロー、TBox + ABox、ロール階層＋推移的ロール、単純ロール上の限定数制約 AtLeast/AtMost）；parse_concept/parse_gci/parse_manchester と concept_to_fol/kb_to_fol/tbox_to_fol/rbox_to_fol/abox_to_fol は一階論理の証明器（数制約の Z3 による Count 展開）と Isabelle/THF エクスポートを再利用します
自由論理・公開告知・反事実条件文・最小化	semantics.free_logic / dynamic_epistemic / conditional / nonmonotonic	free_is_valid/free_entails（有界探索）；[φ!]ψ/⟨φ!⟩ψ は様相モードで解析され、reduce_announcements で決定されます；Lewis の V / VW / VC に対する cf_valid（centering=、デフォルトは弱中心化）；minimal_entails と非有界の circumscription_entails_so
ハイブリッド論理 H(@)（ノミナル、@i φ）	MSFLParser(modal=True)	KripkeModel(nominals=…)、フレームごとの hybrid_is_valid（標準翻訳＋Z3）
関連性論理 B	古典論理の構文＋semantics.relevant	rel_valid / rel_countermodel（Routley–Meyer、有界網羅探索）；isabelle_decide_relevant が両方向を認証します
依存関係論理／IF（チーム意味論）	MSFLParser(dependence=True)	有限構造上の team_satisfies / team_models；dependence_to_eso はガード付き／スラッシュ付き文の断片を ESO に変換し、satisfies_so / Isabelle エクスポートで利用できます
線形論理（ILL、⊤/𝟘 を含む）・Lambek 計算	MSFLParser(linear=True) / lambek=True	ill_prove（カットなし；! を含まない式では完全）・lambek_derivable（決定手続き）；どちらの導出も機械検証済み Isabelle 補題として再実行できます
ローカルに Isabelle がインストールされている場合、hol サブパッケージの浅い埋め込みは
証明になります。isabelle_decide_modal / isabelle_decide_fol / isabelle_decide_relevant
は実際に証明器を実行し、hol.isabelle_substructural は Python が見つけた
ILL/Lambek の導出を、機械検査済みの補題として再生します。hol.deepshallow サブパッケージでは
さらに、命題モーダル論理、直観主義論理、Lewis 条件法論理、関連論理に加え、Tier 2 の量化フラグメント
（K フレーム、定領域、様相 □/◇ のみ）について、深い埋め込み、最大浅埋め込み、最小浅埋め込みを
並べて出力し、それらの間の機械検査済み忠実性証明も生成します（Benzmüller、
arXiv:2502.19311）。すべて Isabelle によってエンドツーエンドで検証されます。
高階論理ガイドを参照してください。

コマンドライン

python -m unicode_logic_kit "∀x P(x)" --to latex

--mode はパーサーの方言（fol（デフォルト）、msfol、msfl、fl、modal、 second_order、dependence、linear、lambek）を選択し、--to は出力形式（tree、 unicode、latex、tptp、prover9、json、dot）を指定します。

7 つの動詞からなるファサードは、サブコマンドからもスクリプトで実行できます（機械可読な出力には --json を指定します。終了コードには判定結果が反映されます）。

python -m unicode_logic_kit prove "Ⓕ P → P" --dialect modal
python -m unicode_logic_kit check "∀x (Human(x) → Mortal(x))" --json

さらに equiv、countermodel、repair、translate も利用できます。

インストール後は、同じコマンドラインを unicode-logic-kit （unicode-logic-kit prove "Ⓕ P → P" --dialect modal）というコマンドで利用でき、 unicode-logic-kit mcp で MCP サーバーを起動できます。

ドキュメントをローカルでビルドする

pip install -e ".[docs]"
sphinx-build -b html docs docs/_build/html

引用

このツールキットを学術研究で使用する場合は、付属のプレプリントを引用してください。

@misc{vossel2025advancingnaturallanguageformalization,
      title={Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs},
      author={Felix Vossel and Till Mossakowski and Björn Gehrke},
      year={2025},
      eprint={2509.22338},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
      url={https://arxiv.org/abs/2509.22338},
}

Vossel, F., Mossakowski, T., & Gehrke, B. (2025). Advancing Natural Language Formalization to First Order Logic with Fine-tuned LLMs. arXiv preprint arXiv:2509.22338.

ライセンス

MIT