First-order unification in the PVS proof assistant

Andréia Borges Avelar, André Luiz Galdino, Flávio Leonardo Cavalcanti de Moura, Mauricio Ayala-Rincón. First-order unification in the PVS proof assistant. Logic Journal of the IGPL, 22(5):758-789, 2014. [doi]

Abstract

Abstract is missing.