unicode_fol_kit.MSFLParser

class unicode_fol_kit.MSFLParser(many_sorted=False, fuzzy=False, modal=False, second_order=False, dependence=False, linear=False, lambek=False)

Bases: object

Unified parser supporting FOL, MSFOL, MSFL, FL, modal, and second-order modes.

Parameters:

• many_sorted (bool) – if True, quantifiers and constants must carry sort annotations (e.g. ∀x:Human P(x), alice:Human).

• fuzzy (bool) – if True, use Łukasiewicz operators (⊗ ⊕ for strong conjunction/disjunction; ¬ → ↔ map to Łukasiewicz nodes).

• modal (bool) – if True, parse classical unsorted FOL extended with modal, epistemic, doxastic, temporal, and deontic operators (□ ◇ K_a B_a Ⓖ Ⓕ Ⓝ Ⓤ Ⓞ Ⓟ). Cannot be combined with many_sorted or fuzzy in v1.

• second_order (bool) – if True, parse classical unsorted FOL extended with second-order quantifiers over predicate variables (∀P / ∃P, where P is an uppercase PREDICATE; the bound predicate’s arity is inferred from its applications in the body). Cannot be combined with many_sorted, fuzzy, or modal in v1.

• dependence (bool) – if True, parse the team-semantic dependence/IF fragment — literals, ∧, splitting ∨, ∀/∃, dependence atoms =(x, y), and slashed existentials ∃y/{x} φ. Standalone (no other flag).

• linear (bool) – if True, parse propositional intuitionistic linear logic — ⊗ & ⊕ ⊸ ! 𝟙 over atomic propositions. Standalone.

• lambek (bool) – if True, parse Lambek-calculus category types — • \ / over atomic categories (NP, S, …). Standalone.

Mode matrix:

(False, False) → FOL: classical ops incl. xor (⊕), unsorted quantifiers/constants (True, False) → MSFOL: classical ∧∨¬→↔⊕, sorted quantifiers/constants (True, True) → MSFL: Łukasiewicz operators, sorted quantifiers/constants (False, True) → FL: Łukasiewicz operators, unsorted quantifiers/constants modal=True → MODAL: classical unsorted FOL + modal/temporal/hybrid operators second_order=True → SO: classical unsorted FOL + second-order quantifiers (∀P / ∃P) dependence=True → DEP: team-semantic dependence/IF fragment linear=True → ILL: propositional intuitionistic linear logic lambek=True → L: Lambek-calculus category types

__init__(many_sorted=False, fuzzy=False, modal=False, second_order=False, dependence=False, linear=False, lambek=False)

Parameters:

• many_sorted (bool)

• fuzzy (bool)

• modal (bool)

• second_order (bool)

• dependence (bool)

• linear (bool)

• lambek (bool)

Methods

__init__([many_sorted, fuzzy, modal, ...])
parse(text)	Parse a formula string and return an AST node.

parse(text)

Parse a formula string and return an AST node.

Raises:

• NamingError – lexer-level failure (unrecognized character).

• ParsingError – parser-level failure (unexpected token or EOF), or a transformation-level failure such as a second-order predicate variable applied at conflicting arities (ConflictingArityError).

Parameters:

text (str)

Return type:

Node