ontop/ontop — pull request #59 by bcogrel (2014-11-14 11:05:13+00:00)
Title: Feature/substitution

Proper distinction between `Unifier` and `Substitution`.

Remind that a unifier is a substitution that satisfy certain conditions. If unifier is the most common type of substitution, other substitutions are also considered (e.g. nullifiers, type propagating substitutions).

Some vocabulary changes:

- `Substitution` now refers to a substitution function. Its previous restricted meaning has been moved to
`SingletonSubstitution`.
- The `Unifier` class has been mostly replaced by the `Substitution` class. Its static method `getMGU()` is now in `UnifierUtilities`.
- Static methods not specific to unification have been moved to `SubstitutionUtilities`.

New functionality:
- Union between substitutions has been implemented.