Efficient execution in an automated reasoning environment
Efficient execution in an automated reasoning environment
复制标题
自动推理环境中的高效执行
DOI：
--
复制
发表时间：
2008
影响因子：
1.1
通讯作者：
M. Wilding
中科院分区：
文献类型：
--
作者：
D. Greve;Matt Kaufmann;P. Manolios;J. S. Moore;S. Ray;J. Ruiz;R. Sumners;D. Vroon;M. Wilding
我们描述了一种允许机械化数学逻辑的用户编写优雅逻辑定义的方法，同时允许声音和有效执行。特别是，支持此方法的功能允许用户以逻辑性的方式安装逻辑定义功能的替代可执行文件。这些替代方案通常比它们所取代的逻辑等效术语更有效。这些功能已在ACL2定理供体中实现，我们讨论了ACL2中该功能的几个应用。
We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.