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_ 环境变量。

为什么选择这个工具包？

• 一个门面、七种动词，专为 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 会自行将这些公理添加为前提，这正是证明与虚假反模型的区别。注册表中的九条边都会声明其保留的性质（comorphism.GUARANTEES）、其像所需的侧公理，以及读取的选项；组合路径会报告其中最弱的保证。我们有意不在逻辑之间进行隐式强制转换——关于转换为何不是向上转型，请参阅逻辑之间的转换。
• 开箱即用的 MCP 服务。 执行 pip install unicode-logic-kit[mcp]，然后运行 python -m unicode_logic_kit.mcp（或者，在未安装任何内容时运行 uvx "unicode-logic-kit[mcp]" mcp），即可将工具包作为三十七个 Model Context Protocol 工具（23 个通用工具、6 个化学工具、8 个描述逻辑工具）提供——任何 MCP 客户端（Claude Code/Desktop、Agent 框架、编辑器）都能解析、证明、诊断和转换，无需编写 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 子句读回为工具包公式，以供模型检验。两种编码错误会产生精确率 1.00、却毫无意义的假设——学习器会跨示例合并的示例局部个体名称，以及每个谓词上的示例参数——这两种错误在输入和输出时都会被拒绝，而不是仅写在文档中。check_separation 会先问一个必须优先回答的问题：你的参考定义是否能区分这两组示例？
• 精确概率逻辑——不采样，不用浮点数。 prob.entailment_bounds 会以精确的最紧区间回答“P(bird)=0.9 对 P(fly) 有何蕴含？”，方法是对可能世界进行 Nilsson 概率蕴含的有理数线性规划，并包含条件概率；prob.query 则会根据 Sato 分布语义，对含有独立概率事实的确定子句程序回答 ProbLog 风格的查询——每个结果都是精确的 Fraction，每个不受支持的片段都会明确拒绝。
• 二十五种证明器后端，一个诚实的 Verdict。 工具包自带的演算与语义搜索（一阶归结——包含用于等式的可靠参数调换与重写，无需手动提供合同公理——、带有记录在案且可独立检查的证明对象的解析表方法、模态解析表、有限模型查找器、有界 Kripke 枚举、QML 嵌入）与 Z3、cvc5、Vampire、E、Zipperposition、Twee（等式证明在工具包报告之前会由独立检查器重新验证）、Prover9、Leo-III、Isabelle、nanoCoP-M（原生一阶模态逻辑，可选启用，并必须进行独立交叉检查），以及 Docker 化的 HETS 服务（CASL 导出并往返导入，保留原生多排序、发出多规范 DOL 库、通过一个名称调用 SPASS/darwin，并在每个 verdict 中提供共态射来源信息）同为一等公民。每条路径都会返回相同的 Verdict，其中包含语义状态（proved / refuted / unknown / error）、独立的为何无法得到更强结果维度（timeout ≠ bound_hit ≠ incomplete ≠ unsupported）、SZS 状态、运行时间，以及可转为 JSON 的见证。还提供链式调用、组合式证明（portfolio_prove，并行运行，设有一致性阈值，并在证明器意见不一致时发出可靠性警报），以及带缓存的批量运行（batch_decide）。
• 面向 NL→FOL 工作的评估工具箱。 提供分级等价阶梯（精确 → 规范化 → 词汇对齐 → 求解器，其中求解器级别有三态结果和部分评分）、AST 级符号对齐、标准公式自审，以及 FOLIO、MALLS、GROVES、WillowNLtoFOL、ProntoQA、ProofWriter、LogicNLI、ProverQA 和 FraCaS 的适配器——每种数据集的上游架构都经过源头验证，其局限性也会如实记录，而非掩盖。FraCaS 是纯 NLI 数据集：完全没有标准公式，因此翻译步骤由注入的可调用对象负责，工具包只负责判定。
• 能够自我解释的反模型。 api.countermodel 会返回机器可读的见证，并附有通俗易懂的说明（“反模型有 2 个可能世界。……在世界 0 中，公式不成立。”）；反驳功能也确实涵盖时态片段：Ⓕ P → P 会返回已反驳及双世界 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

一个解析器类 MSFLParser 可处理一阶、二阶和三阶经典逻辑，每种都可带或不带类型，也可带或不带模态系列（模态／时态／认知／道义／混合）：由三个构造标志控制的十二种组合。第四个标志 fuzzy 会在这十二种组合中分别以 Łukasiewicz 联结词替换二值联结词。除此之外，还有团队语义依赖／IF 逻辑、直觉主义线性逻辑和 Lambek 演算。 表层语法采用自然 Unicode 字符（∀ ∃ ∧ ∨ ¬ → ↔ ⊕ ⊗ □ ◇ @ ⊸ 𝟙 …），不提供 ASCII 替代写法。

AST 之上构建了完整的推理栈——四种证明方法（内置归结证明器、带检查器和搜索器的 Fitch 自然演绎、Gentzen 序列演算 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]" 会添加 cvc5，作为第二个进程内 SMT 后端（之后它会紧接 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 可复用 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。

这套包含七种动词的接口也可通过子命令编写脚本（--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 预印本， arXiv:2509.22338。

许可证

MIT