There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners
There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners
复制标题
高阶推理机不存在最佳的 β 标准化策略
DOI：
10.1007/978-3-662-48899-7_23
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
C. Benzmüller
中科院分区：
文献类型：
--
作者：
A. Steen;C. Benzmüller
为逻辑框架和高阶定理证明器中的术语的内部表示选择数据结构是影响其性能的关键低级因素。我们提出了一种基于多态类型的无名主干数据结构的术语表示方法，结合了完美的术语共享和显式替换，在相关系统中，a-规范化方法的选择通常是静态固定的，不能在运行时根据输入问题进行调整。因此，主要的策略是实现最左边-最外面的标准化的特定适应。我们介绍了几种不同的归一化策略，并通过约简步长对来自不同(TPTP)领域的约7000个异类问题的性能进行了实证评估，研究表明，不存在普遍存在的最佳归一化策略，并且对于不同的问题域，可以识别不同的最佳归一化策略。评估结果表明，对于高阶推理系统，优先归一化策略的选择依赖于问题。
The choice of data structures for the internal representation of terms in logical frameworks and higher-order theorem provers is a crucial low-level factor for their performance. We propose a representation of terms based on a polymorphically typed nameless spine data structure in conjunction with perfect term sharing and explicit substitutions.In related systems the choice of a-normalization method is usually statically fixed and cannot be adjusted to the input problem at runtime. The predominant strategies are hereby implementation specific adaptions of leftmost-outermost normalization. We introduce several different-normalization strategies and empirically evaluate their performance by reduction step measurement on about 7000 heterogeneous problems from different (TPTP) domains.Our study shows that there is no generally best-normalization strategy and that for different problem domains, different best strategies can be identified. The evaluation results suggest a problem-dependent choice of a preferred-normalization strategy for higher-order reasoning systems.
登录
查看更多内容
一阶模态逻辑的 QMLTP 问题库
DOI：
10.1007/978-3-642-31365-3_35
发表时间：
2012
期刊：
J. Symb. Comput.
影响因子：
--
作者：
Thomas Raths;J. Otten
通讯作者：
J. Otten
使用 TPTP THF 基础设施进行高阶逻辑自动推理
影响因子：
--
作者：
G. Sutcliffe;Christoph Benzmüller
通讯作者：
Christoph Benzmüller
基于 HOL 的一阶模态逻辑证明器
DOI：
--
发表时间：
2013
期刊：
Logic Programming and Automated Reasoning
影响因子：
--
作者：
Christoph Benzmüller;Thomas Raths
通讯作者：
Thomas Raths
LeoPARD - 用于实现高阶推理机的通用平台
DOI：
10.1007/978-3-319-20615-8_22
发表时间：
2015
期刊：
ArXiv
影响因子：
--
作者：
M. Wisniewski;A. Steen;Christoph Benzmüller
通讯作者：
Christoph Benzmüller
Lambda 项的细粒度表示法及其在内涵运算中的应用
DOI：
--
发表时间：
1996
期刊：
Journal of Functional and Logic Programming
影响因子：
--
作者：
G. Nadathur
通讯作者：
G. Nadathur