ai.krr.fol
Interface Substitution

All Known Implementing Classes:

Instantiation, VariableRenaming

public interface Substitution

A Substitution maps a set of Variables to a set of Terms.

Author:

Gerhard Wickler

Method Summary

boolean	contains(Variable var) This function tests whether this Substitution contains the given Variable.
Term	getValue(Variable aVar) This function returns the Term the given Variable is mapped to under this Substitution.
boolean	unify(Term lTerm, Variable rVar) This function attempts to extend this Substitution such that the given Variable (from the "right" expression) and the given Term (from the "left") are unified and returns whether this succeeded.
boolean	unify(Variable lVar, Term rTerm) This function attempts to extend this Substitution such that the given Variable (from the "left" expression) and the given Term (from the "right") are unified and returns whether this succeeded.
boolean	unify(Variable lVar, Variable rVar) This function attempts to extend this Substitution such that the given Variables will be unified and returns true if this was possible.

Method Detail

unify

boolean unify(Variable lVar,
              Term rTerm)

This function attempts to extend this Substitution such that the given Variable (from the "left" expression) and the given Term (from the "right") are unified and returns whether this succeeded. The given Term must not be a Variable.

Parameters:

lVar - the Variable the given Term is to be unified with

rTerm - the Term the given Variable will be mapped to

Returns:

whether successful extension of this Substitution was possible

unify

boolean unify(Term lTerm,
              Variable rVar)

This function attempts to extend this Substitution such that the given Variable (from the "right" expression) and the given Term (from the "left") are unified and returns whether this succeeded. The given Term must not be a Variable.

Parameters:

lTerm - the Term the given Variable will be mapped to

rVar - the Variable the given Term is to be unified with

Returns:

whether successful extension of this Substitution was possible

unify

boolean unify(Variable lVar,
              Variable rVar)

This function attempts to extend this Substitution such that the given Variables will be unified and returns true if this was possible. Where this matters, the first variable is considered to come from the "left" expression and the second from the "right".

Parameters:

lVar - a Variable to be associated with the other given Variable

rVar - a Variable to be associated with the other given Variable

Returns:

whether successful extension of this Substitution was possible

contains

boolean contains(Variable var)

This function tests whether this Substitution contains the given Variable. In general, this will be the case if the Variable has been unified with another Variable or a Term.

Parameters:

var - the Variable that may occur in this Substitution

Returns:

whether the Variable is contained in this Substitution

getValue

Term getValue(Variable aVar)

This function returns the Term the given Variable is mapped to under this Substitution. More specifically, if the Variable has been unified with a Constant or FunctionTerm, this function returns that Term instantiated (cloned) under this Substitution. If the Variable is contained in this Substitution but not mapped to a Term (it may have been unified with another Variable only) or the Variable is not contained in this Substitution, then this substitution will be extended to map the given Variable to a new Variable that will also be returned. However, not all implementations can be extended in this way, and an Exception will be thrown if this is not possible.

Parameters:

aVar - the Variable the mapped Term is being sought for

Returns:

the instantiated Term the given Variable is mapped to