Linear Logic with Isabelle: Pruning the Proof Search Tree
Linear Logic with Isabelle: Pruning the Proof Search Tree
复制标题
伊莎贝尔的线性逻辑：修剪证明搜索树
DOI：
10.1007/3-540-59338-1_41
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
P. D. Groote
中科院分区：
文献类型：
--
作者：
P. D. Groote
本文介绍了乘法加法线性逻辑的通用后向证明搜索策略。这个以伊莎贝尔的基本战术和战术为基础的策略已经付诸实施，并且显得颇为高效。它的效率源自我们在论文中介绍的几种启发式方法。我们证明这些启发式方法保持了完整性。
This paper introduces a general backward proof search strategy for multiplicative additive linear logic. This strategy, which is based on Isabelle's basic tactics and tacticals, has been implemented and appears to be rather efficient. Its efficiency derives from several heuristics that we introduce in the paper. We prove that these heuristics preserve completeness.