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