unicode_fol_kit.atp.modal_tableau

Labelled analytic tableaux for the propositional modal family.

The classical unicode_fol_kit.atp.tableau engine has no rule for a modal operator — a Box / Knows / Obligatory node makes it raise. This module fills that gap with a labelled (world-prefixed) tableau: a branch is a set of labelled formulas w: φ (worlds are integers) together with the accessibility edges generated along the way. The propositional / connective rules act at a fixed world; the modal rules move between worlds:

  • w: □φ (a box over its relation) asserts v: φ at every successor v of w — and is re-applied whenever a new successor appears;

  • w: ◇φ (a diamond) creates a fresh successor v with v: φ;

  • a negated box becomes a diamond of the negation and vice versa (¬□φ ≡ ◇¬φ).

The box/diamond family handled here is exactly the one with a single accessibility relation: alethic □/◇, epistemic K_a, doxastic B_a, deontic O/P, and the one-step temporal X (Next). The relation names match the KripkeModel convention ("alethic" / "K:"+a / "B:"+a / "deontic" / "temporal"), so an open branch is read off directly as a Kripke counter-model. The temporal closure operators Always (G), Eventually (F) and Until need least/greatest-fixpoint (eventuality) machinery beyond a basic labelled tableau and are rejected with a pointer to satisfies_modal() / isabelle_decide_modal(). Hybrid constructs (Nominal / At) are likewise rejected — a nominal’s name-exactly-one-world constraint has no rule here; use hybrid_is_valid (the standard translation + Z3) or evaluate in a KripkeModel with a nominals= assignment.

Frame conditions are realised as structural rules over the edge set: reflexivity adds w → w for every world, symmetry mirrors each edge, transitivity takes the closure, the euclidean rule closes w→v, w→u ⊢ v→u, and seriality manufactures a successor for a world that lacks one. The named systems are K, T, D/KD, B/KB, K4, K45, S4, S5, KD45.

Soundness vs. completeness. Every rule preserves satisfiability over its frame class, so a closed tableau is a real proof — is_modal_valid only returns True when the tableau closes. Termination on the transitive logics relies on subset blocking, and the whole search is bounded (max_worlds / max_steps); to keep the invalid verdict trustworthy regardless of any blocking/bound effect, an open branch’s model is verified with satisfies_modal() before it is reported, and a model that fails to falsify the formula downgrades the answer to "unknown" rather than risk a wrong "invalid". The result is the same valid / invalid / unknown contract as the local-Isabelle runner, but in-process and install-free.

Public API: modal_tableau_closed(), is_modal_valid(), modal_prove(), modal_decide(), modal_countermodel().

Functions

has_modal(node)

True iff node contains any modal/temporal/epistemic/deontic/hybrid operator.

is_modal_valid(formula[, frame, systems, ...])

Return True iff formula is modally valid over frame — ¬formula closes.

modal_countermodel(formula[, frame, ...])

Return a Kripke model falsifying formula over frame, or None.

modal_decide(formula[, frame, systems, ...])

Decide formula over frame: "valid" / "invalid" / "unknown".

modal_prove(premises, conclusion[, frame, ...])

Return True iff premises locally entail conclusion over frame.

modal_tableau_closed(formulas[, frame, ...])

Return True iff formulas are jointly unsatisfiable at a world (the tableau closes).
unicode_fol_kit.atp.modal_tableau.has_modal(node)[source]

True iff node contains any modal/temporal/epistemic/deontic/hybrid operator.

Hybrid constructs (Nominal / At) count as modal so the classical tableau routes them here, where they get the clean hybrid rejection instead of a generic no-rule error.

Parameters:

node (Node)

Return type:

bool

unicode_fol_kit.atp.modal_tableau.modal_tableau_closed(formulas, frame='K', systems=None, max_worlds=400, max_steps=200000)[source]

Return True iff formulas are jointly unsatisfiable at a world (the tableau closes).

Interprets the list as a set of formulas true at the same (root) world under the chosen frame (alethic system) and systems (per-family systems for epistemic / doxastic / deontic / temporal relations). Sound: a True is a real closed tableau. A False means “no closed tableau within the bound”, never a positive satisfiability claim — use modal_countermodel() for that.

Parameters:

  • frame (str)

  • max_worlds (int)

  • max_steps (int)

Return type:

bool

unicode_fol_kit.atp.modal_tableau.is_modal_valid(formula, frame='K', systems=None, max_worlds=400, max_steps=200000)[source]

Return True iff formula is modally valid over frame — ¬formula closes.

Sound: only the closed tableau yields True. An open or bound-exhausted search yields False (the formula is then invalid-or-unknown; modal_decide() distinguishes the two with a verified counter-model).

Parameters:
Return type:

bool

unicode_fol_kit.atp.modal_tableau.modal_prove(premises, conclusion, frame='K', systems=None, max_worlds=400, max_steps=200000)[source]

Return True iff premises locally entail conclusion over frame.

Local consequence: the tableau for premises ∪ {¬conclusion} at one world closes. Sound (a True is a closed tableau); incomplete only up to the bound.

Parameters:
Return type:

bool

unicode_fol_kit.atp.modal_tableau.modal_countermodel(formula, frame='K', systems=None, max_worlds=400, max_steps=200000)[source]

Return a Kripke model falsifying formula over frame, or None.

None means the formula is valid (the tableau closed) or the search was inconclusive within the bound. The returned model is verified: it is only handed back when satisfies_modal() confirms the formula is false at its root world, so a counter-model is never spurious.

Parameters:
unicode_fol_kit.atp.modal_tableau.modal_decide(formula, frame='K', systems=None, max_worlds=400, max_steps=200000)[source]

Decide formula over frame: "valid" / "invalid" / "unknown".

"valid" — the tableau for ¬formula closed (a sound proof). "invalid" — an open branch yielded a counter-model verified by

satisfies_modal().

"unknown" — the search hit the world/step bound, or an open branch’s model

failed verification (so neither verdict is safe to assert).

Mirrors the valid / invalid / unknown contract of the local-Isabelle runner (isabelle_decide_modal()), but runs fully in-process with no external prover.

Parameters:
Return type:

str