unicode-fol-kit

A Python toolkit for first-order logic with Unicode operators — parse, transform, and reason about formulas — with a reasoning layer that reaches well beyond classical FOL into modal, temporal, hybrid, many-valued, fuzzy, intuitionistic, relevant, second-order, description, dependence/IF, substructural, and a range of further non-classical logics.

from unicode_fol_kit import MSFLParser, is_valid

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

One parser class, MSFLParser, has nine modes (classical FOL, many-sorted FOL, many-sorted and single-sorted Łukasiewicz fuzzy logic, modal/temporal/epistemic/deontic/ hybrid, second-order, team-semantic dependence/IF logic, intuitionistic linear logic, and the Lambek calculus) selected by constructor flags, with natural Unicode surface syntax (∀ ∃ ∧ ∨ ¬ → ↔ ⊕ ⊗ □ ◇ @ ⊸ 𝟙 …) and no ASCII fallbacks.

On top of the AST sits a full reasoning stack — four proof methods (a built-in resolution prover, Fitch natural deduction with checker and searcher, the Gentzen sequent calculi LK/LJ, and analytic tableaux), a finite model finder, SMT (Z3) and external-prover (Prover9 / Vampire) backends, truth tables, and dedicated semantics for every logic. Formulas import/export to TPTP, Prover9, SMT-LIB, LaTeX, and JSON.

📖 Documentation

Full guide and API reference: https://unicode-fol-kit.readthedocs.io/

The documentation walks through every logic with runnable examples — start with the Quickstart and Choosing a tool.

Installation

pip install unicode-fol-kit

Requires Python 3.10+. Z3 ships with the package; Prover9, Vampire, and Isabelle are optional external tools you install separately to unlock the corresponding backends.

Logics at a glance

Logic	Enable / entry point	Decide / reason with
Classical FOL / MSFOL	`MSFLParser()` / `many_sorted=True`	resolution, Z3, Prover9/Vampire, tableaux, Fitch, LK, finite model finder
Fuzzy Łukasiewicz / Gödel / product	`MSFLParser(fuzzy=True)`	`fuzzy_evaluate`, `fuzzy_is_valid(…, tnorm=…)` (Z3 reals, quantifier grounding)
Modal / temporal / epistemic / deontic	`MSFLParser(modal=True)`	`satisfies_modal`, `standard_translation`, native `is_modal_valid` / `modal_decide` (K…S5, B, KD45)
Quantified modal	`KripkeModel(domains=…)`	`qml_is_valid` per domain regime + frame; THF / Isabelle export
Many-valued K3 / LP / Belnap FDE	`truth_table`, `semantics.matrix`	`matrix_is_valid` / `matrix_entails` over any finite `TruthMatrix`
Intuitionistic	`int_valid` / `int_countermodel`	propositional decision + bounded first-order Kripke search; LJ checker
Second-order	`MSFLParser(second_order=True)`	`satisfies_so`, bounded `so_is_valid_finite` / `so_find_countermodel`
Description logic ALC	`unicode_fol_kit.dl`	`concept_satisfiable` / `subsumes` / `abox_consistent` (tableau, TBox + ABox)
Free · public-announcement · counterfactual · circumscription	`semantics.free_logic` / `dynamic_epistemic` / `conditional` / `nonmonotonic`	dedicated evaluators and (non-monotonic) consequence
Hybrid H(@) (nominals, `@i φ`)	`MSFLParser(modal=True)`	`KripkeModel(nominals=…)`, `hybrid_is_valid` per frame (standard translation + Z3)
Relevant logic B	classical syntax + `semantics.relevant`	`rel_valid` / `rel_countermodel` (Routley–Meyer, bounded exhaustive search)
Dependence / IF (team semantics)	`MSFLParser(dependence=True)`	`team_satisfies` / `team_models` over finite structures
Linear logic (ILL) · Lambek calculus	`MSFLParser(linear=True)` / `lambek=True`	`ill_prove` (cut-free; complete for !-free) · `lambek_derivable` (decision procedure)

With a local Isabelle installed, the hol subpackage's shallow embeddings become proofs: isabelle_decide_modal / isabelle_decide_fol actually run the prover. The hol.deepshallow subpackage goes further, emitting — for propositional modal, intuitionistic, Lewis-conditional and relevant logic — the deep, maximal-shallow and minimal-shallow embeddings side by side with machine-checked faithfulness proofs between them (Benzmüller, arXiv:2502.19311), verified end to end by Isabelle. See the higher-order guide.

Building the documentation locally

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

Citation

If you use this toolkit in academic work, please cite the accompanying preprint:

@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.

License

MIT

Metadata

Release files for unicode-fol-kit 0.15.0

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for unicode-fol-kit 0.15.0
File	Size	Uploaded
unicode_fol_kit-0.15.0.tar.gz	716.6 kB	Jul 11, 2026	Details

Built distribution (wheel)

Table of built distributions (wheels) for unicode-fol-kit 0.15.0
File	Interpreter	ABI	Platform	Reset
unicode_fol_kit-0.15.0-py3-none-any.whl 369.2 kB Jul 11, 2026	Python 3	none	any	Details

Total release size: 1.1 MB

Release files / unicode_fol_kit-0.15.0.tar.gz

Download URL	unicode_fol_kit-0.15.0.tar.gz
Size	716.6 kB
Tags	Source
SHA-256 checksum How to use checksums	`89a197982c2160f00f0e0d80419ba295ae7f0515b015b6475d9ddde71e1a988d`
BLAKE2b-256 checksum How to use checksums	`724f4d5eb96431c029cd6168a472f9044977913941eab1f59084eab9b4d64f1a`
Upload date	Jul 11, 2026
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`twine/6.2.0 CPython/3.10.20`

Release files / unicode_fol_kit-0.15.0-py3-none-any.whl

Download URL	unicode_fol_kit-0.15.0-py3-none-any.whl
Size	369.2 kB
Tags	Python 3
SHA-256 checksum How to use checksums	`eefd2c0e8903c9a293d4e8923b964cd38f2bce7a49fae9b5736e33890f703ef5`
BLAKE2b-256 checksum How to use checksums	`b47a5a0aa96a7a69141b8773c6dd1abd0802afdad9c70e3364672bc4de5df579`
Upload date	Jul 11, 2026
Uploaded using Trusted Publishing? What is trusted publishing?	No
Uploaded via	`twine/6.2.0 CPython/3.10.20`