In this paper we investigate the theoretical foundation of a new bottom-up semantics for linear logic programs, and more precisely for the fragment of LinLog that consists of the language LO enriched with the constant 1. We use constraints to symbolically and finitely represent possibly infinite collections of provable goals. We define a fixpoint semantics based on a new operator in the style of Tp working over constraints. An application of the fixpoint operator can be computed algorithmically. As sufficient conditions for termination, we show that the fixpoint computation is guaranteed to converge for propositional LO. To our knowledge, this is the first attempt to define an effective fixpoint semantics for linear logic programs. As an application of our framework, we also present a formal investigation of the relations between LO and Disjunctive Logic Programming. Using an approach based on abstract interpretation, we show that DLP fixpoint semantics can be viewed as an abstraction of our semantics for LO. We prove that the resulting abstraction is correct and complete for an interesting class of LO programs encoding Petri Nets.
Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
我们定义了一个新的,可拓的,三值语义的高阶逻辑程序与否定。新的语义是基于解释类型的源语言作为三值拟合单调函数在所有级别的类型层次结构。我们证明了这样的拟合单调函数和双值结果函数对之间存在一个双射,其中该对的第一个成员是单调-反单调的,第二个成员是反单调-单调的。通过推导一致近似不动点理论(Denecker et al. 2004)的扩展并利用上述双射,我们定义了一个迭代过程,该过程为任何给定的高阶逻辑程序产生一个杰出的扩展模型。我们证明,这个模型实际上是一个最小的。此外,我们证明,我们的建设推广了熟悉的良好的基础语义的经典逻辑程序,使我们的建议,以这种方式一个有吸引力的制定捕捉良好的基础语义高阶逻辑程序。本文件正在考虑被TPLP接受。
Proceedings 29th and 30th Workshops on (Constraint) Logic Programming and 24th International Workshop on Functional and (Constraint) Logic Programming
(约束)逻辑编程研讨会(WLP)是德国逻辑编程学会(Gesellschaft für Logische Programmierung e.V.,GLP),并汇集了对逻辑编程、约束编程、答案集编程以及数据库和人工智能等相关领域感兴趣的研究人员(不仅来自德国)。函数和(约束)逻辑编程国际研讨会(WFLP)旨在汇集对函数编程,逻辑编程及其集成感兴趣的研究人员,学生和从业者。讲习班有一个共同地点的传统,以促进对高级声明性程序设计语言和相关领域的基础、应用和组合感兴趣的社区之间的跨部门思想和经验交流。
The Stable Model Semantics for Higher-Order Logic Programming
Vrije Universiteit Brussel(布鲁塞尔自由大学);Katholieke Universiteit Leuven(鲁汶大学);Harokopio University of Athens(雅典哈罗科皮奥大学);National and Kapodistrian University of Athens(雅典国立与卡波迪斯特里亚大学)