"First-order unification in the PVS proof assistant."

Andréia Borges Avelar et al. (2014)
a service of Schloss Dagstuhl - Leibniz Center for Informatics