线性变量分离重写系统的一阶重写理论：自动化、形式化与认证
First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems: Automation, Formalization, Certification.
作者信息
Middeldorp Aart, Lochmann Alexander, Mitterwallner Fabian
机构信息
Department of Computer Science, University of Innsbruck, Innsbruck, Austria.
出版信息
J Autom Reason. 2023;67(2):14. doi: 10.1007/s10817-023-09661-7. Epub 2023 Apr 6.
The first-order theory of rewriting is decidable for linear variable-separated rewrite systems. We present a new decision procedure which is the basis of FORT, a decision and synthesis tool for properties expressible in the theory. The decision procedure is based on tree automata techniques and verified in Isabelle. Several extensions make the theory more expressive and FORT more versatile. We present a certificate language that enables the output of FORT to be certified by the certifier FORTify generated from the formalization, and we provide extensive experiments.
重写的一阶理论对于线性变量分离重写系统是可判定的。我们提出了一种新的判定过程，它是FORT的基础，FORT是一个用于判定和综合该理论中可表达属性的工具。该判定过程基于树自动机技术，并在Isabelle中得到验证。几个扩展使该理论更具表达力，FORT更通用。我们提出了一种证书语言，使FORT的输出能够由从形式化生成的验证器FORTify进行验证，并且我们提供了广泛的实验。
Zotero 插件