main

Demonstrates applying a it.unibo.tuprolog.core.Substitution to a term via Substitution.applyTo.

A substitution built as {X -> abraham} is applied to the term father(X, isaac), replacing every occurrence of the variable X with the atom abraham. This is the core mechanism used internally by unification and resolution to propagate variable bindings across terms, and is useful to understand in isolation before looking at how it.unibo.tuprolog.unify.Unificator and the solvers use it.

Running this example prints father(abraham, isaac).

Demonstrates walking a chain of variable-to-variable bindings backwards with Substitution.getOriginal.

The substitution {X -> Y, Y -> Z} binds X to Y and Y to Z, forming a chain X -> Y -> Z. Calling getOriginal(Z) follows the chain backwards and retrieves X, the variable that was originally substituted to eventually reach Z. This is useful when a solver needs to recover the user-facing variable a value should be reported against, after internal renaming has introduced intermediate variables.

Running this example prints the substitution itself, followed by the variable X.

Demonstrates combining two independent substitutions with the + operator (it.unibo.tuprolog.core.Substitution.plus).

Two single-variable substitutions, {X -> abraham} and {Y -> isaac}, are merged into one substitution binding both X and Y. Because the two substitutions bind disjoint variables, the composition simply unions their bindings (contrast this with the Contradiction example in this same package, where composing substitutions that bind the same variable to different values yields a failed substitution). Applying the combined substitution to father(X, Y) replaces both variables at once.

Running this example prints father(abraham, isaac).

Demonstrates that composing two substitutions that bind the same variable to different, non-unifiable values yields a failed substitution (it.unibo.tuprolog.core.Substitution.Fail/Substitution.isFailed).

{X -> abraham} and {X -> nahor} both bind X, but to different atoms, so sub1 + sub2 is inconsistent and the + operator (it.unibo.tuprolog.core.Substitution.plus) produces a failed substitution rather than throwing. A failed substitution acts as an identity when applied to a term via applyTo: the term is returned unchanged because the (contradictory) bindings cannot be performed. This mirrors what happens internally when unification of two terms fails.

Running this example prints the failed substitution, followed by the original term father(X, isaac), unchanged.

Demonstrates the simplest way of building a it.unibo.tuprolog.core.Substitution: via the varargs Substitution.of factory, passing a sequence of Var to Term pairs.

Here X is bound to the atom abraham and Y to the atom isaac, producing a substitution with two independent bindings. This is the starting point for the other examples in this package, which show how substitutions can be applied to terms (Application), composed (Composition), found to be inconsistent (Contradiction), or chained (Chain).

Running this example prints the substitution, e.g. {X_0=abraham, Y_1=isaac}.