布尔约束下的资源分配
摘要：逐步探究带有乘法（或内涵）连词的逻辑的顺序展示中的证明搜索问题。具体来说，我们从线性逻辑的乘法片段开始，并扩展到带有其加法的线性逻辑，另一方面，也扩展到带有捆绑推导逻辑的加法，即BI逻辑。我们提供了一种代数方法，用于计算乘法规则中侧式的分布，该方法允许在获得足够信息后确定证明的一个分支上的公式是否出现或不出现。在这样的规则的结论中，每个公式被分配一个布尔表达式。随着搜索的进行，会生成一组布尔约束方程。我们证明了这样一组方程的解决方案确定了与给定搜索相对应的证明。我们解释了一系列策略，从懒惰到渴望，用于解决约束方程集。我们指出如何系统地将我们的方法应用于大量相关系统。
作者：James Harland, David Pym
论文ID：cs/0012018
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23