unicode-fol-kit 0.11.0

Parser and toolkit for first-order logic formulas using Unicode operators

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, many-valued, fuzzy, intuitionistic, second-order, description, and a range of 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 six modes (classical FOL, many-sorted FOL, many-sorted and single-sorted Łukasiewicz fuzzy logic, modal/temporal/epistemic/deontic, and second-order) 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

With a local Isabelle installed, the hol subpackage's shallow embeddings become proofs: isabelle_decide_modal / isabelle_decide_fol actually run the prover. 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