用于实际简化过程的封装
Encapsulation for Practical Simplification Procedures
摘要：
利用ACL 2证明了两种简化方法的性质。程序的复杂性不同，但解决了相同的编程问题，在决议/paramodulation定理证明系统的背景下出现的。术语重写是这两个过程的核心，但重写过程本身的细节是无关紧要的。ACL 2封装构造用于断言重写函数的存在并声明其某些属性。终止，不可还原性，和健全的性能，建立了每个程序。ACL 2中封装机制的可用性被认为是快速有效地验证此类算法的关键。
英文摘要：
ACL2 was used to prove properties of two simplification procedures. The procedures differ in complexity but solve the same programming problem that arises in the context of a resolution/paramodulation theorem proving system. Term rewriting is at the core of the two procedures, but details of the rewriting procedure itself are irrelevant. The ACL2 encapsulate construct was used to assert the existence of the rewriting function and to state some of its properties. Termination, irreducibility, and soundness properties were established for each procedure. The availability of the encapsulation mechanism in ACL2 is considered essential to rapid and efficient verification of this kind of algorithm.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
