arXivDaily arXiv每日学术速递 周一至周五更新
arXiv cs/0208032cs.LO
收藏

作为约束程序设计语言的一阶逻辑

First-order Logic as a Constraint Programming Language

K. R. Apt, C. F. M. Vermeulen

摘要:

我们提供了一个指称语义的一阶逻辑,捕捉两个级别的视图的计算过程中典型的约束编程。在一个层次上,我们有通常的程序执行。在另一个级别,进行约束存储的自动维护。我们证明,由此产生的语义是健全的真理定义。通过具体形式的约束管理策略的实例化,我们得到了几个良好的评价政策的一阶公式。这种语义也可以用来作为在存在块声明和条件的情况下合理实现约束维护的基础。

英文摘要:

We provide a denotational semantics for first-order logic that captures the two-level view of the computation process typical for constraint programming. At one level we have the usual program execution. At the other level an automatic maintenance of the constraint store takes place. We prove that the resulting semantics is sound with respect to the truth definition. By instantiating it by specific forms of constraint management policies we obtain several sound evaluation policies of first-order formulas. This semantics can also be used a basis for sound implementation of constraint maintenance in presence of block declarations and conditionals.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑