如何用 ACL2 实现这些？ACL2 的近期增强功能
数学软件
2011-10-24 v1 计算机科学中的逻辑
符号计算
摘要
过去几年中，ACL2 的功能得到了重大增强，这在很大程度上是由其用户社区的需求推动的，包括现已普遍使用的实用工具，如 'make-event'、'mbe' 和信任标签。在本文中，我们提供了自版本 3.5 发布（2009 年 5 月，大约在 2009 年 ACL2 研讨会召开时）至 2011 年 7 月版本 4.3 发布（大约两年后）期间引入的一些 ACL2 增强功能的用户级概述。其中许多功能目前尚未被广泛熟知，但大多数 ACL2 用户至少可以利用其中一部分。一些更改可能会影响现有的证明工作，例如将 'member' 和 'member-equal' 等函数对视为同一函数的更改。
引用
@article{arxiv.1110.4673,
title = {How Can I Do That with ACL2? Recent Enhancements to ACL2},
author = {Matt Kaufmann and J Strother Moore},
journal= {arXiv preprint arXiv:1110.4673},
year = {2011}
}
备注
In Proceedings ACL2 2011, arXiv:1110.4473