Reasoning

Clauses

class fosf.reasoning.clauses.ClauseNormalizer[source]

Bases: object

deref_tag(X)[source]
Parameters:

X (Tag)

Return type:

Tag

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

Terms

class fosf.reasoning.terms.TermUnifier[source]

Bases: ClauseNormalizer

homomorphisms()[source]
normalize(term, taxonomy, theory=None, rename_terms=True, return_degree=False)[source]
Parameters:
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]

Return 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. It can rename tags in terms to avoid clashes and optionally return the fuzzy unification degree.

Parameters:

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

  • taxonomy (SortTaxonomy) – The taxonomy or fuzzy taxonomy for GLB computation on sorts.

  • theory (OsfTheory, optional) – An OSF theory, used to normalize the unifier according to the theory’s constaints.

  • rename_terms (bool, default=True) – Whether to rename tags in terms to avoid clashes during unification.

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

Returns:

  • NormalTerm – The normalized term resulting from unification.

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

Return type:

NormalTerm | tuple[NormalTerm, float]

fosf.reasoning.terms.normalize_term(term, taxonomy, theory=None, return_degree=False)[source]
Parameters:
Return type:

NormalTerm

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]
Parameters:
Return type:

NormalTerm | tuple[NormalTerm, float]

Theory

class fosf.reasoning.theory.TheoryTermNormalizer[source]

Bases: object

deref_tag(X)[source]
Parameters:

X (Tag)

Return type:

Tag

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]
Parameters:
Return type:

NormalTerm | tuple[NormalTerm, float]