@Inproceedings{EPTCS81.5, author = {Avelar, Andr\'eia B and Galdino, Andr\'e L and de Moura, Fl\'avio LC and Ayala-Rinc\'on, Mauricio}, year = {2012}, title = {A Formalization of the Theorem of Existence of First-Order Most General Unifiers}, editor = {Rocca, Simona Ronchi della and Pimentel, Elaine}, booktitle = {{\rm Proceedings 6th Workshop on} Logical and Semantic Frameworks with Applications, {\rm Belo Horizonte, Brazil, 27 August 2011}}, series = {Electronic Proceedings in Theoretical Computer Science}, volume = {81}, publisher = {Open Publishing Association}, pages = {63-78}, doi = {10.4204/EPTCS.81.5}, }