Analytic Tableaux for Higher-Order Logic with Choice
Analytic Tableaux for Higher-Order Logic with Choice
复制标题
DOI：
10.1007/s10817-011-9233-2
复制
发表时间：
2011-12-01
期刊：
影响因子：
--
通讯作者：
Brown, Chad Edward
中科院分区：
文献类型：
--
作者：
Backes, Julian;Brown, Chad Edward
虽然许多高阶交互式定理证明器包括选择算子，但高阶自动定理证明器迄今为止还没有。为了支持自动推理的存在下的选择操作，我们提出了一个切自由地面tableau演算教堂的简单类型理论的选择。Tableau演算的设计考虑到了自动搜索。特别地，规则仅在公式的顶层结构上操作。此外，我们将量词的实例化项限制在依赖于当前分支的论域中。在基本类型中，实例化的范围是有限的。这两种限制都是为了尽量减少相应的搜索程序必须考虑的规则数量。我们证明了相对于Henkin模型的Tableau演算的完备性。
While many higher-order interactive theorem provers include a choice operator, higher-order automated theorem provers so far have not. In order to support automated reasoning in the presence of a choice operator, we present a cut-free ground tableau calculus for Church's simple type theory with choice. The tableau calculus is designed with automated search in mind. In particular, the rules only operate on the top level structure of formulas. Additionally, we restrict the instantiation terms for quantifiers to a universe that depends on the current branch. At base types the universe of instantiations is finite. Both of these restrictions are intended to minimize the number of rules a corresponding search procedure is obligated to consider. We prove completeness of the tableau calculus relative to Henkin models.