unicode_fol_kit.hol.isabelle_runner

Run a local Isabelle to actually discharge the emitted shallow-embedding theories — turning the unicode_fol_kit.hol exporters from emit into proven / refuted.

The rest of the toolkit only emits HOL/Isabelle/THF problem files (see the hol package docstring): it is honest that first-order modal logic, FOL and SOL are undecidable, so an emission is “a sound problem a prover may discharge”. This module is the opt-in other half: if a local Isabelle/HOL is installed, it writes the emitted theory to a scratch session, invokes isabelle build, and reads the verdict off the build — a real proof, not a promise.

Decision procedure for modal validity (isabelle_decide_modal())

The shallow embedding is faithful to the Kripke evaluator unicode_fol_kit.semantics.kripke.satisfies_modal(), so deciding the emitted lemma decides the modal formula (for the chosen frame / domain regime):

  1. Prove — emit lemma <goal> with a proof that brings the frame/domain axioms into scope and tries a battery of methods (using <axioms> by (blast | force | fastforce | auto | meson … | metis …)). If isabelle build exits 0, the lemma is a theorem ⇒ the formula is VALID.

  2. Refute — otherwise emit the same lemma followed by nitpick[expect = genuine]. Nitpick searches for a finite counter-model; expect = genuine makes the build succeed iff a genuine counter-model is found, so exit 0 here ⇒ the formula is INVALID. The verdict is certified by the exit code; for the propositional alethic fragment ModalVerdict.countermodel then carries a concrete Kripke counter-model reconstructed from the toolkit’s own evaluator (isabelle build does not echo nitpick’s model), and is None for fragments the bounded search does not cover — never weakening the verdict.

  3. Otherwise the result is UNKNOWN (neither a battery proof nor a finite counter-model within the time/size budget — expected, since the logic is undecidable).

This is sound (Isabelle’s kernel certifies the proof; nitpick reports only genuine counter-models), and necessarily incomplete.

Honesty / soundness boundary

A VALID / INVALID verdict is only as meaningful as the embedding’s faithfulness to the chosen semantics. UNKNOWN is a real outcome, not a failure. The runner never claims a decision it did not obtain from the prover.

Platform support

Linux and macOS are the primary path: the isabelle binary is invoked directly (isabelle build -D <dir>) with nothing platform-specific. Windows is also supported — Isabelle ships its own Cygwin and its CLI is a Bash script, so there the runner additionally routes the build through contrib/cygwin/bin/bash, translates the scratch path to a /cygdrive/... path, and (idempotently) sets the execute bit on the launcher scripts (some installs ship them without it, which makes the internal exec isabelle java fail with Permission denied). No install path is ever hard-coded; installations are discovered generically (see below).

Locating Isabelle

find_isabelle() looks, in order, at an explicit path, the env vars UFK_ISABELLE_HOME / ISABELLE_HOME, isabelle on PATH, and a light scan of standard install locations. isabelle_available() is the cheap predicate tests gate on (skip when no Isabelle is present).

Functions

check_theory(theory_text, theory_name, *[, ...])

Build one self-contained Isabelle theory and report whether it loads/proves.

find_isabelle([isabelle_home, use_cache])

Locate an Isabelle installation, or return None if none is found.

isabelle_available([isabelle_home])

True iff an Isabelle installation can be located (cheap; cached).

isabelle_decide_fol(formula, *[, msfol, ...])

Decide a classical FOL (or MSFOL) formula's validity by running Isabelle.

isabelle_decide_modal(formula, *[, frame, ...])

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

Classes

BuildResult(ok, exit_code, output, ...)

Outcome of building one scratch theory with isabelle build.

FolVerdict(status[, method, countermodel, ...])

Result of deciding a classical FOL formula's validity through Isabelle.

IsabelleInstall(home, is_windows, isabelle_exe)

A located Isabelle/HOL installation and how to invoke its CLI.

ModalVerdict(status, frame, mode[, method, ...])

Result of deciding a modal formula's validity through Isabelle.

Exceptions

IsabelleNotAvailable

Raised when an Isabelle install is required but none could be located.
exception unicode_fol_kit.hol.isabelle_runner.IsabelleNotAvailable[source]

Bases: RuntimeError

Raised when an Isabelle install is required but none could be located.

class unicode_fol_kit.hol.isabelle_runner.IsabelleInstall(home, is_windows, isabelle_exe, cygwin_bash=None, version=None)[source]

Bases: object

A located Isabelle/HOL installation and how to invoke its CLI.

Parameters:

  • home (str)

  • is_windows (bool)

  • isabelle_exe (str)

  • cygwin_bash (str | None)

  • version (str | None)

home: str
is_windows: bool
isabelle_exe: str
cygwin_bash: str | None = None
version: str | None = None
class unicode_fol_kit.hol.isabelle_runner.BuildResult(ok, exit_code, output, theory_name, session, elapsed)[source]

Bases: object

Outcome of building one scratch theory with isabelle build.

Parameters:
ok: bool
exit_code: int
output: str
theory_name: str
session: str
elapsed: float
class unicode_fol_kit.hol.isabelle_runner.ModalVerdict(status, frame, mode, method=None, countermodel=None, prove_output='', refute_output='', prove_elapsed=0.0, refute_elapsed=0.0, infra_error=None)[source]

Bases: object

Result of deciding a modal formula’s validity through Isabelle.

status is one of "valid" (a battery proof closed the lemma), "invalid" (nitpick found a genuine counter-model), or "unknown" (neither, within budget). Truthiness follows validity. On an "unknown" result, infra_error is set to a short signature when a build failed for an infrastructure reason (syntax/JVM/timeout/…) rather than honest incompleteness — it never changes the status (an infra failure can only land on UNKNOWN).

Parameters:

  • status (str)

  • frame (str)

  • mode (str)

  • method (str | None)

  • countermodel (str | None)

  • prove_output (str)

  • refute_output (str)

  • prove_elapsed (float)

  • refute_elapsed (float)

  • infra_error (str | None)

status: str
frame: str
mode: str
method: str | None = None
countermodel: str | None = None
prove_output: str = ''
refute_output: str = ''
prove_elapsed: float = 0.0
refute_elapsed: float = 0.0
infra_error: str | None = None
property is_valid: bool
property is_invalid: bool
property is_unknown: bool
class unicode_fol_kit.hol.isabelle_runner.FolVerdict(status, method=None, countermodel=None, prove_output='', refute_output='', prove_elapsed=0.0, refute_elapsed=0.0, infra_error=None)[source]

Bases: object

Result of deciding a classical FOL formula’s validity through Isabelle.

Same VALID / INVALID / UNKNOWN scheme as ModalVerdict (no frame/mode). Note that FOL is only semi-decidable, so UNKNOWN is common and expected; and equality = / ≠ is the uninterpreted predicate feq / fneq of to_isabelle_fol() (no equality axioms are assumed), so e.g. ∀x. x = x is not VALID here.

Parameters:

  • status (str)

  • method (str | None)

  • countermodel (str | None)

  • prove_output (str)

  • refute_output (str)

  • prove_elapsed (float)

  • refute_elapsed (float)

  • infra_error (str | None)

status: str
method: str | None = None
countermodel: str | None = None
prove_output: str = ''
refute_output: str = ''
prove_elapsed: float = 0.0
refute_elapsed: float = 0.0
infra_error: str | None = None
property is_valid: bool
property is_invalid: bool
property is_unknown: bool
unicode_fol_kit.hol.isabelle_runner.find_isabelle(isabelle_home=None, *, use_cache=True)[source]

Locate an Isabelle installation, or return None if none is found.

Search order: isabelle_home argument → env UFK_ISABELLE_HOME → env ISABELLE_HOME → isabelle on PATH → a light scan of standard install locations. The result is cached (keyed by the explicit argument); pass use_cache=False to force a fresh lookup.

Parameters:

  • isabelle_home (str | None)

  • use_cache (bool)

Return type:

IsabelleInstall | None

unicode_fol_kit.hol.isabelle_runner.isabelle_available(isabelle_home=None)[source]

True iff an Isabelle installation can be located (cheap; cached).

Parameters:

isabelle_home (str | None)

Return type:

bool

unicode_fol_kit.hol.isabelle_runner.check_theory(theory_text, theory_name, *, install=None, session=None, session_timeout=120, wall_timeout=None, keep=False)[source]

Build one self-contained Isabelle theory and report whether it loads/proves.

Writes <theory_name>.thy plus a ROOT (session ... = HOL + options [timeout] theories <theory_name>) into a scratch directory and runs isabelle build on it. ok is True iff the build exits 0 — i.e. every proof in the theory was discharged by Isabelle’s kernel.

Parameters:

  • theory_text (str) – the full theory <theory_name> ... end text. Its declared theory name MUST equal theory_name.

  • theory_name (str) – the theory / file name (a valid Isabelle identifier).

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

  • session (str | None) – the build session name (default "S_" + theory_name).

  • session_timeout (int) – per-session Isabelle timeout option, in seconds.

  • wall_timeout (float | None) – hard subprocess timeout; defaults to session_timeout + 180 to cover JVM startup + image load.

  • keep (bool) – keep the scratch directory (for debugging) instead of deleting it.

Raises:

IsabelleNotAvailable – if no Isabelle installation can be located.

Return type:

BuildResult

unicode_fol_kit.hol.isabelle_runner.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

unicode_fol_kit.hol.isabelle_runner.isabelle_decide_fol(formula, *, msfol=False, methods=('blast', 'force', 'fastforce', 'auto', 'meson', 'metis'), refute=True, card='1-4', prove_timeout=60, refute_timeout=60, install=None)[source]

Decide a classical FOL (or MSFOL) formula’s validity by running Isabelle.

Emits the uninterpreted-signature embedding (to_isabelle_fol(), or to_isabelle_msfol when msfol=True) and, exactly like isabelle_decide_modal():

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

  2. otherwise (refute) runs nitpick[expect = genuine] over the individual type i — exit 0 ⇒ INVALID;

  3. otherwise UNKNOWN (common — FOL is only semi-decidable).

Sound (Isabelle’s kernel certifies the proof; nitpick reports only genuine finite counter-models) and necessarily incomplete. Equality is uninterpreted (see FolVerdict).

Parameters:

  • formula (Node) – the FOL AST node.

  • msfol (bool) – emit the many-sorted embedding (sorts relativised to guard predicates) instead of plain FOL.

  • install (IsabelleInstall | None) – as for isabelle_decide_modal() (card bounds the individual type i).

  • methods (Sequence[str])

  • refute (bool)

  • card (str)

  • prove_timeout (int)

  • refute_timeout (int)

  • install

Raises:

IsabelleNotAvailable – if no Isabelle installation can be located.

Return type:

FolVerdict