unicode_fol_kit.standard_translation

unicode_fol_kit.standard_translation(formula, world='w')[source]

Translate a propositional modal formula into a classical FOL Node.

world names the free current-world variable threaded through the translation (default "w"); the result is a plain first-order formula in which propositional atoms A become A(world) and each modality becomes a quantification over a fresh world variable bounded by an accessibility predicate (see the module docstring for the exact scheme and the fixed predicate names). The returned Node uses only classical FOL constructs, so it can be handed to to_z3 / to_prover9 / to_tptp / the Tarski evaluator.

Hybrid constructs translate too: Nominal i becomes the world-equality world = nom_i and At(i, φ) becomes ST(φ) anchored at the constant nom_i (the "nom_" prefix keeps nominal constants disjoint from user constants — see the module docstring).

Raises:

NotImplementedError – on Until (not first-order definable), any object-level quantifier (first-order modal logic is out of scope for v1), a Łukasiewicz node, or a lambda node.

Parameters:
Return type:

Node