一阶逻辑的指称语义中的声音搜索
摘要：一阶逻辑作为约束编程语言的定义和结果的改进视为系统中的重要思想，我们给出了激励性的例子。然后我们为一阶逻辑建立了指示意义的语义学，其中语义宇宙包含由两个组成部分组成的状态：一个可以看作计算答案的替代，以及可以看作原始问题的剩余，尚未由约束编程处理的约束满足问题。这些组件之间的交互由一个称为“infer”的算子调节。在本文中，我们将infer视为对状态集合的算子，以便我们能够分析状态之间的搜索和选择的思想。 对定义和结果的精确改进能够处理这些例子，并且我们展示了，在给定一些合理条件的情况下，新的定义确保了系统对于一阶逻辑的标准解释的正确性。以这种方式，“合理条件”可以被看作是进行正确搜索所需的条件。 我们简要指出了未来研究中如何调查搜索的效率。
作者：C.F.M. Vermeulen
论文ID：cs/0307067
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23