unicode-logic-kit

# unicode-logic-kit

[![Tests](https://github.com/fvossel/unicode-logic-kit/actions/workflows/tests.yml/badge.svg)](https://github.com/fvossel/unicode-logic-kit/actions/workflows/tests.yml)
[![Isabelle live tests](https://github.com/fvossel/unicode-logic-kit/actions/workflows/isabelle-tests.yml/badge.svg)](https://github.com/fvossel/unicode-logic-kit/actions/workflows/isabelle-tests.yml)
[![PyPI](https://img.shields.io/pypi/v/unicode-logic-kit)](https://pypi.org/project/unicode-logic-kit/)
[![Docs](https://readthedocs.org/projects/unicode-logic-kit/badge/?version=latest)](https://unicode-logic-kit.readthedocs.io/)

<!-- mcp-name: io.github.fvossel/unicode-logic-kit -->

A Python toolkit for **logic with Unicode operators** — *parse, transform, and reason
about* formulas of classical first-order logic and well beyond it: modal, temporal,
hybrid, many-valued, fuzzy, intuitionistic, relevant, second- and third-order,
description, dependence/IF, substructural, and a range of further non-classical
logics. On top of that sits **infrastructure for NL→logic research**:
one small API a verification loop can drive, one uniform verdict type over a dozen
provers, and an evaluation toolbox for scoring LLM-generated formulas against
benchmark gold data.

```python
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
```

> **Renamed in 0.31.0.** Up to 0.30.0 this package was `unicode-fol-kit`
> (`import unicode_fol_kit`): first-order logic is one of the logics it handles,
> not the whole of it. `pip install -U unicode-fol-kit` still works — it installs
> this package and forwards the old import name with a `DeprecationWarning` — but
> new code should `pip install unicode-logic-kit` and `import unicode_logic_kit`.
> Nothing else changed its name, the `UFK_` environment variables included.

## Why this kit?

- **One facade, seven verbs, built for LLM loops.** `api.parse_any` (dialect
  auto-detection over Unicode / TPTP / LaTeX / Prover9 / SMT-LIB — never raises,
  records every parser's objection), `api.check` (well-formedness + signature
  conformance with did-you-mean suggestions), `api.equivalent`, `api.prove`,
  `api.countermodel`, `api.repair` (a diagnose→suggest→fix generator whose fixer
  callback is *your* LLM), `api.translate` (logic-to-logic via a comorphism
  registry). Every result has a JSON-compatible `to_dict()`, and the API carries an
  explicit stability policy.
- **Logics as values, and a translation that carries its side conditions.**
  `FOL(MSFOL(f))` converts a sorted formula and keeps its side axioms (each
  sort is non-empty, each sorted constant lies in its sort) *with* the term, as
  a `Sentence`; `api.prove` adds them as premises itself, which is the
  difference between a proof and a spurious countermodel. Each of
  the nine registry edges declares what it preserves (`comorphism.GUARANTEES`),
  which side axioms its image needs and which options it reads; a composed path
  reports the weakest guarantee on it. There is no implicit coercion between
  logics on purpose — see
  [Translating between logics](https://unicode-logic-kit.readthedocs.io/en/latest/guide/logic-graph.html)
  for why a translation is not an upcast.
- **An MCP server out of the box.** `pip install unicode-logic-kit[mcp]`, then
  `python -m unicode_logic_kit.mcp` (or, with nothing installed,
  `uvx "unicode-logic-kit[mcp]" mcp`) exposes the toolkit as thirty-seven Model
  Context Protocol tools (23 general-purpose, 6 for chemistry, 8 for
  description logic) — any MCP client (Claude Code/Desktop, agent
  frameworks, editors) can parse, prove, diagnose and translate without
  writing Python; the repair loop inverts naturally (the client LLM is the
  fixer). An error-analysis layer comes along: prediction-vs-gold
  breakdowns with symbol diffs (`compare_formulas`), corpus metrics
  (`score_batch`), satisfiability of premise sets with model witnesses
  (`check_consistency`), normal forms, cross-syntax rendering, truth
  tables, signature extraction, and DRS→FOL for discourse phenomena.
- **Model checking against real structures, not just model finding.** A
  molecule, a knowledge-graph neighbourhood, a scene graph is *given* — the
  question is whether a definition holds of it. `FiniteStructure` +
  `evaluate_in_structure` answer that directly: no prenex form, no CNF
  (both are documented timeout sources elsewhere), quantifiers ranging over
  indexed candidate sets rather than the whole domain, counting quantifiers
  counted instead of expanded, and properties that are decidable on a
  structure but not first-order definable over it (connectivity, ring
  membership) admitted as **computed predicates**. `unicode_logic_kit.chem`
  turns a SMILES string into such a structure over the ChemLog signature.
- **Rule learning, both directions, with the silent failures made loud.**
  `unicode_logic_kit.ilp` turns those same structures into an ILP task (Popper's
  `bk.pl` / `exs.pl` / `bias.pl`) and reads the learned Prolog clause back as a
  kit formula you can model-check. Two encoding mistakes produce a hypothesis
  that scores **precision 1.00 and means nothing** — example-local individual
  names a learner joins across, and the example argument on every predicate —
  and both are refused rather than documented, on the way out and on the way
  back. `check_separation` asks the question that has to come first: does your
  reference definition separate the two example sets at all?
- **Exact probabilistic logic — no sampling, no floats.**
  `prob.entailment_bounds` answers "what does P(bird)=0.9 entail about
  P(fly)?" with the exact tightest interval (Nilsson's probabilistic
  entailment as a rational LP over possible worlds, conditionals included);
  `prob.query` answers ProbLog-style queries over definite programs with
  independent probabilistic facts under Sato's distribution semantics —
  every result an exact `Fraction`, every unsupported fragment a loud
  refusal.
- **Twenty-five prover backends, one honest `Verdict`.** The kit's own calculi and
  semantic searches (resolution — with sound paramodulation/demodulation for
  equality, no hand-supplied congruence axioms needed —, analytic tableaux
  with recorded, independently checkable proof objects, modal tableau, finite
  model finder, bounded Kripke enumeration, QML embedding) are first-class
  citizens next to Z3,
  cvc5, Vampire, E, Zipperposition, Twee (equational proofs re-verified by an
  independent checker before the kit reports them), Prover9, Leo-III, Isabelle,
  nanoCoP-M (native first-order modal logic, opt-in with a mandatory independent
  cross-check) and a Dockerized HETS server (CASL export *and* round-trip
  import with native many-sortedness, multi-spec DOL library emission,
  SPASS/darwin behind one name, comorphism provenance in every
  verdict). Every route returns the same
  `Verdict` with a semantic status (`proved` / `refuted` / `unknown` / `error`),
  a separate *why-not-more* axis (`timeout` ≠ `bound_hit` ≠ `incomplete` ≠
  `unsupported`), the SZS status, wall time, and JSON-able witnesses. Chains,
  portfolios (`portfolio_prove`, parallel with agreement thresholds and a
  soundness alarm on prover disagreement), and cached batch runs
  (`batch_decide`) are built on top.
- **An evaluation toolbox for NL→FOL work.** A graded equivalence ladder (exact →
  canonical → vocabulary-aligned → solver, with a tri-state solver level and
  partial credit), AST-level symbol alignment, gold-formula self-audit, and
  adapters for **FOLIO, MALLS, GROVES, WillowNLtoFOL, ProntoQA, ProofWriter,
  LogicNLI, ProverQA and FraCaS** — each with its upstream schema verified at the
  source and its limitations documented instead of smoothed over. FraCaS is the
  pure-NLI one: no gold formulas at all, so the translation step is an injected
  callable and the kit only decides.
- **Countermodels that explain themselves.** `api.countermodel` returns a
  machine-readable witness *plus* a plain-English rendering ("The countermodel has
  2 possible worlds. … At world 0 the formula fails."), and refutation actually
  covers the temporal fragment: `Ⓕ P → P` comes back **refuted** with a two-world
  Kripke witness, not "unknown".
- **Honesty as a contract.** No route silently degrades: fuzzy input is refused by
  classical provers rather than collapsed, an unavailable backend raises instead
  of vanishing from the chain, incomplete methods report *why* they stopped, and
  every proof method has an independent checker.

```python
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
```

One parser class, `MSFLParser`, reads classical logic at the **first, second and third
order**, each with or without **sorts** and with or without the **modal** family
(modal/temporal/epistemic/deontic/hybrid): twelve combinations of three constructor
flags. Next to them stand many-sorted and single-sorted Łukasiewicz fuzzy logic,
team-semantic dependence/IF logic, intuitionistic linear logic, and the Lambek calculus.
The surface syntax is natural Unicode (`∀ ∃ ∧ ∨ ¬ → ↔ ⊕ ⊗ □ ◇ @ ⊸ 𝟙 …`) with 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** — the latter backed by Dyckhoff's **G4ip**, a genuine
terminating decision procedure for propositional intuitionistic logic — and analytic
tableaux), a **finite mode