TY - JOUR
TI - Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
AU - Charalambidis, A.
AU - Rondogiannis, P.
AU - Symeonidou, I.
JO - Theory and Practice of Logic Programming
PY - 2018
VL - 18
TODO - 3-4
SP - 421-437
PB - Cambridge University Press
SN - 1471-0684, 1475-3081
TODO - 10.1017/S1471068418000108
TODO - Computer circuits;  Formal logic;  Semantics, Classical logic;  Fixpoints;  Higher order logic;  Higher-order logic programming;  Monotonic functions;  Negation in logic programming;  Type hierarchies;  Well founded semantics, Logic programming
TODO - 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 an appealing formulation for capturing the well-founded semantics for higher-order logic programs. Copyright © Cambridge University Press 2018.
ER -