Reasoning

Clauses

fosf.reasoning.clauses.normalize_clause(clause: RootedClause, taxonomy: SortTaxonomy) → RootedSolvedClause[source]
fosf.reasoning.clauses.normalize_clause(clause: Clause, taxonomy: SortTaxonomy) → SolvedClause

Normalize a clause according to a sort taxonomy.

Parameters:
Return type:

SolvedClause

class fosf.reasoning.clauses.ClauseNormalizer[source]

Bases: object

Class implementing the OSF constraint normalization rules of [1].

Variables:

  • taxonomy (SortTaxonomy) – The taxonomy used for greatest lower bound computation on sorts.

  • self.rep_to_code (dict[Tag, int]) – A mapping from tags to an integer bitcode

  • self.rep_to_feats (dict[Tag, dict[Feature, Tag]]) – A mapping from tags to feature->tag maps.

normalize(clause: RootedClause, taxonomy: SortTaxonomy) → RootedSolvedClause[source]
normalize(clause: Clause, taxonomy: SortTaxonomy) → SolvedClause

Normalize a clause according to a sort taxonomy.

Parameters:
Return type:

SolvedClause

Terms

fosf.reasoning.terms.unify_terms(terms: list[Term], taxonomy: SortTaxonomy, theory: OsfTheory | None = None, rename_terms: bool = True, return_degree=False) → NormalTerm[source]
fosf.reasoning.terms.unify_terms(terms: list[Term], taxonomy: SortTaxonomy, theory: OsfTheory | None = None, rename_terms: bool = True, return_degree=True) → tuple[NormalTerm, float]

Unify the OSF terms according to a sort taxonomy and optionally an OSF theory.

Parameters:

  • terms (list[Term]) – The OSF terms to unify.

  • taxonomy (SortTaxonomy) – The background sort taxonomy for unification.

  • theory (OsfTheory | None, default=None) – Optionally, an OsfTheory to further normalize the unifier.

  • rename_terms (bool, default=True) – If True, rename apart the terms to unify.

  • return_degree (bool, default=False) – If True, return the subsumption degree of the unifier with respect to the input terms.

Returns:

A NormalTerm if return_degree is False. Otherwise, a NormalTerm and and approximation degree.

Return type:

NormalTerm | tuple[NormalTerm, float]

fosf.reasoning.terms.normalize_term(term: Term, taxonomy: SortTaxonomy, theory: OsfTheory | None = None, return_degree: bool = False) → NormalTerm[source]
fosf.reasoning.terms.normalize_term(term: Term, taxonomy: SortTaxonomy, theory: OsfTheory | None = None, return_degree: bool = True) → tuple[NormalTerm, float]

Normalize a single OSF term according to a sort taxonomy and optionally an OSF theory.

Parameters:
Return type:

NormalTerm | tuple[NormalTerm, float]

class fosf.reasoning.terms.TermUnifier[source]

Bases: ClauseNormalizer

Class implementing OSF term unification [1] and fuzzy OSF term unification [3].

Variables:

  • taxonomy (SortTaxonomy) – The taxonomy used for greatest lower bound computation on sorts.

  • self.rep_to_code (dict[Tag, int]) – A mapping from tags to an integer bitcode

  • self.rep_to_feats (dict[Tag, dict[Feature, Tag]]) – A mapping from tags to feature->tag maps.

  • terms (list[Term]) – List of terms to unify.

  • mappings (list[dict[Tag, Tag] | None]) – List of tag renamings (or None’s, if no renaming is applied), one for each term.

normalize(term, taxonomy, theory=None, return_degree=False)[source]

Normalize a single OSF term according to a sort taxonomy and optionally an OSF theory.

Parameters:
Returns:

A NormalTerm if return_degree is False. Otherwise, a NormalTerm and and approximation degree.

Return type:

NormalTerm | tuple[NormalTerm, float]

unify(terms: list[Term], taxonomy: SortTaxonomy, theory: OsfTheory | None = None, rename_terms=True, return_degree=False) → NormalTerm[source]
unify(terms: list[Term], taxonomy: SortTaxonomy, theory: OsfTheory | None = None, rename_terms=True, return_degree=True) → tuple[NormalTerm, float]

Compute the unification of a list of OSF Terms.

This method attempts to unify the provided terms according to the given (fuzzy) taxonomy and, optionally, an OSF theory. Tags in the inpyt terms can be renamed to avoid clashes. Optionally, the fuzzy unification degree can also be returned.

Parameters:

  • terms (list[Term]) – The terms to unify.

  • taxonomy (SortTaxonomy) – The (fuzzy) sort taxonomy used to compute greatest lower bounds of sorts during unification.

  • theory (OsfTheory, optional) – An OSF theory used to normalize the resulting unifier according to its constraints.

  • rename_terms (bool, default=True) – If True, rename tags in the input terms to avoid clashes.

  • return_degree (bool, default=False) – If True, also return the fuzzy unification degree.

Returns:

  • NormalTerm – The normalized term resulting from unification.

  • tuple[NormalTerm, float], optional – If return_degree is True, a tuple of the normalized term and the fuzzy unification degree.

Return type:

NormalTerm | tuple[NormalTerm, float]

homomorphisms()[source]

Generate mappings from the tags of each input term to the tags of their unifier.

Each mapping witnesses the subsumption of the unifier with respect to the respective input OSF term.

Note

This method should be called after unifying a few OSF terms in order to obtain the tag mappings.

Return type:

Generator[dict[Tag, Tag], None, None]

Theory

class fosf.reasoning.theory.TheoryTermNormalizer[source]

Bases: object

Class implementing OSF theory normalization according to the constraint normalization rules of [2]. Additionally, it implements the computation of the satisfaction degree of an OSF term with respect to the constraints of the OSF theory.

Note

A global tag is a tag appearing in an OSF term. A local tag is a theory tag.

Variables:

  • taxonomy (SortTaxonomy) – A backgrond (fuzzy) sort subsumption taxonomy.

  • theory (OsfTheory) – The OSF theory used for normalization.

  • rep_to_feats (dict[Tag, dict[Feature, Tag]]) – A dict mapping each tag to a feature-tag map. Represents the features materialized for each tag, and their corresponding value.

  • frames (dict[Tag, _Frame]) – A dict maping each global tag to its principal frame.

  • global_to_frames (dict[Tag, set[Tag]]) – A dict mapping each global tag X to the frames where X appears.

  • eq_queue (deque[tuple[Tag, Tag]]) – High-priority queue, holding equality constraints to be processed.

  • queue (deque[Constraint]) – Queue, holding the rest of the constraints to be processed.

  • rule_9_stack (dict[Tag, Feature]) – Low-priority stack, delaying the rule-9 applications which can cause the normalization to diverge.

normalize(term: Term, theory: OsfTheory, normalize_first: bool, return_degree=False) → NormalTerm[source]
normalize(term: Term, theory: OsfTheory, normalize_first: bool, return_degree=True) → tuple[NormalTerm, float]

Normalize an input (normal) OSF term with respect to an OSF theory.

OSF theory normalization ensures that an input (normal) OSF term satisfies the constraints of an OSF theory.

Parameters:

  • term (Term)

  • theory (OsfTheory)

  • normalize_first (bool, default=True) – If True, make sure that the input term is in Normal form.

  • return_degree (bool, default=False) – If True, return the satisfaction degree of the normalized OSF term with respect to the OSF theory.

Return type:

NormalTerm | tuple[NormalTerm, float]

References

[1] (1,2)

Hassan Aït-Kaci and Andreas Podelski. Towards a meaning of life. J. Log. Program., 16(3):195–234, 1993. doi:https://doi.org/10.1016/0743-1066(93)90043-G.

[2]

Hassan Aït-Kaci, Andreas Podelski, and Seth Copen Goldstein. Order-sorted feature theory unification. The Journal of Logic Programming, 30(2):99–124, 1997. doi:https://doi.org/10.1016/S0743-1066(96)00053-2.

[3]

Gian Carlo Milanese and Gabriella Pasi. Fuzzy order-sorted feature logic. Fuzzy Sets and Systems, 477:108800, 2024. doi:https://doi.org/10.1016/j.fss.2023.108800.