首页    期刊浏览 2024年11月29日 星期五
登录注册

文章基本信息

  • 标题:A Formalization of the Theorem of Existence of First-Order Most General Unifiers
  • 本地全文:下载
  • 作者:Andréia B Avelar ; André L Galdino ; Flávio LC de Moura
  • 期刊名称:Electronic Proceedings in Theoretical Computer Science
  • 电子版ISSN:2075-2180
  • 出版年度:2011
  • 卷号:81
  • 页码:63-78
  • DOI:10.4204/EPTCS.81.5
  • 出版社:Open Publishing Association
  • 摘要:This work presents a formalization of the theorem of existence of most general unifiers in first-order signatures in the higher-order proof assistant PVS. The distinguishing feature of this formalization is that it remains close to the textbook proofs that are based on proving the correctness of the well-known Robinson's first-order unification algorithm. The formalization was applied inside a PVS development for term rewriting systems that provides a complete formalization of the Knuth-Bendix Critical Pair theorem, among other relevant theorems of the theory of rewriting. In addition, the formalization methodology has been proved of practical use in order to verify the correctness of unification algorithms in the style of the original Robinson's unification algorithm.
国家哲学社会科学文献中心版权所有