unicode_fol_kit.to_thf_modal

unicode_fol_kit.to_thf_modal(formula, mode='constant', frame='K')

Emit a Benzmüller-style TPTP THF shallow embedding of formula.

Produces a complete, self-contained THF problem — type declarations, the lifted modal operators, the frame axioms for frame (K/T/S4/S5/KD/KD45), the existsAt domain axioms for mode (constant / increasing / decreasing / varying), and the conjecture mvalid @ ⟨formula⟩ — ready for a higher-order ATP (Leo-III, Satallax). Covers the alethic □/◇ fragment.

Equality = / ≠ is emitted as an ordinary uninterpreted (world-relativized) predicate, not primitive HOL identity, to stay faithful to satisfies_modal and the first-order embedding; for rigid identity, add your own axioms to the output.

Parameters:

• formula (Node)

• mode (str)

• frame (str)

Return type:

str