Unification
6 methods in the atlas attack this one problem. They are rivals: each wins something the others do not.
Phrasings that mean this problem
Syntactic unificationEquational unificationHigher-order unification
automated-reasoning
- Robinson unificationOccurs-check substitution buildingstandardautomated-reasoning
- Martelli-Montanari unificationMultiequation transformation rulesspecialistautomated-reasoning
- Paterson-Wegman unificationShared-DAG linear mergingspecialistautomated-reasoning
- AC unificationDiophantine basis enumerationspecialistautomated-reasoning
- Huet's algorithmFlex-rigid pair enumerationspecialistautomated-reasoning
- Miller pattern unificationDistinct-bound-variable restrictionspecialistautomated-reasoning