unicode_fol_kit.team_satisfies

unicode_fol_kit.team_satisfies(structure, team, formula)[source]

Return whether team satisfies formula in structure.

Väänänen’s strict team semantics over a finite structure. team is any iterable of assignments (mappings from variable names to domain elements); it is copied and deduplicated internally, so the caller’s dicts are never mutated and duplicates are harmless.

Parameters:

  • structure (Structure) – a finite first-order Structure (the same class the Tarskian evaluator uses).

  • team (Iterable[Mapping[str, Any]]) – an iterable of dict[str, element] assignments. The empty team satisfies every formula of the fragment.

  • formula (Node) – a formula of the team fragment — literals, ∧, the splitting ∨, ∀/∃, dependence atoms =(…), and slashed existentials ∃x/{…} (parse with MSFLParser(dependence=True)).

Raises:

  • TypeError – for a node outside the team fragment (→, ↔, ¬ of a non-atom, dual negation of team atoms, modal/fuzzy nodes, …).

  • ValueError – when a brute-force search would exceed MAX_TEAM_SEARCH candidates.

Return type:

bool