core/it.unibo.tuprolog.argumentation.core.runtime/Arg2pUnificator

Arg2pUnificator

The unificator of the argumentation solvers: the default one, without the occurs check unless explicitly requested (as in unify_with_occurs_check/2), as in standard Prolog, computed in a single pass (see Unification).

The occurs check visits the whole term bound to a variable, and arguments (nested lists of rules, conclusions and premises) are bound to variables at almost every resolution step.

Properties

context

open override val context: Substitution

Functions

match

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

Theories look clauses up by matching Head :- _ against each stored clause: the body is a fresh variable, which matches any body, so only the heads are compared. Matching the bodies too would cost, with the default unificator, a pass over the stored body for every variable of the head.

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

merge

open override fun merge(substitution1: Substitution, substitution2: Substitution): Substitution

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

mgu

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

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

unify

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

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