WALDMEISTER - High-Performance Equational Deduction
WALDMEISTER - High-Performance Equational Deduction
复制标题
WALDMEISTER - 高性能等式推导
DOI：
--
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Bernd Löchner
中科院分区：
文献类型：
--
作者：
T. Hillenbrand;A. Buch;R. Vogt;Bernd Löchner
Waldmeister是一个高性能的单位方程一阶逻辑定理证明器。在Waldmeister的制作过程中，我们采用了工程方法，确定了时间和空间效率的关键点。我们的逻辑三层系统模型由最低层的基本操作组成，我们非常强调高效的数据结构和算法。对于中间层次，其中的推理步骤被聚合到一个推理机，灵活的调整已被证明是必不可少的，在实验评估。顶层包含控制策略和约简排序。虽然在这个级别上只采用标准策略，但在合理的时间内管理了真正的大型证明任务。
Waldmeister is a high-performance theorem prover for unit equational first-order logic. In the making of Waldmeister, we have applied an engineering approach, identifying the critical points with respect to efficiency in time and space. Our logical three-level system model consists of the basic operations on the lowest level, where we put great stress on efficient data structures and algorithms. For the middle level, where the inference steps are aggregated into an inference machine, flexible adjustment has proven essential during experimental evaluation. The top level holds control strategy and reduction ordering. Although at this level only standard strategies are employed, really large proof tasks have been managed in reasonable time.