Metadata-Version: 2.4
Name: unicode-fol-kit
Version: 0.13.0
Summary: Parser and toolkit for first-order logic formulas using Unicode operators
Project-URL: Documentation, https://unicode-fol-kit.readthedocs.io/
Project-URL: Repository, https://github.com/fvossel/unicode-fol-kit
Project-URL: Issues, https://github.com/fvossel/unicode-fol-kit/issues
Author-email: Felix Vossel <felixvossel@gmail.com>
License: MIT
License-File: LICENSE
Keywords: first-order-logic,fol,lambda-calculus,logic,lukasiewicz,parser
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Scientific/Engineering
Requires-Python: >=3.10
Requires-Dist: lark>=1.1
Requires-Dist: z3-solver>=4.12
Provides-Extra: docs
Requires-Dist: furo>=2024.1.29; extra == 'docs'
Requires-Dist: myst-parser>=2.0; extra == 'docs'
Requires-Dist: sphinx>=7.0; extra == 'docs'
Provides-Extra: test
Requires-Dist: pytest-xdist>=3.0; extra == 'test'
Requires-Dist: pytest>=7.0; extra == 'test'
Description-Content-Type: text/markdown

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

```python
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](https://unicode-fol-kit.readthedocs.io/en/latest/guide/quickstart.html) and
[Choosing a tool](https://unicode-fol-kit.readthedocs.io/en/latest/guide/choosing.html).

## Installation

```bash
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](https://unicode-fol-kit.readthedocs.io/en/latest/guide/higher-order.html).

## Building the documentation locally

```bash
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:

```bibtex
@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
