unicode_fol_kit.isabelle_decide_fol

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