Proof Pearl: A Formal Proof of Higman’s Lemma in ACL2

详细信息    查看全文

• 作者：Francisco J. Martí ; n-Mateos ; Jos&eacute ; L. Ruiz-Reina ; Jos&eacute ; A. Alonso ; Mariá ; J. Hidalgo
• 刊名：Lecture Notes in Computer Science
• 出版年：2005
• 出版时间：2005
• 年：2005
• 卷：3603
• 期：1
• 页码：p.358
• 全文大小：233 KB
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349

文摘

In this paper we present a formalization and proof of Higman’s Lemma in ACL2. We formalize the constructive proof described in [10] where the result is proved using a termination argument justified by the multiset extension of a well-founded relation. To our knowledge, this is the first mechanization of this proof.