实用简化程序的封装
摘要：ACL2 用于证明两个简化过程的性质。这两个过程在复杂性上有所不同，但解决的是在解析/参数模拟定理证明系统的背景下出现的相同编程问题。术语重写是这两个过程的核心，但重写过程本身的细节是无关紧要的。ACL2 的封装机制用于断言重写函数的存在并陈述一些其性质。每个过程的终止性、不可简约性和正确性性质都得到了证实。ACL2 中封装机制的可用性被认为对于快速和高效地验证这种算法是至关重要的。
作者：Olga Shumsky Matlin and William McCune
论文ID：cs/0402010
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23