agent_logic.proofs.unification

Classes

Unification()

Handles unification for first-order logic terms.
class agent_logic.proofs.unification.Unification[source]

Bases: object

Handles unification for first-order logic terms.

static unify(term1, term2)[source]

Unifies two predicates by finding a substitution θ such that term1(θ) = term2(θ). .. rubric:: Example

P(x) and P(f(y)) → {x → f(y)}

Return type:

Optional[Dict[str, str]]

Parameters: