unicode_fol_kit.to_fol

unicode_fol_kit.to_fol(node, include_sort_facts=False)[source]

Reduce an MSFL (or plain FOL) node to a purely classical FOL node.

Two-phase reduction: 1. to_msfol() — replaces Łukasiewicz operators with classical boolean

counterparts (And/Or/Not/Implies/Iff); sort annotations are preserved.

  1. _relativize() — replaces SortedQuantifier with a guarded plain Quantifier; replaces SortedConstant with a plain Constant and collects sort-membership atoms as a side-effect.

Parameters:

  • node (Node) – any Node (MSFL or classical FOL).

  • include_sort_facts (bool) – if True, deduplicated sort-membership atoms are conjoined as a prefix block at the top level. Dedup is by (sort-predicate, constant-name) in first-occurrence order.

Returns:

A Node built from classical FOL constructs only.

Return type:

Node