见证属性和Prolog剪枝的语义
摘要："Prolog中“cut”构造的语义在逻辑编程系统的可取属性，即证明属性的上下文中得到探讨。证明属性涉及对查询响应的运行一致性。描述了具有否定失败和剪枝的Prolog的泛化，证明它没有证明属性。然后描述了系统的限制，该限制保留了剪枝的选择和第一个解行为，同时允许系统具有证明属性。 在受限系统中，剪枝的概念比Prolog的硬剪枝更受限制，但保留了硬剪枝的有用的第一个解行为，而其他提出的剪枝（如“软剪枝”）没有保留。认为受限系统在Prolog剪枝的功能和实用性以及逻辑编程系统内部一致性的需求之间达到了良好的折衷。受限系统具有抽象的语义，该语义依赖于证明属性；这种语义表明，受限系统与逻辑之间具有更深层次的联系，而不仅仅是允许一些逻辑性的计算。 本文的部分内容以不同形式先前发表在1995年国际逻辑编程研讨会的论文集中。"
作者：James H. Andrews
论文ID：cs/0201029
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23