论文标题
FGL中的新重写器功能
New Rewriter Features in FGL
论文作者
论文摘要
FGL是GL的继任者，GL是ACL2的证明程序，它允许将复杂的限制猜想转化为有效的布尔函数表示形式，并使用SAT求解器证明。 FGL的主要重点是使用重写规则允许更大的可编程性。 尽管FGL重写器是在ACL2的重写器上建模的，但我们添加了几个功能，以使重写规则更强大。 一个特定的重点是使重写规则更方便地使用句法域中的信息，从而使它们在许多情况下可以替换内置的原始原则和元规则。 由于比对于在句法级别编程的规则进行编写，维护和证明重写规则的健全性更容易，因此这些功能有助于使用户精确地编程行为或重写器。 我们描述了FGL重写者实施的新功能，讨论解决方案在实施中遇到的一些技术问题的解决方案，并评估将这些功能添加到ACL2重写器中的可行性。
FGL is a successor to GL, a proof procedure for ACL2 that allows complicated finitary conjectures to be translated into efficient Boolean function representations and proved using SAT solvers. A primary focus of FGL is to allow greater programmability using rewrite rules. While the FGL rewriter is modeled on ACL2's rewriter, we have added several features in order to make rewrite rules more powerful. A particular focus is to make it more convenient for rewrite rules to use information from the syntactic domain, allowing them to replace built-in primitives and meta rules in many cases. Since it is easier to write, maintain, and prove the soundness of rewrite rules than to do the same for rules programmed at the syntactic level, these features help make it feasible for users to precisely program the behavior or the rewriter. We describe the new features that FGL's rewriter implements, discuss the solutions to some technical problems that we encountered in their implementation, and assess the feasibility of adding these features to the ACL2 rewriter.
