The Stable Model Semantics for Higher-Order Logic Programming
Bart Bogaerts, Angelos Charalambidis, Giannos Chatziagapis, Babis Kostopoulos, Samuele Pollaci, Panos Rondogiannis
TL;DR
The paper defines a stable model semantics for higher-order logic programming by grounding it in Approximation Fixpoint Theory, unifying two- and three-valued logics and yielding alternative semantics such as well-founded and Kripke–Kleene. It introduces a three-valued type semantics and an operator-based approach that, via a tau isomorphism, reduces to pairs of two-valued interpretations, thereby generalizing classical stable models while preserving minimality and well-founded properties. A broad class of stratified higher-order programs is identified, shown to have a unique two-valued stable model that matches the well-founded model, ensuring robust semantics in common cases. The framework is demonstrated on motivating problems (max-clique), abstract argumentation, and generalized geography, illustrating the approach’s expressiveness and potential as a foundation for future ASP systems. The work also outlines future directions for implementation and exploration of expressivity and efficiency in higher-order stable reasoning.
Abstract
We propose a stable model semantics for higher-order logic programs. Our semantics is developed using Approximation Fixpoint Theory (AFT), a powerful formalism that has successfully been used to give meaning to diverse non-monotonic formalisms. The proposed semantics generalizes the classical two-valued stable model semantics of (Gelfond and Lifschitz 1988) as-well-as the three-valued one of (Przymusinski 1990), retaining their desirable properties. Due to the use of AFT, we also get for free alternative semantics for higher-order logic programs, namely supported model, Kripke-Kleene, and well-founded. Additionally, we define a broad class of stratified higher-order logic programs and demonstrate that they have a unique two-valued higher-order stable model which coincides with the well-founded semantics of such programs. We provide a number of examples in different application domains, which demonstrate that higher-order logic programming under the stable model semantics is a powerful and versatile formalism, which can potentially form the basis of novel ASP systems.