unicode_fol_kit.isabelle_decide_modal

unicode_fol_kit.isabelle_decide_modal(formula, *, frame='K', mode='constant', temporal_closure=True, methods=('blast', 'force', 'fastforce', 'auto', 'meson', 'metis'), refute=True, card='1-4', prove_timeout=60, refute_timeout=60, install=None)[source]

Decide a modal formula’s validity by running a local Isabelle.

Emits the Benzmüller shallow embedding of formula (isabelle_modal_theory(), faithful to satisfies_modal()) and:

  1. tries a proof battery — exit 0 ⇒ VALID;

  2. otherwise (refute) runs nitpick[expect = genuine] — exit 0 ⇒ INVALID (certified by the exit code; for the propositional alethic fragment countermodel carries a concrete Kripke model from the toolkit’s evaluator, else None);

  3. otherwise UNKNOWN.

Parameters:

  • formula (Node) – the modal AST node.

  • frame (str) – alethic frame system (K/T/S4/S5/KD/KD45) — fixes the axioms on r.

  • mode (str) – object-quantifier domain regime (constant/possibilist/varying/…).

  • temporal_closure (bool) – constrain the temporal relation to refl+trans (henceforth).

  • methods (Sequence[str]) – proof methods tried, in order, as a by (… | …) battery.

  • refute (bool) – also run nitpick to certify INVALID when the proof battery fails.

  • card (str) – nitpick cardinality range for the world type i (e.g. "1-4").

  • refute_timeout (int) – per-session Isabelle timeouts (seconds).

  • install (IsabelleInstall | None) – an IsabelleInstall; located via find_isabelle() when None.

  • prove_timeout (int)

  • refute_timeout

Returns:

A ModalVerdict.

Raises:

  • IsabelleNotAvailable – if no Isabelle installation can be located.

  • ValueError / NotImplementedError – propagated from the emitter for an unsupported frame/mode/operator (e.g. Until).

Return type:

ModalVerdict