FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs

Authors: Angelos Charalambidis, Panos Rondogiannis and Ioanna Symeonidou

Paper Information

Title:Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
Authors:Angelos Charalambidis, Panos Rondogiannis and Ioanna Symeonidou
Proceedings:ICLP Proceedings of ICLP 2018
Editors: Paul Tarau and Alessandro Dal Palu'
Keywords:Higher-Order Logic Programming, Approximation Fixpoint Theory, Negation in Logic Programming
Abstract:

ABSTRACT. We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first member of the pair is monotone-antimonotone and the second member is antimonotone-monotone. By deriving an extension of consistent approximation fixpoint theory (Denecker et al. 2004) and utilizing the above bijection, we define an iterative procedure that produces for any given higher-order logic program a distinguished extensional model. We demonstrate that this model is actually a minimal one. Moreover, we prove that our construction generalizes the familiar well-founded semantics for classical logic programs, making in this way our proposal a serious candidate for the title of the well-founded semantics for higher-order logic programs.

Pages:31
Talk:Jul 14 12:00 (Session 95E: Foundations I)
Paper: