Logic programming: Laxness and saturation
Logic programming: Laxness and saturation
复制标题
逻辑编程：松弛和饱和
DOI：
10.1016/j.jlamp.2018.07.004
复制
发表时间：
2018
影响因子：
0.9
通讯作者：
Komendantskaya E
中科院分区：
文献类型：
--
作者：
Komendantskaya E
一个命题逻辑程序P可以用程序中原子命题集合上的P f P f-余代数来标识。相应的C（PfPf）-余代数，其中C（PfPf）是PfPf上的余自由余单子，通过归结描述导子.这种对应关系已经发展到两种方式，松散的语义和饱和的语义，局部有序的范畴和右Kan扩展的基础上，分别建模一阶程序。我们统一了这两种方法，展示它们作为互补而不是竞争，反映了逻辑编程的定理证明和证明搜索方面。在保持这种统一性的同时，我们进一步细化了松散的语义，给出了存在变量的逻辑程序的有限模型，并在逻辑程序中的变量和局部状态的世界之间建立了精确的语义关系。
A propositional logic program P may be identified with a P f P f-coalgebra on the set of atomic propositions in the program. The corresponding C (P f P f)-coalgebra, where C (P f P f) is the cofree comonad on P f P f, describes derivations by resolution. That correspondence has been developed to model first-order programs in two ways, with lax semantics and saturated semantics, based on locally ordered categories and right Kan extensions respectively. We unify the two approaches, exhibiting them as complementary rather than competing, reflecting the theorem-proving and proof-search aspects of logic programming. While maintaining that unity, we further refine lax semantics to give finitary models of logic programs with existential variables, and to develop a precise semantic relationship between variables in logic programming and worlds in local state.