Унификация двух формул
 

Помогите пожалуйста, Нужно сделать программу для унификации формул и поиск общего унификатора.Может кто то знает где информация есть по этому алгоритму и исходник тоже не помешал бы желательно на языке С(конечно это я много прошу ну вдруг у кого то есть), или хотябы объяснить как его реализовать.