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
Methods
checkTermsEquality
protected abstract fun checkTermsEquality(first: Term, second: Term): Boolean
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
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
|
Checks provided Terms for equality