Unificator

interface Unificator: Any

Fields

Name Description
abstract context: Substitution

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

Methods

mgu

abstract 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

mgu

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

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

Parameters

Name Description
term1: Term
term2: Term

ReturnValue

Name Description
Substitution

match

open fun match(term1: Term, term2: Term, occurCheckEnabled: Boolean): Boolean

Tells whether two Terms match each other, that is there's a Most General Unifier for them

Parameters

Name Description
term1: Term
term2: Term
occurCheckEnabled: Boolean

ReturnValue

Name Description
Boolean

match

open fun match(term1: Term, term2: Term): Boolean

Tells whether two Terms match each other, that is there's a Most General Unifier for them. It performs unification with occur check

Parameters

Name Description
term1: Term
term2: Term

ReturnValue

Name Description
Boolean

unify

open fun unify(term1: Term, term2: Term, occurCheckEnabled: Boolean): Term?

Unifies two Terms if possible

Parameters

Name Description
term1: Term
term2: Term
occurCheckEnabled: Boolean

ReturnValue

Name Description
Term?

unify

open fun unify(term1: Term, term2: Term): Term?

Unifies two Terms if possible, with occurs check

Parameters

Name Description
term1: Term
term2: Term

ReturnValue

Name Description
Term?

CompanionObject

Unificator

interface Unificator: Any

Fields

Name Description
val default: /** * The default unification strategy that uses plain equals to determine [Term]s identity, and exploits an * LRU cache whose capacity is [DEFAULT_CACHE_CAPACITY] */

The default unification strategy that uses plain equals to determine Terms identity, and exploits an LRU cache whose capacity is DEFAULT_CACHE_CAPACITY

const DEFAULT_CACHE_CAPACITY: Int

Methods

mguWith

infix fun Term.mguWith(other: Term): Substitution

Computes the Most General Unifier, using default unification strategy

Receiver

Name Description
Term

Parameters

Name Description
other: Term

ReturnValue

Name Description
Substitution

matches

infix fun Term.matches(other: Term): Boolean

Computes whether the two terms match, using default unification strategy

Receiver

Name Description
Term

Parameters

Name Description
other: Term

ReturnValue

Name Description
Boolean

unifyWith

infix fun Term.unifyWith(other: Term): Term?

Computes the unified term, using default unification strategy

Receiver

Name Description
Term

Parameters

Name Description
other: Term

ReturnValue

Name Description
Term?

naive

fun naive(context: Substitution): Unificator

Creates naive unification strategy, with the given context, that checks Terms identity through their Term.equals methods, except in the case of numbers which are compared by value

Parameters

Name Description
context: Substitution

ReturnValue

Name Description
Unificator

naive

fun naive(): Unificator

Creates naive, empty unification strategy, that checks Terms identity through their Term.equals methods, except in the case of numbers which are compared by value

ReturnValue

Name Description
Unificator

strict

fun strict(context: Substitution): Unificator

Creates naive unification strategy, with the given context, that checks Terms identity through their Term.equals methods

Parameters

Name Description
context: Substitution

ReturnValue

Name Description
Unificator

strict

fun strict(): Unificator

Creates naive unification strategy, that checks Terms identity through their Term.equals methods

ReturnValue

Name Description
Unificator

cached

fun cached(other: Unificator, capacity: Int): Unificator

Makes another unification strategy cached, by letting memorising the most recent terms unified through it

Parameters

Name Description
other: Unificator

is the Unificator to be made cached

capacity: Int

is the maximum amount of items the cache may store

ReturnValue

Name Description
Unificator

a decorated Unificator