Hyper Tableaux
Hyper Tableaux
复制标题
超级画面
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Ilkka Niemelä
中科院分区：
文献类型：
--
作者：
Peter Baumgartner;Ulrich Furbach;Ilkka Niemelä
本文介绍了小句范式表aux的一个变体，我们称之为“超表”。超tableaux保留了分析tableaux的许多相似特征，同时利用了（正）超归结的中心思想，即在一个推理步骤中归结掉一个子句的所有否定文字。所提出的演算的另一个特点是广泛使用普遍量化的变量。这使得新的有效的前向链接证明程序的完整的一阶理论的变种表ux演算。
This paper introduces a variant of clausal normal form table aux that we call “hyper tableaux”. Hyper tableaux keep many desirabl e features of analytic tableaux while taking advantage of the central idea fr om (positive) hyper resolution, namely to resolve away all negative literals of a clause in a single inference step. Another feature of the proposed calculus is th e extensive use of universally quantified variables. This enables new efficient fo rward-chaining proof procedures for full first order theories as variants of table ux calculi.