AbstractUnificator

abstract class AbstractUnificator: Unificator, Any

Fields

Name Description
open context: Substitution

The context (in terms of already present bindings) in which the unification is performed

Constructors

<init>

constructor(context: Substitution)

Parameters

Name Description
context: Substitution

Methods

checkTermsEquality

protected abstract fun checkTermsEquality(first: Term, second: Term): Boolean

Checks provided Terms for equality

Parameters

Name Description
first: Term
second: Term

ReturnValue

Name Description
Boolean

mgu

open fun mgu(term1: Term, term2: Term, occurCheckEnabled: Boolean): Substitution

Calculates the Most General Unifier of given Terms, optionally enabling occur-check

Parameters

Name Description
term1: Term
term2: Term
occurCheckEnabled: Boolean

ReturnValue

Name Description
Substitution

merge

open fun merge(substitution1: Substitution, substitution2: Substitution, occurCheckEnabled: Boolean): Substitution

Merges two Substitutions

Parameters

Name Description
substitution1: Substitution
substitution2: Substitution
occurCheckEnabled: Boolean

ReturnValue

Name Description
Substitution