This work presents a general methodology for verification of the completeness of first-order unification algorithms à la Robinson developed in the higher-order proof assistant PVS. The methodology is based on a previously developed formalization of the theorem of existence of most general unifiers for unifiable terms over first-order signatures. Termination and soundness proofs of any unification algorithm are proved by reusing the formalization of this theorem and completeness should be proved according to the specific way in that non unifiable inputs are treated by the algorithm. © 2010 Springer-Verlag.
CITATION STYLE
Avelar, A. B., De Moura, F. L. C., Galdino, A. L., & Ayala-Rincón, M. (2010). Verification of the completeness of unification algorithms à la Robinson. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6188 LNAI, pp. 110–124). https://doi.org/10.1007/978-3-642-13824-9_10
Mendeley helps you to discover research relevant for your work.