Proof search in first-order linear logic and other cut-free sequent calculi
Proof search in first-order linear logic and other cut-free sequent calculi
复制标题
一阶线性逻辑和其他无割序贯演算中的证明搜索
DOI：
10.1109/lics.1994.316061
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
N. Shankar
中科院分区：
文献类型：
--
作者：
P. Lincoln;N. Shankar
我们提出了一个通用框架，用于以一阶无剪切顺序进行证明搜索，并将其应用于线性逻辑的特定情况。在此框架中，使用赫布兰德函数来编码通用量化，并使用统一来实例化存在量化器，以便尊重特征性条件。我们提供了此过程的优化，以利用主题逻辑的排他性。我们证明了几个相关的证明搜索程序的健全性和完整性。此证明搜索框架用于证明一阶购物中心的可预订性位于Nexptime中，一阶MLL在NP中。还给出了基于程序的序言实现的性能比较。量化搜索中量化器步骤的优化可以有效地与许多其他基于固定性的优化相结合。<< etx >>
We present a general framework for proof search in first-order cut-free sequent calculi and apply it to the specific case of linear logic. In this framework, Herbrand functions are used to encode universal quantification, and unification is used to instantiate existential quantifiers so that the eigenvariable conditions are respected. We present an optimization of this procedure that exploits the permutabilities of the subject logic. We prove the soundness and completeness of several related proof search procedures. This proof search framework is used to show that provability for first-order MALL is in NEXPTIME, and first-order MLL is in NP. Performance comparisons based on Prolog implementations of the procedures are also given. The optimization of the quantifier steps in proof search can be combined effectively with a number of other optimizations that are also based on permutability.<<ETX>>