Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem - Avelar, Andréia Borges (2011)
Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2009.